如何消除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) 的结果等于(simplify G)。例如，在 Z3 v4.3.1 中，simplify 命令为 (= (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行代码）。