問題タブ [z3]

parsesmtlib2string を使用してテストを実装しようとすると、エラーが発生しました。

「Check-sat」のコメントを外すと、「unknown」と表示されます。「モデル」のコメントを外すと、「サポートされていません」と表示されます。

Z3 3.2 で F# を使用すると Term が返されますが、Scala では戻り値の型は Unit です。Z3-C API を調べましたが、ist の使用方法に関する適切な例が見つかりませんでした。

では、smtlib2string を使用してモデルを取得する最良の方法は何でしょうか?

ところで: Scala^Z3 を使用して Z3AST をビルドすると問題なく動作し、.checkAndGetModel() を使用してモデルを取得できます。上記の SMT-LIB2 コードは、F# .NET parsesmtlib2string メソッドで正常に動作します。

「getSMTLIBFormulas、getSMTLIBAssumptions、getSMTLIBDecls、getSMTLIBSorts」のいずれかを使用すると、「エラー: パーサー (データ) が利用できません」というメッセージが表示されます。

「getSMTLIBError.size」を使用すると「0」になります。

Z3バージョン2.18を使用して、次のような式を単純化しようとしています。

• （および（>（-（-x 1）1）0）（> x 0））
• （または（>（-（-x 1）1）0）（> x 0））

（> x 2）および（> x 0）のようなものを取得したいと考えています。

次の入力ファイルを使用してZ3を実行しています。ここで、Fは上記の式の1つです。

これは、次の出力が得られる論理和でうまく機能します。

ただし、接続詞を使用すると、次のようになります。

Z3に上記の式をさらに単純化するように強制する方法はありますか？取得できるといいのですが(not (<= x 2))。

PS：Z3にその出力をインライン化させる方法はありますか（つまり、(not (<= x 0))の代わりに持つ(let (($x35 (<= x 0))) (not $x35))）

ありがとう、ガス

Z3のINIオプションの詳細なドキュメントはありますか。QF_BVの問題に最適なオプションを見つけるために、試行錯誤のアプローチをとらなければなりませんでした。z3の実行を高速化するオプションが他にもあるかどうかはまだわかりません。誰かがINIオプションの既存の詳細な説明を指摘できれば素晴らしいと思います。

ありがとう。

APIからZ3を使用しており、制約をデバッグする方法を探しています。コードがコンパイルされ、Z3が制約で実行されますが、制約に問題があります。Z3に与えた制約を調べて、何が間違っているか、何が欠けているかを判断したいと思っていますが、非常に読みやすい方法でこれを行う方法がわかりません。問題は、SMTLIB_DUMP_ASSERTIONSのような機能を使用しても、自由変数に意味のある名前が提供されないことです。同じ式を何度も再利用しているので、ほとんどすべてが生成された変数に拘束されます。

入力制約のファイルをダンプする方法はありますか？ここで、自由変数は私が割り当てた名前を持っていますか？フォーマットは特に気にしませんが、SMTLIB1または2がいいでしょう。

Z3 (V3.2) アセンブリを GAC に入れたいのですが、署名されていません。その理由はありますか？

シンボリック実行（Klee）のコンテキストでのインクリメンタルソルビングに必要です。シンボリック実行パスの分岐のポイントでは、ソルバーコンテキストを2つの部分に分割する必要があります。真と偽の条件です。もちろん、コストのかかる回避策があります。空のコンテキストを作成し、すべての制約を再生します。

Z3_contextを分割する方法はありますか？そのような機能を追加する予定はありますか？

ノート

深さ優先のシンボリック探索を使用すると、コンテキストの分割を回避できます。つまり、現在の実行パスが「終了」に達するまで探索されるため、このパスは今後探索されなくなります。この場合、分岐点に到達するまでポップして、別の条件分岐の探索を続けるだけで十分です。ただし、Kleeの場合、多くのシンボリックパスが「同時に」探索される（真と偽の分岐の探索がインターリーブされる）ため、ソルバーコンテキストソルバーの切り替え（各メソッドにZ3_context引数があります）と分岐（このためのメソッドはありません、それが私に必要なものです）。

ありがとう！

テキスト形式でZ3を使用すると、define-fun後で再利用するための関数を定義するために使用できます。例えば：

define-fun関数の本体をどこでも繰り返すのではなく、Z3 API（私はF＃を使用）で作成する方法を考えています。重複を避け、数式を簡単にデバッグするために使用したいと思います。で試してみましContext.MkFuncDeclたが、解釈できない関数しか生成されないようです。

F# と Z3 3.2 API を使用して、LIA で量指定子の削除を行っています。

Z3 にQUANT_ARITHは、Cooper の方法または LIA 量指定子の除去のためのオメガ テストの使用を示す構成がありました。ELIM_QUANTIFIERSしかし、そのオプションはZ3 2.6で置き換えられました( Z3 リリース ノートを参照)。

Z3 3.2 が量指定子の削除に使用する方法をどのように認識しているか内部的に尋ねたいのですが? ユーザーは以前のように方法の選択に影響を与えることができますQUANT_ARITHか?

さらに、戦略仕様言語の導入により、Z3 では、これらのメソッドを拡張または組み合わせることで、量指定子の削除をカスタマイズできますか?

z3 SMT-LIB 2.0 ベンチマークでアサーションに名前を付ける方法を教えてください。SMT-LIB の標準構文を使用したいのですが、z3 はそれを理解していないようなので、z3 で動作するものを探しています。必要なのは、ラベル付きの未飽和コアを取得することです。

私がテストしたベンチマークの例を次に示します。

矛盾 (x < y and y <= x) のため unsat コア {hyp4, hyp5} を期待していますが、z3 は次を返します。

z3 がこの命名方法を理解していないことは理解していますが、z3 のドキュメントで別の方法を見つけることができませんでした。

私を手伝ってくれますか？

libgmp.so.3 に対する Z3 の依存関係は、Linux パッケージでは解決されていないため、ユーザーはこのライブラリを提供する必要があります。ただし、このライブラリは非常に古く、すぐには利用できません。

この問題を回避する方法を知っている人はいますか? 私は現在 x86_64 を実行していますが、この不足している依存関係を回避するには、多大な手間がかかります。

Linux パッケージを修正して、予想されるライブラリをディストリビューションに含めることはできますか?