問題タブ [smt]

今日、この一見重大なバグに遭遇しました。

この Z3 スクリプトを検討してください。(完全を期すために以下に再掲します。)

式は未飽和です。最初に、追加の仮定を使用して式を確認し、unsat期待どおりに取得します。ただし、もう一度確認すると、何も仮定せずに Z3 が報告するようになりsatました。モデルを求めると、明らかに間違ったモデルが得られます (本質的に矛盾してい(distinct 1 1)ます)。

(check-sat ...)最初のものを(push)andで囲むと(pop)、結果は期待どおりになります。check-satこれは、 に追加の仮定が渡されると、不健全な単純化がコンテキストに適用されることを示唆しています。

check-sat間違った使い方をしているのではないでしょうか?

左または右に任意の量だけビット単位のロールを行う推奨される方法はありますか?

たとえば、バイトで - 0x57 rolr 3 = 0xEA.

Z3py ドキュメントで「ロール」操作を見つけられませんでした。各ビットに s を使用することを考えてBitVecいましたが、それは効率的ではないようです/おそらく機能しません。アドバイスをいただければ幸いです。

編集：これまでの回答に感謝します。私は今それを吸うので、これはよりAPIの質問です。ここに私が出発点として持っているものがあります。

これは何も出力せず、モデルは利用できません。

smt の問題のすべての満足のいくインスタンスに、他の smt の問題からの一致するインスタンスがあるかどうかを確認する必要があります。つまり、「A のすべてのインスタンスに B st のインスタンスが存在します ....」 ここで、A と B は、いくつかの smt-lib コードから生成された sat モデルです。

いろいろ考えてるけどどうしたらいいのかわからない

一次理論に関する事実を証明するために Z3 の使用を最適化する実験を行っています。現在、私は Python で 1 次理論を指定し、そこで量化子を接地し、すべての節を証明目標の否定とともに Z3 に送信します。私は、結果を最適化できることを望む次の考えを持っています:証明の目標に関連する理論の数式のみを Z3 に送りたいです。この概念について詳しくは説明しませんが、直感は単純だと思います。私の理論は数式の結合であり、証明目標の真理値に影響を与える可能性のある結合のみを送信したいのです。

私の質問は次のとおりです。これは効率の改善につながるのでしょうか、それとも Z3 はすでに同様の方法を使用していますか? Z3 は、最後のアサーションが証明の目標であると常に想定しているとは思わないため、これを最適化する方法がないため、そうではないと思います。

Z3 が対処できない単純な一連の制約があります。

http://pastebin.com/3eaLQ9wx

結果を得るために制約を微調整する方法はありますか? これはより大きな制約セット (数千) の単純な例ですが、このような単純な例でも機能しないことに何となく困っています。

前もって感謝します ！！

z3とmathsatを使用していくつかの実験を行う必要があります。私はすでにmathsatで実験を終えました。mathsatの入力ファイルを作成するには時間がかかり、z3の入力ファイルを再度作成したくありません。Mathsatは、「msat」ファイルからの「smt」ファイルの生成をサポートしています。変換コマンドを以下に示します。

私の質問は、z3がこの「smt」ファイルを認識できるかどうかです。

クリックしてファイルを表示

このファイルは SMT2.0 規格に準拠していますか? 少なくとも z3 はそれを受け入れることができます。ところで、'declare-const' と 'declare-fun' の違いは何ですか? たとえば、Bool 変数を宣言するために、declare-const a Boolorと書くことができますdeclare-fun a() Bool。

私は Z3 を使用して、CUTE、DART、または (おそらく) SAGE と非常によく似た、深さ優先の順序で状態空間を探索するシンボリック エグゼキューターによって生成されたパス条件を解決しています。Z3 のさまざまな使用方法を実験しています。極端な場合、すべてのクエリを Z3 に送信し、その直後に (リセット) します。もう 1 つは、すべての追加の分岐制約を (プッシュ) し、パス条件を正しく弱めるために必要な最小限のバックトラックを (ポップ) (ポップ) します。問題は、すべての状況で他の戦略よりもうまく機能する戦略がないように見えることです。プッシュは最高の利点を提供するようですが、すべてのクエリの後に Z3 をリセットすると、プッシュ/ポップを実行するよりも 1 桁以上高速になるいくつかのケースに遭遇しました。通信のオーバーヘッドはごくわずかであることに注意してください。ほとんどすべての時間が check-sat 内で費やされます。

共有する経験がある人、または Z3 によって内部的に保持されている状態 (レンマなど) に関する何らかの兆候があり、その動作を明確にするのに役立ちますか? また、他の SMT ソルバーの動作はどうですか?

Java を SMT Z3 ソルバーと統合する方法を教えてください。理論的な質問だけでなく、いくつかの実装経験についても説明していただければ幸いです。