AUFBVをサポートしていますか？

Question

Z3はAUFBVをサポートしますか？

次のスクリプトの場合：

(set-logic AUFBV) 
(declare-fun x() (_ BitVec 16)) 
(declare-const t (Array (_ BitVec 16) (_ BitVec 16))) 
(assert (= (select t #x0000) #x0000)) 

オンラインZ3のデモはset-logicコールと幸せになりそうですが、それは種類BitVecとArrayについて不平を言います。 （ちなみに、オンラインデモでも、このような(set-logic blarg)として偽の名前で、かかわらず、論理名のset-logicコールと幸せになりそうです。）SMT-LibのウェブサイトはUFBVもAUFBVどちらも言及していない

が、与えられました（QF_UFBVとQF_AUFBV）、私はZ3がAUFBVもサポートすることを望んでいました。

言うまでもなく、配列は実際には非常に重要な役割を果たしています。私は、AUFBVロジックは、有限の議論を考えれば決定可能なままであるべきだと思います。 Z3がそれをサポートしているのを見るのは本当にうれしいでしょう。

ありがとうございます！

Answer 1

Z3は、自分自身を設定するためにset-logicコマンドを使用しています。 SMTスクリプトにset-logicが含まれていない場合、すべての理論ソルバが有効になります。スクリプトからset-logicコマンドを削除すると、Z3は期待どおりに動作します。あなたが言ったように

は、AUFBVロジックが決定可能です。しかし、複雑さは本当に高いです（NEXPTIME完了）。理論的には、Model Based Quantifier Instantiation（MBQI）モジュールは、Z3がこのロジックの決定プロシージャであることを保証しますが、複雑さが高いため、Z3は多くのスクリプトで失敗します（メモリおよび/または時間なしで実行）。

ロジックAUFBVは公式にサポートされている論理を一覧にありません。 Z3はそれを認識せず、理論ソルバーをインストールしませんでした。したがって、Z3 3.1でこのロジックを使用するには、set-logicコマンドを使用しないでください。

ところで、あなたは本当に配列を必要としません。それらは、量子を使用してUFBVでエンコードすることができます。 多くの場合、量子を使用する場合は、配列理論を避けるのが最善です。 Z3の配列理論ソルバーは、数量問題のない問題に最適化されています。

(set-logic blarg)などの偽のコマンドについては、ロジックが認識されないという警告メッセージを表示するコードを追加しました.Z3は利用可能なすべての理論を使用します。変更はZ3 3.2で利用可能になります。正式にサポートされているロジックのリストにはAUFBVも含まれています。