4

実数を使用した SMT2-Lib スクリプトが 2 つありますが、これらは道徳的に同等です。唯一の違いは、一方はビットベクトルも使用し、他方は使用しないことです。

実数とビットベクトルの両方を使用するバージョンは次のとおりです。

; uses both reals and bit-vectors
(set-option :produce-models true)
(define-fun s2 () Real (root-obj (+ (^ x 2) (- 2)) 2))
(define-fun s3 () Real 0.0)
(define-fun s6 () Real (/ 1.0 1.0))
(declare-fun s0 () (_ BitVec 1))
(declare-fun s1 () (_ BitVec 1))
(assert
   (let ((s4 (- s3 s2)))
   (let ((s5 (ite (= #b1 s1) s2 s4)))
   (let ((s7 (+ s5 s6)))
   (let ((s8 (- s5 s6)))
   (let ((s9 (ite (= #b1 s0) s7 s8)))
   (let ((s10 (ite (>= s9 s3) #b1 #b0)))
   (= s10 #b1))))))))

(check-sat)
(get-model)

Boolサイズ 1 のビットベクトルの代わりに使用する、道徳的に同等のスクリプトを次に示します。それ以外の場合は、本質的に同じです。

; uses reals only
(set-option :produce-models true)
(define-fun s2 () Real (root-obj (+ (^ x 2) (- 2)) 2))
(define-fun s3 () Real 0.0)
(define-fun s6 () Real (/ 1.0 1.0))
(declare-fun s0 () (Bool))
(declare-fun s1 () (Bool))
(assert
   (let ((s4 (- s3 s2)))
   (let ((s5 (ite s1 s2 s4)))
   (let ((s7 (+ s5 s6)))
   (let ((s8 (- s5 s6)))
   (let ((s9 (ite s0 s7 s8)))
   (let ((s10 (ite (>= s9 s3) #b1 #b0)))
   (= s10 #b1))))))))

(check-sat)
(get-model)

前者についてはunknownz3 (Mac では v4.1) から入手しましたが、後者satはモデルを適切に生成します。

SMT-Lib2 では実数とビット ベクトルを混在させることはできませんが、Z3 ではこれらの組み合わせを問題なく処理できると思いました。私は間違っていますか？回避策はありますか?

(これらは生成されたスクリプトであることに注意してください。そのため、Bool代わりに使用するだけで(_ BitVec 1)はかなりコストがかかります。他の場所でかなりの変更が必要になるためです。)

4

1 に答える 1

5

新しい非線形ソルバーは、まだ他の理論と統合されていません。実変数とブール値のみをサポートします。実際には、整数変数も使用できますが、それらのサポートは非​​常に限定されています。実際には非線形整数問題を実際の問題として解き、最後に各整数変数が整数値に割り当てられているかどうかをチェックします。さらに、このソルバーは、Z3 で使用できる唯一の非線形 (実数) 算術の完全な手順です。

最初の問題にはビット ベクトルが含まれているため、非線形ソルバーは Z3 では使用されません。代わりに、Z3 は多くの理論を組み合わせた汎用ソルバーを使用しますが、非線形演算については不完全です。

そうは言っても、これが制限であることは理解しており、それに取り組んでいます。(そう遠くない) 将来、Z3 には、非線形演算、配列、ビットベクトルなどを統合する新しいソルバーが搭載される予定です。

最後に、ビットベクトル理論は、Z3 の命題論理に簡単に還元できるため、非常に特殊なケースです。Z3 にはbit-blast、この削減を適用する戦術があります。この戦術により、非線形+ビットベクトルの問題を、実数とブール値のみを含む問題に減らすことができます。例を次に示します ( http://rise4fun.com/Z3/0xl )。

; uses both reals and bit-vectors
(set-option :produce-models true)
(define-fun s2 () Real (root-obj (+ (^ x 2) (- 2)) 2))
(define-fun s3 () Real 0.0)
(define-fun s6 () Real (/ 1.0 1.0))
(declare-fun s0 () (_ BitVec 1))
(declare-fun s1 () (_ BitVec 1))
(declare-fun v2 () (_ BitVec 8))
(assert
   (let ((s4 (- s3 s2)))
   (let ((s5 (ite (= #b1 s1) s2 s4)))
   (let ((s7 (+ s5 s6)))
   (let ((s8 (- s5 s6)))
   (let ((s9 (ite (= #b1 s0) s7 s8)))
   (let ((s10 (ite (>= s9 s3) #b1 #b0)))
   (= s10 #b1))))))))

(assert (or (and (not (= v2 #x00)) (not (= v2 #x01))) (bvslt v2 #x00)))
(assert (distinct (bvnot v2) #x00))
(check-sat-using (then simplify bit-blast qfnra))
(get-model)
于 2012-10-17T14:14:14.087 に答える