Оцените BitVec в Z3Py

Я изучаю 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

Спасибо!


expression evaluate z3py
person BenS    schedule 04.03.2018    source источник

Ответы (1)


arrow_upward
0
arrow_downward

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

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()
person BenS    schedule 04.03.2018
comment
В общем, ваш стиль кодирования меня несколько сбивает с толку. кажется, что было бы проще использовать новые переменные python для новых выражений, чтобы каждая переменная содержала одно конкретное назначение (например, в одиночных статических назначениях). После этого вам будет легче отслеживать изменения. Следовательно, я бы посоветовал не использовать переменные повторно (как вы неоднократно делаете с e1 и e2) - person stklik; 05.03.2018
comment
@stklik этот код является примером. В реальном случае выражения «e1» и «e2» обновляются в цикле на основе дизассемблированных инструкций (более 200 инструкций ADD/SUB/INC/DEC). В конце цикла мы получаем окончательные выражения. Мы заменяем c1 и c2 их значениями, чтобы вычислить упрощенное выражение из более чем 200 инструкций. - person BenS; 05.03.2018