arxpy.bitvector.core module

Provide the basic bit-vector types.

class arxpy.bitvector.core.Term

Bases: sympy.core.basic.Basic

Represent bit-vector terms.

Bit-vector terms are constants, variables and operations applied to terms.

Bit-vector terms support many operations with the standard operators symbols (<=, +, ^, etc.). See operation for more information.

This class is not meant to be instantiated but to provide a base class for the different types of terms.

Note that Term inherits the methods of the SymPy class Basic; many of these methods work with bit-vector terms out of the box.

property width

The bit-width of the term.

property formula_size

The formula size of the bit-vector term.

As defined in Complexity of Fixed-Size Bit-Vector Logics.

vrepr()

Return a verbose string representation.

srepr()

Return a short string representation.

doit()

Evaluate the term.

Terms are evaluated by default, but this behaviour can be disabled. See Evaluation for more information.

class_key()

Return the key (identifier) of the class for sorting.

atoms(*types)

Returns the atoms that form the current object.

Similar to SymPy atoms() method, but this method doesn’t throw an exception when one of the arguments is of type ‘int’.

class arxpy.bitvector.core.Constant

Bases: sympy.core.basic.Atom, arxpy.bitvector.core.Term

Represent bit-vector constants.

Bit-vector constants are interpreted as unsigned integers in base 2, that is, a bit-vector \((x_{n-1}, \dots, x_1, x_0)\) represents the non-negative integer \(x_0 + 2 x_1 + \dots + 2^{n-1} x_{n-1}\).

Parameters

• val – the integer value.

• width – the bit-width.

>>> from arxpy.bitvector.core import Constant
>>> Constant(3, 12)
0x003
>>> Constant(0b11, 12)
0x003
>>> Constant(0x003, 12)
0x003
>>> Constant(3, 12).vrepr()
'Constant(0b000000000011, width=12)'

classmethod class_key()

Return the key (identifier) of the class for sorting.

property val

The integer represented by the bit-vector constant.

property formula_size

The formula size of the constant.

bin()

Return the binary representation.

>>> from arxpy.bitvector.core import Constant
>>> print(Constant(3, 4).bin())
0b0011
>>> print(Constant(4, 6).bin())
0b000100

hex()

Return the hexadecimal representation.

>>> from arxpy.bitvector.core import Constant
>>> print(Constant(3, 4).hex())
0x3

oct()

Return the octal representation.

>>> from arxpy.bitvector.core import Constant
>>> print(Constant(4, 6).oct())
0o04

class arxpy.bitvector.core.Variable

Bases: sympy.core.basic.Atom, arxpy.bitvector.core.Term

Represent bit-vector variables.

Parameters

• name – the name of the variable.

• width – the bit-width.

>>> from arxpy.bitvector.core import Variable
>>> Variable("x", 12)
x
>>> Variable("x", 12).vrepr()
"Variable('x', width=12)"

property name

The name of the variable.

property formula_size

The formula size of the variable.

arxpy.bitvector.core.bitvectify(t, width)

Convert the argument t to a bit-vector of bit-width width.

>>> from arxpy.bitvector.core import bitvectify
>>> print(bitvectify(0, 8).vrepr())
Constant(0b00000000, width=8)
>>> print(bitvectify("x", 8).vrepr())
Variable('x', width=8)