Оценить BitVec в Z3Py

Question

Я изучаю Z3 и, возможно, мой вопрос не подходит, поэтому, пожалуйста, будьте терпеливы.

Предположим, у меня есть следующее:

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)

Когда я печатаю их 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))

У меня вопрос, как я могу оценить числовые значения "e1" и "e2" для пользовательских значений c1 и c2?

Например, e1(c1=1, c2=1) == 6, e2(c1=1, c2=1) == 4

Спасибо!

Answer 1

Я понял. Мне пришлось ввести две отдельные переменные, которые будут содержать выражения. Затем мне пришлось ввести две переменные результата, для которых я могу запросить модель на предмет их значения:

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()