z3 - 如何消除 Z3 中的位向量运算

Question

我正在尝试使用 z3 来消除表达式

not ((not x) add y)

等于

x sub y

通过这个code :

(declare-const x (_ BitVec 32))
(declare-const y (_ BitVec 32))
(assert (= (bvnot (bvadd (bvnot x) y)) (bvsub x y)))
(check-sat)
(simplify (bvnot (bvadd (bvnot x) y)))

我想得到这样的结果:

sat
(bvsub x y) 

然而，结果是:

sat
(bvnot (bvadd (bvnot x) y))

有人能帮帮我吗？

Answer 1

我们可以使用以下脚本证明 (bvnot (bvadd (bvnot x) y)) 等同于 (bvsub x y)。

(declare-const x (_ BitVec 32))
(declare-const y (_ BitVec 32))
(assert (not (= (bvnot (bvadd (bvnot x) y)) (bvsub x y))))
(check-sat)

在此脚本中，我们使用 Z3 来证明 (not (= (bvnot (bvadd (bvnot x) y)) (bvsub x y))) 是不可满足的。也就是说，不可能找到 x 和 y 的值使得 (bvnot (bvadd (bvnot x) y)) 不同于 (bvsub x y) 的值。

在 Z3 中，simplify 命令只应用重写规则，它忽略断言表达式集。 simplify 命令比使用 check-sat 检查可满足性要快得多。此外，给定两个等价表达式 F 和 G，不能保证 (simplify F) 的结果等于 (简化 G)。例如，在 Z3 v4.3.1 中，简化命令为 (= (bvnot (bvadd (bvnot x) y) 和 (bvsub x y) 生成不同的结果，尽管它们是等价的表达式。另一方面，它为 (= (bvneg (bvadd (bvneg x) y) 和 (bvsub x y) 产生相同的结果。

(simplify (bvnot (bvadd (bvnot x) y)))
(simplify (bvneg (bvadd (bvneg x) y)))
(simplify (bvsub x y))

Here是上述示例的完整脚本。

顺便说一句，如果我们使用 Z3 Python interface，这些示例将更具可读性.

x, y = BitVecs('x y', 32)
prove(~(~x + y) == x - y)
print simplify(x - y)
print simplify(~(~x + y))
print simplify(-(-x + y))

最后，Z3 有更复杂的化简程序。它们以策略的形式提供。 Python 中的教程和 SMT 2.0格式提供附加信息。

另一种可能性是修改 Z3 简化器/重写器。正如您所指出的，not x 等同于 -x -1。我们可以很容易地添加这个重写规则:not x --> -x - 1 到 Z3 重写器。 例如，in this commit ，我添加了一个名为“bvnot2arith”的新选项来启用此规则。 实际实现非常小(5 行代码)。