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 のバグですか?
誰でも私を助けてください。どうも