smt2 Namespace Reference

Variables
	a = ExprId("a", 64)
	b = ExprId('b', 32)
	c = ExprId('c', 16)
	d = ExprId('d', 8)
	e = ExprId('e', 1)
	left
tuple	cond
	right
	t_z3 = TranslatorZ3()
	t_smt2 = TranslatorSMT2()
	e_z3 = t_z3.from_expr(e)
	smt2 = t_smt2.to_smt2([t_smt2.from_expr(e)])
	result = parse_smt2_string(smt2)
	smt2_z3 = result[0]
	s = Solver()

Variable Documentation

a

smt2.a = ExprId("a", 64)

b

smt2.b = ExprId('b', 32)

c

smt2.c = ExprId('c', 16)

cond

tuple smt2.cond

Initial value:

=  (
    ExprSlice(
        ExprSlice(
            ExprSlice(a, 0, 32) + b, 0, 16
        ) * c,
        0,
        8
    ) << ExprOp('>>>', d, ExprInt(0x5, 8))
)

d

smt2.d = ExprId('d', 8)

e

smt2.e = ExprId('e', 1)

e_z3

smt2.e_z3 = t_z3.from_expr(e)

left

smt2.left

Initial value:

=  ExprCond(
    e + ExprOp('parity', a),
    ExprMem(a * a, 64),
    ExprMem(a, 64)
)

result

smt2.result = parse_smt2_string(smt2)

right

smt2.right

Initial value:

=  ExprCond(
    cond,
    a + ExprInt(0x64, 64),
    ExprInt(0x16, 64)
)

s

smt2.s = Solver()

smt2

smt2.smt2 = t_smt2.to_smt2([t_smt2.from_expr(e)])

smt2_z3

smt2.smt2_z3 = result[0]

t_smt2

smt2.t_smt2 = TranslatorSMT2()

t_z3

smt2.t_z3 = TranslatorZ3()