使用 Z3 进行等价检查答案

【问题标题】：equivalence checking with Z3使用 Z3 进行等价检查
【发布时间】：2012-12-18 09:37:02
【问题描述】：

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

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

谢谢。

【问题讨论】：

标签： z3

【解决方案1】：

是的，这是可能的。有很多使用 Z3 来实现这一点。最简单的一种使用Z3 Python API 中的过程prove。例如，假设我们想证明公式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 是 2 的幂时，x != 0 and x & (x - 1) == 0 为真。

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

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

【讨论】：

@LeonardodeMoura 指向 Rise4fun 的链接无效。他们是否删除了服务？