2012-01-25 20 views
3

私はZ3 SMTソルバーで次のことを証明しようとしています:((x*x) + x) = ((~x * ~x) + ~x)。 これは、Cプログラミング言語のオーバーフローセマンティックのために正しいです。 Z3からz3から間違った結果

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

出力は次のとおりです:

は、今私は、次のSMT-libのコードを書かれている

0 
0 
unsat 

今、私の質問:なぜ結果が "UNSAT" とは?私のコードのsimplifyコマンドは、myfun1とmyfun2が同じ結果を持つように有効な割り当てを得ることが可能であることを示しています。

私のコードに問題がありますか、これはz3のバグですか?

誰でも助けてください。 Thx

+1

Cのような整数で作業する場合、手動のエンコーディングでの演習でない限り、数学的な整数ではなくビットベクトルを使用することをお勧めします。 – Philippe

+3

クイックコメント:この誤った結果は、Z3の式プリプロセッサのバグが原因です。これは修正され、修正は次のリリースで利用可能になります。このバグは、 '(mod(+ a b))'や '(mod(* a b))'という形式の式を使用するベンチマークに影響します。 –

+0

@GManNickG:良い点、私はそれを行います。 –

答えて

2

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

例文hereをオンラインで再試行して、予期した結果を得ることができます。