Z3:如何在Z3 python中对If-the-else进行编码？

Question

我想在Z3 python中对If-the-else进行编码,但是找不到任何关于如何做的文档或示例.

我有一个示例代码,如下所示.

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

现在我该如何将这个条件编码为F:

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

非常感谢.

Answer 1

你需要Z3的If功能:

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

创建一个Z3 if-then-else表达式.

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

(从这里)

Answer 2

您可以If为此使用。If接受三个参数：条件、条件为真时为真的表达式和条件为假时为真的表达式。所以为了表达你的逻辑，你会写：

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