問題タブ [smt]

なぜ？

問題が発生するユースケースのコンテキスト

三角形のランダムなアイテムを 3 つ定義します。Microsoft Z3 は次のように出力する必要があります。

• 制約が満たされているか、または無効な入力値がありますか?
• すべての変数が具体的な値に割り当てられている他のすべての三角形アイテムのモデル。

項目を制約するために、assert等式を三角形にする必要があります。ピタゴラスの定理 ( (h_c² + p² = b²) ^ (h_c² + q² = a²)) から始めたかったのです。

問題

Microsoft Z3 には、非線形の算術問題を解決するための限られた機能しかないことを知っています。しかし、一部の手計算機でさえ、次のような非常に単純化されたバージョンを解決できます。

質問

• 2 つの値が指定されている場合、Microsoft Z3 でピタゴラスの定理を解く方法はありますか?
• または: 非線形算術のこれらのケースを処理できる別の定理証明者はいますか?

ご協力ありがとうございます - 何か不明な点があれば、コメントしてください。

解釈されていない並べ替えと関数で遊んでいて、定量化された数式が空のモデルとどのように相互作用するかを完全に理解できません。ここ（ここでもhttp://rise4fun.com/Z3Py/6ets）は、私をやや混乱させるいくつかの簡単な例です：

1. [∀v : False]は未飽和ですが、「直感的に」空のモデルに当てはまります。
2. チェック[∃v : v = v]すると空のモデルが生成されますが、それには満足のいく割り当てがありません。
3. と一見同等のいくつかの式は[∃v : v = v]、どういうわけか z3 が空のモデルを生成するのを防ぎます。[∃v, v1 : v = v1]はその一例です。たとえば、そのような式をソルバーに追加してから、allsat プロシージャに似たものを作成しようとすると (より多くのモデルを除外するために、より多くの制約を追加する)、空のモデルを取得する前に unsat に遭遇します。

では、z3 が量指定子と空のモデルをどのように処理するかを説明しているドキュメント/論文を参照していただけますか? また、空でないモデルのみに注意を向けることを選択した場合、z3 にそれを求める正しい方法は何ですか? のような[∃v, v1 : v = v1]ことがうまくいくように見えますが、より良い方法はありますか?

次のZ3制約をZ3py（Python API）に変換するにはどうすればよいですか。

次の作業例では、一致したモデルを取得しようとしています。この場合、2つの満足のいくモデルがあります。

と

問題は、実行中のソルバーがタイムアウトするまで、一致したモデルを繰り返すことです。満足のいくモデルを繰り返さずに取得するにはどうすればよいですか。

どうもありがとう、

簡単な提案があります。厳密にソートされた整数のリストの最初の要素は、リスト内のすべての要素の最小値であると断言したいと思います。ソートされたリストを定義する方法は、すべての要素が次の要素よりも小さいというローカル不変量を定義することです。私はZ3で次のように命題を定式化しました-

まず、どのクラスの公式が効果的に命題論理であるかを正確に知りたいと思います。私の主張は効果的に命題として分類できますか？第二に、上記の私の定式化は正しいですか？第三に、Z3で、効果的に命題論理である場合にのみ定量化された数式を受け入れるようにするには、どのオプションを設定する必要がありますか？

z3をPythonで動作させるのに問題があります。私はWindows764ビットを実行しています。64ビットのPython3.3.0と64ビットのz34.3.0をダウンロードしました。PATHとPYTHONPATHを更新して、z3\binディレクトリを含めました。ただし、Pythonでz3を使用しようとすると、次のエラーが発生します。

from z3 import *トレースバック（最後の最後の呼び出し）：ファイル ""、1行目、ImportError：'z3'の不正なマジックナンバー：b'\ x03 \ xf3 \ r \ n'

何がうまくいかず、それを修正する方法を誰かが知っていますか？

ありがとう

Z3 Python 関数で 255 を超える引数を使用する方法を教えてください。

次の作業例では、一致したモデルを取得する方法は?

例: 次のソルバーとして

次のサンプルのように、非常に大きな Z3 python プログラムを実行しようとしています。

一致したモデルを取得するためにセット制約を使用しました。一致したモデルは、次のように関数の引数に基づいて取得されます。

しかし、次のエラーが表示されます

Z3 で SMTLIBv2 入力形式とパターンを使用すると、問題が発生します。次の入力で「不明」という結果が返され続けます。

リストを使用して、遷移システムを介して可能なパスを表します。この場合の遷移システムは、L0 から L1 への遷移によってリンクされた状態 L0 と L1 のみで構成されます。assert ステートメントによって、パスを L0 で始まり、長さが 2 になるように制限します。パス (L0 (cons (L1 (cons nil)))) をモデルとして取得することを期待しています。

私はすでに問題を示す最小限の例に要約しようとしましたが、上記のコードが得られました。パターンを使用して「パス」に再帰チェックを実装し、リスト内の 2 つの連続するノードがそれぞれ (遷移) 制約に準拠していることを確認します。連続するコンスのチェックは、この再帰チェックの停止条件として使用されます。上記の例では、checkTransition を使用して再帰チェックを削除しましたが、それでも機能しません。全体のアイデアは、Z3 2.0 と .net API を使用してこのような方法でモデル チェックの問題を表す Milicevic と Kugler による記事にまでさかのぼります。

パターンのインスタンス化によって結果が「不明」になる可能性があることは承知していますが、なぜこのような単純な (?) 例で既に発生しているのか疑問に思っていました。量指定子のサポートを実現するために間違った方法でパターンを使用していますか?

この問題に関するアイデアは大歓迎です!

よろしくカルステン

PS: MacOS X (10.8.3) で Z3 バージョン 4.3.2 を使用しています。前述の記事: Milicevic, A. & Kugler, H., 2011. SMT とリスト理論を使用したモデル チェック。NASA Formal Methods、pp.282–297。

mhs のコメントに基づく編集:

バージョン4.3.2(不安定)からモデルが取得できない問題が発生するようです。さまざまなバージョンでいくつかのトラブルシューティングを行いました。

• Z3 4.3.0 32 ビット、WinXP 32 ビット、インストーラーから
  • 結果: 不明ですが、モデルを提供します
• Z3 バージョン 4.3.1、git checkout 89c1785b73225a1b363c0e485f854613121b70a7、MacOS X、自己コンパイル、これは master ブランチの最新バージョンです....
  • 結果: 不明ですが、モデルを提供します
• master ブランチの他のさまざまなチェックアウト、すべて <= 4.3.1 は同じ結果をもたらします。
• Z3 バージョン 4.3.2、夜間ビルド z3-4.3.2.197b2e8ddb91-x64-osx-10.8.2、MacOS X...
  • 結果: 不明、モデルなし
• Z3 バージョン 4.3.2、夜間ビルド z3-4.3.2.96f4606a7f2d-x64-osx-10.8.2、MacOS X...
  • 結果: 不明、モデルなし

面白い？