問題タブ [smt]

私は、算術、数量詞、平等の理論を組み合わせたZ3を実験しています。これはあまり効率的ではないようです。実際、可能な場合は、数量詞をすべてのインスタンス化された地上インスタンスに置き換える方が効率的であるようです。f次の例を考えてみましょう。この例では、sortの2つの引数を取りObj、解釈されたsortを返す関数の一意の名前の公理をエンコードしましたS。この公理は、引数の各一意のリストがf一意のオブジェクトを返すことを示しています。

これはロジックでそのような公理を定義する標準的な方法ですが、このように実装すると計算コストが非常に高くなります。これには4つの定量化された変数が含まれ、それぞれが8つの値を持つことができます。これは、これが8^4 = 4096平等になることを意味します。これを証明するには、Z30.69sと2016年の数量詞のインスタンス化が必要です。この式のインスタンスを生成する簡単なスクリプトを書くと、次のようになります。

これらの公理を生成するのに0.002秒かかり、Z3でそれを証明するのにさらに0.01秒（またはそれ以下）かかります。定義域内のオブジェクト、または関数への引数の数をf増やすと、この違いは急速に増加し、定量化されたケースはすぐに実行不可能になります。

これは私に不思議に思います：私たちが有界ドメインを持っているとき、なぜ私たちはそもそもZ3で数量詞を使うのでしょうか？SMTはヒューリスティックを使用して解決策を見つけることを知っていますが、接地されたインスタンスをSMTにフィードする単純なドメイン固有のグラウンダーと効率的に競合することはできないと感じています。これはSATの解決にすぎません。私の直感は正しいですか？

Microsoft Research が開発した SMT ソルバーである Z3 を使用して、一次理論の可能なすべてのモデルを取得しようとしています。最小限の作業例を次に示します。

この命題のケースでは、満足のいく代入が 2 つあります。f->trueとf->falseです。Z3 (および一般的な SMT ソルバー) は、満足のいくモデルを 1 つだけ見つけようとするため、すべての解を直接見つけることはできません。ここでという便利なコマンドを見つけました(next-sat)が、Z3 の最新バージョンではこれがサポートされなくなったようです。これは私にとっては少し残念なことですが、一般的にこのコマンドは非常に便利だと思います。これを行う別の方法はありますか？

私は現在、C プログラムの「パス」を対応する SMT クエリに変換して、このパスの実現可能性をテストするコードに取り組んでいます。SMT-LIB v1.2 クエリを作成し、Z3 2.11 と QF_AUFBV ロジックを使用してクエリを解決する作業コードがあります。私は現在、このコードを Z3 4.3 に移植しています。これは、それ以降に発生した可能性のある速度の進歩を利用するためです。特に、以前のコードでは、24 個の値を割り当てるだけのクエリで長い時間 (約 22 分) かかるように思われるためです。 3 次元配列を作成し、配列内の特定の位置の値をチェックします。

ただし、QF_AUFBV ロジック (SMT-LIB v2.0 標準の時点) は、多次元配列、または値も配列である配列 (より深い可能性がある) をサポートしなくなったようです。クエリから「(set-logic QF_AUFBV)」という行を取り出すと、Z3 4.3 はクエリを処理できますが、それでも時間がかかります。

多次元配列のサポートが SMT-LIB v2.0 標準で停止された理由と、使用できる代替ロジックを誰かが知っているかどうか疑問に思っていました。また、QF_AUFBV 理論を指定する行を取り出したときに、Z3 がどのようなロジックを使用していたのかも疑問に思っていました。

ありがとう！

[1] で説明されている決定/インスタンス化手順 (その実装を含む) の「実際的な」影響をテストすることに興味があります。

私は欲しい：

1) SMT ベンチマークを取得し、(おそらく完全な) インスタンス化されたバージョンを返し、戦略を適用する「ツール」。これが不可能な場合は、

2) この戦略を実装する Z3 バージョンと、オンとオフを切り替えるオプション。

それについて私を助けてもらえますか？

[1] Modulo Theories による充足可能性における定量化された数式の完全なインスタンス化

私は以下のような単純なZ3pythonコードを持っています。「print」行は、その上の行に格納されていた「y」を返すことを期待しています。代わりに、結果として「A[x]」が返されました。

Select()によって保存された値を返さないのはなぜStore()ですか？

ありがとう。

SMTlib2 形式でソートを使用すると問題が発生します。たとえば、次のように Interval を定義します。

関数から新しい間隔を返すにはどうすればよいですか? 例えば：

これはうまくいきません。私の質問は、特定の種類のオブジェクトを作成してインスタンス化するにはどうすればよいですか? また、それらのフィールドにアクセスするにはどうすればよいですか?

現在、フィールド ゲッターとして作成した 2 つの UF を使用していますが、コンストラクターの作成方法はまだわかりません。

ありがとう、ヌーノ

スコーレム化を使用して、私の理論で存在記号を削除しようとしています。これは、存在記号を、存在記号のスコープ内の全称記号変数によってパラメーター化された関数に置き換えることを意味します。

ここで、Z3でこれを行う方法の説明を見つけましたが、まだ問題があります。次の2つの関数を想定します。

真であるような整数、すなわち。f2が存在するので、それは真であるはずだと私は信じています。存在記号の式に定数を導入することにより、スコーレム化を適用します。t(f1 t)t=3

次に、存在記号を含む式は次のように書き直されます。

これは機能しません。つまり、定数cの値は3ではありません。定数に解釈を与えていないためだと思います。これcを追加すると正常に機能するためです(assert (= c 3))が、これにより存在記号の概念全体が失われます。数量詞。これが機能するように、あまり明確に解釈しない方法はありcますか？

C APIを使用してCraig補間関数を生成しようとしていますが、間違った結果が得られます。ただし、同じ問題をZ3_write_interpolation_problemを介してファイルにダンプし、iZ3を呼び出すと、期待される補間が得られます。

同じ結果を再現できるようにコードを添付します。z34.1を使用しています

次のコマンドを使用して実行可能ファイルを生成します。

g ++-fopenmp-o補間補間.c-I/home / jorge / Systems / z3 / include -I / home / jorge / Systems / z3 / iz3 / include -L / home / jorge / Systems / z3 / lib -L ​​/ home / jorge / Systems / z3 / iz3 / lib -L ​​/ home / jorge / Systems / libfoci-1.1 -lz3 -liz3 -lfoci

制約は基本的に次のとおりであることに注意してください。

A =（x=0およびx1=x0+2およびx2=x1 + 2）、

およびB=（x2> 10）

明らかに不満です。さらに、共通の変数がx2だけであることも簡単にわかります。したがって、有効な内挿にはx2しか含めることができません。

実行可能ファイル./interpolationを実行すると、ナンセンス補間が得られます。

ただし、「iz3 tmp.smt」（tmp.smtはZ3_write_interpolation_problemを使用して生成されたファイル）を実行すると、有効な補間が得られます。

unsat補間：（<= x2 10）

これはバグですか？または、Z3_interpolateを呼び出すときに、いくつかの重要な前提条件が欠落していますか？

PSCAPIでiZ3を使用した例は見つかりませんでした。

乾杯、ホルヘ