python - Z3：Z3 能告诉我算术运算是否返回具体值吗？

Question

我有一个简单的代码，如下所示：

a, b, c = BitVecs('a b c', 32)
a == b + c
c == b + 5

我们可以很容易地看到 (c - b) 返回一个具体的值（数字 5），但 (a - b) 返回一个抽象的值（因为 a - b == c，它具有未知值）。

问题是：给定上述情况的算术运算，Z3 能否告诉我们结果是具体的，还是不具体的？如果这是可能的，该怎么做？

非常感谢。

Answer 1

Z3 是定理证明器，但我们也可以将其视为约束求解器。我们可以查看诸如a == b + c约束之类的表达式。Z3 Python 接口有一个名为solve. 它试图解决一组约束。那就是它，它试图找到一个使所有约束都为真的“分配”。例如，如果我们执行以下命令（也可在此处获得）。

a, b, c = BitVecs('a b c', 32)
solve(a == b + c, c == b + 5)

它产生了解决方案：

[b = 0, a = 5, c = 5]

我们说解决方案“满足”约束。Z3 还有其他几个命令和 API。有关 Z3 的更多信息，请参阅在线教程。

Answer 2

即使我发现这个问题很老。我想发布我的解决方案，看看 z3 中是否有具体的值。

以下方法通过测试位向量是否始终等于或不等于具体值（零）来测试位向量是否具有具体值。is_trueSimplify 在调用or之前是“必需的” is_false。

bool is_concrete_byte(z3::expr byte) {

    z3::expr zero = context.bv_const(0, 8);

    return (zero == byte).simplify().is_true() ||
            (zero == byte).simplify().is_false();

}