与 Z3 的等效性检查 [英] equivalence checking with Z3

问题描述

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

i am still new with Z3, and have a question: is it possible to use Z3 to do equivalence checking?

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

if that is possible, could you give me one example of checking 2 formulas for equivalence?

谢谢.

推荐答案

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

Yes, it is possible. There are many ones to accomplish that using Z3. The simplest one uses the procedure prove in the Z3 Python API. For example, suppose we want to show that the formulas x >= 1 and x == 2*y and x - 2*y == 0, x >= 2 are equivalent. We can do that using the following Python program (you can try it online at 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(也可在线).

We can also show that two formulas are equivalent modulo some side-condition. For example, for bit-vectors (i.e., machine integers), x / 2 is equivalent to x >> 1 if x >= 0 (also available online).

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

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

Note that, x / 2 is not equivalent to x >> 1. Z3 will produce a counterexample if we try to prove it.

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

Z3 Python 教程 包含一个更复杂的示例:它表明 x!= 0 和 x &(x - 1) == 0 为真当且仅当 x 是 2 的幂.

The Z3 Python tutorial contains a more complicate example: it shows that x != 0 and x & (x - 1) == 0 is true if and only if x is a power of two.

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

In general, any satisfiability checker can be used to show that two formulas are equivalent. To show that two formulas F and G are equivalent using Z3, we show that F != G is unsatisfiable (i.e., there is no assignment/interpretation that will make F different from G). That is how the prove command is implemented in the Z3 Python API. Here is the script based on the Solver API:

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

这篇关于与 Z3 的等效性检查的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！