3

我正在尝试使用 Z3 SMT Solver 证明以下内容：((x*x) + x) = ((~x * ~x) + ~x). 这是正确的，因为 c 编程语言中的溢出语义。

现在我编写了以下 smt-lib 代码：

(declare-fun a () Int)

(define-fun myadd ((x Int) (y Int)) Int (mod (+ x y) 4294967296) )
(define-fun mynot ((x Int))         Int (- 4294967295 (mod x 4294967296)) )
(define-fun mymul ((x Int) (y Int)) Int (mod (* x y) 4294967296) )

(define-fun myfun1 ((x Int)) Int (myadd (mynot x) (mymul (mynot x) (mynot x))) )
(define-fun myfun2 ((x Int)) Int (myadd x (mymul x x)) )

(simplify (myfun1 0))
(simplify (myfun2 0))

(assert (= (myfun1 a) (myfun2 a)))
(check-sat)
(exit)

z3 的输出是：

0
0
unsat

现在我的问题是：为什么结果“不满意”？我的代码中的简化命令表明可以获得有效的分配，以便 myfun1 和 myfun2 具有相同的结果。

我的代码有问题还是z3中的错误？

请任何人都可以帮助我。谢谢

4

1 回答 1

2

不正确的结果是由于 Z3 公式/表达式预处理器中的错误造成的。该错误已得到修复，并且已经是当前版本 (v4.3.1) 的一部分。该错误影响了使用以下形式的公式的基准：(mod (+ a b))或(mod (* a b)).

我们可以在这里在线重试示例，并获得预期的结果。

于 2013-02-02T13:36:37.243 回答