用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 >> 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是二的幂.

通常,任何可满足性检查器都可用于表明两个公式是等价的.为了显示两个公式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())