Z3バージョン2.19と3.2 w.r.tの間に違いはありますか？ SMTLIB-2コードの構文？

Question

Z3 V3.1をインストールした後、SMT-LIBコードが正しく動作しません。それは私の以前のバージョン（Z3 V2.19）ではかなり良いものでした。

(define-fun getIP ((o0 Int) (o1 Int) (o2 Int) (o3 Int)) BitVec[32] 

    (bvor (bvshl (int2bv[32] o0) (int2bv[32] 24)) 

      (bvshl (int2bv[32] o1) (int2bv[32] 16))))  

(declare-funs ((dip BitVec[32]) (m BitVec[32]))) 

(declare-funs ((s Bool) (d Bool) (y Int) (z Int))) 

(declare-funs ((r0 Bool) (r1 Bool) (f Bool))) 

(declare-funs ((r0do0 Int) (r0do1 Int) (r0do2 Int) (r0do3 Int) (r0m Int) (r0nh Int))) 

(declare-funs ((r1do0 Int) (r1do1 Int) (r1do2 Int) (r1do3 Int) (r1m Int) (r1nh Int))) 

(declare-funs ((fso0 Int) (fso1 Int) (fso2 Int) (fso3 Int) (fsm Int))) 

(declare-funs ((fdo0 Int) (fdo1 Int) (fdo2 Int) (fdo3 Int) (fdm Int) (fp Int) (fnh Int))) 

(declare-funs ((so0 Int) (so1 Int) (so2 Int) (so3 Int))) 

(declare-funs ((do0 Int) (do1 Int) (do2 Int) (do3 Int))) 

(assert (=> f (and (= fso0 172) (= fso1 16) (= fso2 0) (= fso3 0) (= fsm 16) 

      (= fdo0 150) (= fdo1 96) (= fdo2 1) (= fdo3 0) (= fdm 24) 

      (= fp 0)))) 

(assert (=> r0 (and (= r0do0 150) (= r0do1 96) (= r0do2 0) (= r0do3 0) (= r0m 16)))) 

(assert (=> r1 (and (= r1do0 172) (= r1do1 16) (= r1do2 0) (= r1do3 0) (= r1m 16)))) 

(assert (=> s (and (= so0 172) (= so1 16) (= so2 0) (= so3 1)))) 

(assert (=> d (and (= do0 150) (= do1 96) (= do2 1) (= do3 120)))) 

(assert (= m (int2bv[32] 16))) 


(assert ((= dip (getIP so0 so1 so2 so3)))) 

(check-sat) ; sat 

(model) 

バージョン3.1で実行するには、上記のコードを変更する必要があります。

Answer 1

Z3 3.xは、SMT 2.0規格に準拠しています。バージョン2.xはそうではありませんでした。たとえば、SMT 2.0にはdeclare-funsコマンドはありません。 32ビットベクトルソートはBitVec[32]の代わりに(_ BitVec 32)です。 Z3はまだ非準拠のSMT 2.0パーサーをサポートしています。コマンドラインオプション-smtcを入力するだけです。つまり、SMT 2.0標準に移行することをお勧めします。 SMT 2.0入力言語は、Z3の公式入力言語です。さらに、このフロントエンドでは多くの新機能しか使用できません（例：パラメトリックタイプ）。