3

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

not ((not x) add y)

这等于

x sub y

通过此代码：

(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))

有人会帮我吗？

4

1 回答 1

3

我们可以证明这(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))

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

顺便说一句，如果我们使用Z3 Python 接口，这些示例的可读性会更高。

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

最后，Z3有更复杂的简化程序。它们可作为Tactics使用。Python和SMT 2.0格式的教程提供了更多信息。

另一种可能性是修改 Z3 更简单/重写器。正如您所指出的，not x相当于-x -1. 我们可以很容易地添加这个重写规则：not x --> -x - 1到 Z3 重写器。例如，在这个提交中，我添加了一个名为“bvnot2arith”的新选项来启用这个规则。实际实现非常小（5 行代码）。

于 2012-12-27T16:35:42.307 回答