arxpy.smt.types module

Convert between pySMT types and bitvector types.

arxpy.smt.types.bv2pysmt(bv, boolean=False, strict_shift=False, env=None)

Convert a bit-vector type to a pySMT type.

Parameters

• bv – the bit-vector Term to convert

• boolean – if True, boolean pySMT types (e.g., pysmt.shortcuts.Bool) are used instead of bit-vector pySMT types (e.g., pysmt.shortcuts.BV).

• strict_shift – if True, shifts and rotation by non-power-of-two offsets are power of two are translated to pySMT’s shifts and rotation directly.

• env – a pysmt.environment.Environment; if not specified, a new pySMT environment is created.

>>> from arxpy.bitvector.core import Constant, Variable
>>> from arxpy.smt.types import bv2pysmt
>>> s = bv2pysmt(Constant(0b00000001, 8), boolean=False)
>>> s, s.get_type()
(1_8, BV{8})
>>> x, y = Variable("x", 8), Variable("y", 8)
>>> s = bv2pysmt(x)
>>> s, s.get_type()
(x, BV{8})
>>> s = bv2pysmt(x +  y)
>>> s, s.get_type()
((x + y), BV{8})
>>> s = bv2pysmt(x <=  y)
>>> s, s.get_type()
((x u<= y), Bool)
>>> s = bv2pysmt(x[4: 2])
>>> s, s.get_type()
(x[2:4], BV{3})

arxpy.smt.types.pysmt2bv(ps)

Convert a pySMT type to a bit-vector type.

Currently, only conversion from pysmt.shortcuts.BV and pysmt.shortcuts.Symbol is supported.

>>> from pysmt import shortcuts, typing  # pySMT shortcuts and typing modules
>>> from arxpy.smt.types import pysmt2bv
>>> env = shortcuts.reset_env()
>>> pysmt2bv(env.formula_manager.Symbol("x", env.type_manager.BVType(8))).vrepr()
"Variable('x', width=8)"
>>> pysmt2bv(env.formula_manager.BV(1, 8)).vrepr()
'Constant(0b00000001, width=8)'

arxpy.smt.types.pysmt_model2bv_model(model, differences=None, masks=None)

Convert a pysmt.solvers.solver.Model into a dict of bit-vector types.

To return Difference (resp. Mask) values instead of Term values, a list of symbolic differences (resp. masks) can be passed as argument. In that case, variables in the model also present in differences (resp. masks) will be added to the bit-vector model as Difference (resp. Mask) objects.

>>> from pysmt import shortcuts
>>> from arxpy.smt.types import pysmt_model2bv_model  # pySMT shortcuts
>>> env = shortcuts.reset_env()
>>> fm = env.formula_manager
>>> formula = fm.Equals(fm.BV(0, 8), fm.Symbol("x", env.type_manager.BVType(8)))
>>> pysmt_model = env.factory.get_model(formula)
>>> for var, val in pysmt_model: print(var, val, var.get_type(), val.get_type())
x 0_8 BV{8} BV{8}
>>> bv_model = pysmt_model2bv_model(pysmt_model)
>>> for var, val in bv_model.items(): print(var, val, type(var), type(val))
x 0x00 <class 'arxpy.bitvector.core.Variable'> <class 'arxpy.bitvector.core.Constant'>