Z3: как закодировать If-the-else в Z3 python?

Question

Я хочу кодировать If-the-else в Z3 python, но не могу найти какие-либо документы или примеры того, как это сделать.

У меня есть пример кода, как показано ниже.

F = True 
tmp = BitVec('tmp', 1) 
tmp1 = BitVec('tmp1', 8) 

Теперь, как я могу закодировать это условие в F:

if tmp == 1, then tmp1 == 100. otherwise, tmp1 == 0 

спасибо.

Answer 1

Вам нужно If функцию Z3 в:

def z3py.If (  a, 
      b, 
      c, 
      ctx = None 
) 

Создать Z3, если-то-иначе выражение.

>>> x = Int('x') 
>>> y = Int('y') 
>>> max = If(x > y, x, y) 
>>> max 
If(x > y, x, y) 
>>> simplify(max) 
If(x <= y, y, x) 

(от here)

Answer 2

Для этого можно использовать If. If принимает три аргумента: условие, выражение, которое должно быть истинным, если условие истинно, и выражение, которое должно быть истинным, если условие ложно. Таким образом, чтобы выразить свою логику, вы бы написать:

If(tmp==1, tmp1==100, tmp1==0)