ビットベクトル（SMTLIB2、Z3）に値を割り当てますか？

Question

私はZ3バージョン3.0を使用しています。以下のように、ビットベクトル変数に値を代入したい。 しかし、Z3はエラー "無効な関数のアプリケーション、行3の位置2の引数のソートの不一致"を報告します。

私の定数＃x0aは間違っていますか？どうすればこの問題を解決できますか？ SMT-LIB 2.0標準で

(set-logic QF_BV) 
(declare-fun a() (_ BitVec 32)) 
(assert (= a #x0a)) 
(check-sat) 

Answer 1

おかげで、#x0aが一定aあなたは避けることができますサイズ32 のビットベクトルであるので、あなたは、ソートの不一致エラーを取得するサイズ8のビットベクトルでありますあなたの例を書き換えることにより、タイプ/ソートエラーメッセージとして：SMT-LIBはまた[num]は、小数点表記であるフォーム(_ bv[num] [size])、ビットベクトルのリテラルをサポートし、

(set-logic QF_BV) 
(declare-fun a() (_ BitVec 32)) 
(assert (= a #x0000000a)) 
(check-sat) 

はビットベクトルのサイズです。 したがって、ビットベクトルリテラル #x0000000aを (_ bv10 32)と書くこともできます。

BTWでは、SMT-LIBはバイナリ表記のビットベクトルリテラルもサポートしています。たとえば、#b010はサイズ3のビットベクトルです。