z3 - 与 Z3 的等效性检查

Question

我还是 Z3 的新手，有一个问题:是否可以使用 Z3 进行等效检查？

如果可能的话，你能给我一个检查 2 个等价公式的例子吗？

谢谢。

Answer 1

对的，这是可能的。有很多方法可以使用 Z3 来实现。最简单的使用程序prove在 Z3 Python API .例如，假设我们要证明公式 x >= 1 and x == 2*y和 x - 2*y == 0, x >= 2是等价的。我们可以使用以下 Python 程序来实现(您可以在 rise4fun 在线试用)。

x, y = Ints('x y')
F = And(x >= 1, x == 2*y)
G = And(2*y - x == 0, x >= 2)
prove(F == G)

我们还可以证明两个公式是等价的，以某个边条件为模。
例如，对于位向量(即机器整数)，x / 2相当于 x >> 1如果 x >= 0(也可用 online )。

x = BitVec('x', 32)
prove(Implies(x >= 0, x / 2 == x >> 1))

请注意，x / 2不等于 x >> 1 .如果我们试图证明它，Z3 将产生一个反例。

x = BitVec('x', 32)
prove(x / 2 == x >> 1)
>> counterexample
>> [x = 4294967295]

Z3 Python tutorial包含一个更复杂的例子:它表明 x != 0 and x & (x - 1) == 0为真当且仅当 x是二的幂。

一般来说，任何可满足性检查器都可以用来证明两个公式是等价的。
证明两个公式F和 G等价于使用 Z3，我们证明 F != G是不可满足的(即，没有使 F 与 G 不同的赋值/解释)。prove就是这样的命令在 Z3 Python API 中实现。这是基于 Solver API 的脚本:

s = Solver()
s.add(Not(F == G))
r = s.check()
if r == unsat:
    print("proved")
else:
    print("counterexample")
    print(s.model())