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

ここで私の質問: 結果が「unsat」になるのはなぜですか? コード内の simple コマンドは、myfun1 と myfun2 が同じ結果になるように有効な割り当てを取得できることを示しています。

私のコードに何か問題がありますか、それとも z3 のバグですか?

誰でも私を助けてください。どうも

4

1 に答える 1

2

誤った結果は、Z3 数式/式プリプロセッサのバグが原因でした。このバグは修正されており、現在のリリース (v4.3.1) には既に含まれています。(mod (+ a b))このバグは、またはの形式の式を使用するベンチマークに影響を与え(mod (* a b))ました。

ここでオンラインで例を再試行し、期待される結果を得ることができます。

于 2013-02-02T13:36:37.243 に答える