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 
  )   

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)

(来自 here)