Evaluate a BitVec in Z3Py

Question

I am learning Z3 and perhaps my question does not apply, so please be patient.

Suppose I have the following:

c1, c2 = z3.BitVec('c1', 32), z3.BitVec('c2', 32)

c1 = c1 + c1
c2 = c2 + c2
c2 = c2 + c1
c1 = c1 + c2

e1 = z3.simplify(c1)
e2 = z3.simplify(c2)

When I print their sexpr():

print "e1=", e1.sexpr()
print "e2=", e2.sexpr()

Output:

e1= (bvadd (bvmul #x00000004 c1) (bvmul #x00000002 c2))
e2= (bvadd (bvmul #x00000002 c2) (bvmul #x00000002 c1))

My question is, how can I evaluate the numerical value of 'e1' and 'e2' for user supplied values of c1 and c2?

For example, e1(c1=1, c2=1) == 6, e2(c1=1, c2=1) == 4

Thanks!

Answer 1

I figured it out. I had to introduce two separate variables that will hold the expressions. Then I had to introduce two result variables for which I can query the model for their value:

e1, e2, c1, c2, r1, r2 = z3.BitVec('e1', 32), z3.BitVec('e2', 32), z3.BitVec('c1', 32), 
                         z3.BitVec('c2', 32), z3.BitVec('r1', 32), z3.BitVec('r2', 32)

e1 = c1
e2 = c2

e1 = e1 + e1
e2 = e2 + e2
e2 = e2 + e1
e1 = e1 + e2

e1 = z3.simplify(e1)
e2 = z3.simplify(e2)

print "e1=", e1
print "e2=", e2

s = z3.Solver()

s.add(c1 == 5, c2 == 1, e1 == r1, e2 == r2)
if s.check() == z3.sat:
    m = s.model()
    print 'r1=', m[r1].as_long()
    print 'r2=', m[r2].as_long()