我试图使用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))有人会帮助我吗？
I am trying to use the z3 to eliminate the expression
not ((not x) add y)which equals to
x sub yby this 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)))I want to get the result like:
sat (bvsub x y)However, the result is:
sat (bvnot (bvadd (bvnot x) y))Would some one help me out?
最满意答案
我们可以使用以下脚本证明(bvnot (bvadd (bvnot x) y))等效于(bvsub xy) 。
(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 xy)))是不可满足的。 也就是说，不可能找到x和y的值，使得(bvnot (bvadd (bvnot x) y))的值不同于(bvsub xy)的值。
在Z3中， simplify命令只应用重写规则，它忽略了一组断言的表达式。 simplify命令比使用check-sat检查可满足性要快得多。 此外，给定两个等价表达式F和G ，不能保证(simplify F)的结果等于(simplify G) 。 例如，在Z3 v4.3.1中，simplify命令为(= (bvnot (bvadd (bvnot x) y)和(bvsub xy)产生不同的结果，尽管它们是等效的表达式。另一方面，它产生相同的结果for (= (bvneg (bvadd (bvneg x) y)和(bvsub xy) 。
(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有更复杂的简化程序。 它们可用作战术 。 Python和SMT 2.0格式的教程提供了其他信息。
另一种可能性是修改Z3简化/重写器。 正如您所指出的， not x不等于-x -1 。 我们可以轻松地将这个重写规则添加到Z3重写器中， not x --> -x - 1 。 例如， 在这个提交中 ，我添加了一个名为“bvnot2arith”的新选项，它启用了这个规则。 实际实现非常小（5行代码）。
We can prove that (bvnot (bvadd (bvnot x) y)) is equivalent to (bvsub x y) using the following script.
(declare-const x (_ BitVec 32))
(declare-const y (_ BitVec 32))
(assert (not (= (bvnot (bvadd (bvnot x) y)) (bvsub x y))))
(check-sat)
In this script, we used Z3 to show that (not (= (bvnot (bvadd (bvnot x) y)) (bvsub x y))) is unsatisfiable. That is, it is not possible to find values for x and y such that the value of (bvnot (bvadd (bvnot x) y)) is different from the value of (bvsub x y).
In Z3, the simplify command just applies rewriting rules, and it ignores the set of asserted expressions. The simplify command is much faster than checking satisfiability using check-sat. Moreover, given two equivalent expressions F and G, there is not guarantee that the result of (simplify F) will be equal to (simplify G). For example, in Z3 v4.3.1, the simplify command produces different results for (= (bvnot (bvadd (bvnot x) y) and (bvsub x y), although they are equivalent expressions. On the other hand, it produces the same result for (= (bvneg (bvadd (bvneg x) y) and (bvsub x y).
(simplify (bvnot (bvadd (bvnot x) y)))
(simplify (bvneg (bvadd (bvneg x) y)))
(simplify (bvsub x y))
Here is the full script for the examples above.
BTW, these examples are much more readable if we use the 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))
Finally, Z3 has more complex simplification procedures. They are available as Tactics. The tutorials in Python and SMT 2.0 format provide additional information.
Another possibility is to modify the Z3 simplier/rewriter. As you pointed out, not x is equivalent to -x -1. We can easily add this rewrite rule: not x --> -x - 1 to the Z3 rewriter. As an example, in this commit, I added a new option called "bvnot2arith" that enables this rule. The actual implementation is very small (5 lines of code).
更多推荐
发布评论