z3 - リストの理論は決定可能ですか？

Question

リストのz3理論が決定可能かどうか疑問に思っていますか？理論を使って、不満であるが座っていない事実しか証明できないように思われるので、それが実際に決定可能であるかどうか私は興味があります。ご協力いただきありがとうございます。

Answer 1

Z3では、理論が決定可能であると言うとき、私たちは通常、数量詞のない問題について話します。Z3で実装されたリストの理論は決定可能です。ただし、 z3の外積のように、数量詞と解釈されていない関数を使用するとすぐに、問題は決定不能になります。Z3はいくつかのフラグメントを決定できますが、z3の外積で説明されている問題は、Z3でサポートされているフラグメントにはありません。実際、Z3はこれと同様の問題のモデルを構築することはできません。したがって、モデルを構築しようとして永久に実行されるか、を返すことを諦めunknownます。結果unknownまだ役に立つかもしれません。場合によっては、Z3が「候補モデル」を作成することがあります。つまり、問題のすべての普遍的な式を満たしていないが、すべての数量詞のない式、および普遍的な式の多くのインスタンスを満たしている解釈です。これを実現するには、モジュールMBQIを無効にする必要があります。MBQIが有効になっている場合、Z3はすべての数量詞を満たす解釈を見つけようとし続けます。例として、これを行う方法を示します。

http://rise4fun.com/Z3/kGtk

秘訣は、スクリプトの冒頭に含めた次の2つのコマンドです。

(set-option :auto-config false)
(set-option :mbqi false) 

このコマンドを使用してget-value、Z3によって生成された解釈がを満たしていることを示しました(assert (= (first (head l)) a))。一方、の解釈はappend、この例の普遍的な公式を実際には満たしていません。