我有一个简单的代码，如下所示:
a, b, c = BitVecs('a b c', 32)
a == b + c
c == b + 5
我们可以很容易地看到，(c - b) 返回一个具体值(数字 5)，但 (a - b) 返回一些抽象值(因为 a - b == c，其值未知)。
问题是:给定像上面这样的算术运算，Z3 能否告诉我们结果是具体的还是不具体的？如果可以的话，该怎么做？
非常感谢。
最佳答案
Z3是一个定理证明器，但我们也可以将其视为一个约束求解器。我们可以将诸如a == b + c之类的表达式视为约束。 Z3 Python 界面有一个名为 solve 的命令。它试图解决一组约束。也就是说，它试图找到一个使所有约束成立的“任务”。例如，如果我们执行以下命令(也可用 here )。
a, b, c = BitVecs('a b c', 32)
solve(a == b + c, c == b + 5)
它产生解决方案:
[b = 0, a = 5, c = 5]
我们说该解决方案“满足”约束。 Z3 还有其他几个命令和 API。 有关 Z3 的更多信息，请参阅online tutorial .
关于python - Z3:Z3能告诉我算术运算是否返回具体值吗？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/16000228/