Z3：如何在 Z3 python 中编码 If-the-else？答案

【问题标题】：Z3: how to encode If-the-else in Z3 python?Z3：如何在 Z3 python 中编码 If-the-else？
【发布时间】：2013-04-12 09:45:03
【问题描述】：

我想在 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

非常感谢。

【问题讨论】：

标签： python z3

【解决方案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)

（来自here）

【讨论】：

【解决方案2】：

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

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

【讨论】：

你确定可以这样使用吗？根据我在网上看到的示例，它始终用作 C++ 中的 (?:) 运算符（例如，y = condition?x1 : x2）。我实际上是在寻找代表 IF-THEN 的东西，而不是“暗示”。
@Mohammed 我看不出 OP 的 if tmp == 1, then tmp1 == 100. otherwise, tmp1 == 0 和 tmp == 1 ? tmp1 == 100 : tmp1 == 0 之间有什么区别。在我看来，这只是表达同一事物的两种不同符号。
好的@sepp2k，谢谢。我的意思是tmp1 = (tmp == 1)? 100 : 0 我不是 100% 确定，但如果我们分配相同的变量，与tmp == 1? tmp1 == 100 : tmp2 == 0 相比，它可能是相同的。不管怎样，我才意识到这是一个有 7 年历史的帖子。感谢您的回复。
@Mohammed 我不完全确定你的意思。 Z3 没有赋值的概念。如果您正在分析某种编程语言，那么在 Z3 中，像 tmp1 = (tmp == 1)? 100 : 0 这样的结构确实可以建模为 Z3 中的 If(tmp==1, tmp1==100, tmp1==0)，假设变量从未重新分配。