z3 - 使用 Z3 进行等价检查

Question

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

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

谢谢。

Answer 1

是的，有可能。有很多使用 Z3 来实现这一点。最简单的一个使用Z3 Python APIprove中的过程。例如，假设我们要证明公式和是等价的。我们可以使用以下 Python 程序来做到这一点（您可以在rise4fun在线尝试）。x >= 1 and x == 2*yx - 2*y == 0, x >= 2

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 >> 1if x >= 0 （也可在线获得）。

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 教程包含一个更复杂的示例：它表明x != 0 and x & (x - 1) == 0当且仅当x是 2 的幂时这是正确的。

一般来说，任何可满足性检查器都可以用来证明两个公式是等价的。为了证明两个公式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())