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

问题:

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.

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

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