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