Z3: how to code if-else-else in a Z3 python?

Question

I want to encode If-the-else in python Z3, but cannot find any documents or examples of how to do this.

I have some sample code as below.

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

Now, how can I encode this condition in F:

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

Many thanks.

Answer 1

You will need the Z3 function If:

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

Create a Z3 if-then-else expression.

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

(from here )

Answer 2

You can use Iffor this. Iftakes three arguments: a condition, an expression that must be true if the condition is true, and an expression that must be true if the condition is false. Therefore, to express your logic, you must write:

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