cascada.smt.pysmttypes module

Convert between pySMT types and bitvector types.

`bv2pysmt`	Convert a bit-vector type to a pySMT type.
`pysmt2bv`	Convert a pySMT type to a bit-vector type.
`pysmt_model2bv_model`	Convert a `pysmt.solvers.solver.Model` into a `dict` of bit-vector types.

cascada.smt.pysmttypes.bv2pysmt(bv, boolean=False, parse_shifts_rotations=False, env=None)[source]

Convert a bit-vector type to a pySMT type.

The SMT solver Boolector only supports shifts and rotations where the width of the first bit-vector operand is a power of two. If parse_shifts_rotations=True, shifts and rotations are preprocessed: shifts by extending, shifting and then shrinking back and rotations by extracting and concatenating bits.

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).
parse_shifts_rotations – if True, shifts and rotation are preprocessed as above.
env – a pysmt.environment.Environment; if not specified, a new pySMT environment is created.

>>> from cascada.bitvector.core import Constant, Variable
>>> from cascada.bitvector.secondaryop import BvMaj
>>> from cascada.smt.pysmttypes 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})
>>> s = bv2pysmt(BvMaj(x, y, x + y))
>>> s, s.get_type()
((((x & y) | (x & (x + y))) | (y & (x + y))), BV{8})

cascada.smt.pysmttypes.pysmt2bv(ps)[source]

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 cascada.smt.pysmttypes 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)'

cascada.smt.pysmttypes.pysmt_model2bv_model(model, properties=None)[source]

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

To return Property values instead of Term values, a list of symbolic properties can be passed as argument. In that case, variables in the model also present in properties will be added to the bit-vector model as Property objects.

>>> from pysmt import shortcuts
>>> from cascada.bitvector.core import Variable
>>> from cascada.differential.difference import XorDiff
>>> from cascada.smt.pysmttypes 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.vrepr(), ":", val.vrepr())
Variable('x', width=8) : Constant(0b00000000, width=8)
>>> bv_model = pysmt_model2bv_model(pysmt_model, properties=[XorDiff(Variable("x", 8))])
>>> for var, val in bv_model.items(): print(var.vrepr(), ":", val.vrepr())
XorDiff(Variable('x', width=8)) : XorDiff(Constant(0b00000000, width=8))