Z3: how to encode If-the-else in Z3 python?

Question

I want to encode If-the-else in Z3 python, but cannot find any docs or sample on how to do that.

I have a sample code like below.

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

Now how can I encode this condition into F:

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

Thanks so much.

Answer 1

You'll need Z3's If function:

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 If for this. If takes three arguments: the condition, an expression that should be true if the condition is true and an expression that should be true if the condition is false. So to express your logic, you'd write:

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