問題タブ [z3]

私はZ3を使用して、有界モデルチェッカーを構築しています。完全性テストを実装しようとすると、奇妙なパフォーマンスの問題が発生します。完全性テストでは、すべてのパスに各状態が最大で1回含まれていることをすべての状態で確認する必要があります。この特性を満たすパスがまだある場合、Z3はすぐに答えを出しますが、すべてのパスを考慮した場合、Z3は指数関数的に遅いように見えます。

テストケースを次のように減らしました。

私のコンピューターでは、これにより次の実行時間が発生します（パスの長さによって異なります）。

• 3：0.057秒
• 4：0.561秒
• 5：42.602秒
• 6：> 15m（中止）

Intからサイズ64のビットベクトルに切り替えると、パフォーマンスは少し向上しますが、それでも指数関数的に見えます。

• 3：0.035秒
• 4：0.053秒
• 5：0.061秒
• 6：0.106秒
• 7：0.467秒
• 8：1.809s
• 9：2分49.074秒

不思議なことに、長さが10の場合、2m34.197秒しかかかりません。小さいサイズのビットベクトルに切り替えると、パフォーマンスは少し向上しますが、それでも指数関数的です。

だから私の質問は：これは予想されることですか？この「ループのない」制約を定式化するためのより良い方法はありますか？

Microsoft.Z3.dll は、ファイルのプロパティに Z3 Managed DLL として記述されています。

Java は dll をロードできます。プログラマーの好みに応じて、System.loadLibrary または System.load を使用してこれを行います。

Java 設計者が DLL も作成する場合は、javah を使用してインポート/エクスポート宣言を定義できます。残念ながら、それは私の場合ではありません。DLL は、マネージ C# DLL として Microsoft によって既に作成されています。

Microsoft RISE Z3 マネージ APIで見つかったような C# 宣言を取得し、呼び出しを成功させるために Java パッケージ/クラスのプロトタイプを作成する助けが必要です。（DLLがロードされていると確信しています）。

簡単にするために、特定の呼び出しは Microsoft.Z3.h の 03042 行でMicrosoftによって定義されています。サンプルコードは大歓迎です！

サーバーから取得しているエラーは次のとおりです。

Azure で実行されている C# Web ロールがあり、C# プロジェクトは、アプリと共にデプロイする F# dll のコードを呼び出します。

ローカル Azure エミュレーターを使用してローカルで実行している場合、F# コードが呼び出され、正常に実行されます。クラウド内の Azure で実行されている場合、F# コードは特定の時点で失敗し、次の例外が発生します。

x の関数の解析に失敗しました: var(2).Exception: System.IO.FileNotFoundException: ファイルまたはアセンブリ 'FSharp.Core, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a' またはその依存関係の 1 つを読み込めませんでした。システムは、指定されたファイルを見つけることができません。ファイル名: 'FSharp.Core, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a'
at Microsoft.FSharp.Text.Lexing.LexBuffer 1.FromArray(char[] s) at Microsoft.FSharp.Text.Lexing.LexBuffer1.FromString(String s) at Marshal.vars@27.GenerateNext(IEnumerable` 1&次)
WRN: アセンブリ バインディングのログがオフになっています。アセンブリ バインド エラーのログを有効にするには、レジストリ値 [HKLM\Software\Microsoft\Fusion!EnableLog] (DWORD) を 1 に設定します。この機能をオフにするには、レジストリ値 [HKLM\Software\Microsoft\Fusion!EnableLog] を削除します。.デフォルトの機能を使用します。

その理由を示唆するいくつかの投稿を見つけました。

Windows Azure は、アプリケーションの実行をサンドボックス化する一環として、部分信頼でアプリケーションを実行します。ただし、F# コア ライブラリは現在 GAC にインストールされていますが、AllowPartialTrustedCallers 属性はありません。そのため、Azure で実行する F# アプリケーションをビルドする場合、F# ライブラリは --standalone を使用して静的にリンクする必要があります。提供されているテンプレートがこれを処理しますが、次の副作用があることに気付くでしょう: • 通常より長いコンパイル時間 • 大量の参照セット • "RDManaged.dll" へのダミー参照

http://archive.msdn.microsoft.com/fsharpazure

これを回避するために、以下のアドバイスに従い、–standaloneF# ライブラリのビルド構成にフラグを設定します。

http://www.42spikes.com/post/F-and-Azure.aspx

ただし、F# ライブラリはこのフラグでコンパイルされません。次のビルド エラーが発生します。

エラー 3 バイナリ 'obj\Debug\Analyzer.dll' の書き込み中に問題が発生しました: タイプ Microsoft.FSharp.Text.StructuredFormat.Joint の pass2 でエラーが発生しました: エラー: モジュールの 1 つで、タイプ 'System.Collections.IStructuralEquatable' が発行されるモジュール内で定義されます。入力ファイルが見つからない可能性があります FSC 1 1
アナライザー

このビルド エラーは、F# プロジェクトの依存関係によるものでしょうか? これは、FSharp.PowerPack.dll と Microsoft.Z3.dll、およびソリューションの別の C# ライブラリ、AnalyzerCommon.dll (F# と C# の両方のコードが実装する共通インターフェイスのみを含む) を参照します。

F# コードが呼び出されて正常に実行されるのは興味深いことです。これは、コードの特定の部分 (FSharp.PowerPack.dll を使用する数式パーサー) に到達するまでのみです。

どんなヒントでも大歓迎です。

ありがとう、サム

量化記号消去法の結果を表示するにはどうすればよいですか？
z3は次の入力に満足しているようです

ただし、出力と同じように返されます。

ありがとう

これが私がz3で実行したSMT-LIB2.0ベンチマークです：

sat結果は、少なくともZのべき集合（整数）であり、Zのサブセット（一種の要素）への整数のメンバーシップをテストする述語であるモデルでPZあると予想しました。MSPZ

しかし、z3は答えunsatました。

この結果を理解するのを手伝ってもらえますか？具体的には、z3はソートをどのように解釈しますIntか？それは本当に無限と見なされますか？動的に宣言されたソート（ここではソートPZ）はどうですか？

私は現在、Alloy (リレーショナル ロジック/言語) で記述された仕様の制限付きエンジンとして Z3 を試しています。ターゲット言語として UFBV を使用しています。

Z3 オプションを使用して問題を検出しました(set-option :pull-nested-quantifiers true)。

意味的に同一の 2 つの SMT 仕様 Spec1 と Spec2 の場合、Z3 は Spec1 の証明でタイムアウト (200 秒) しますが、Spec2 の証明を行います。

Spec1 と Spec2 の唯一の違いは、関数識別子が異なることです (Java ハッシュ名を使用しているため)。これはバグに関連している可能性がありますか?

共有して議論したい 2 番目の所見はiff、UFBV のコンテキストにおける " " 演算子です。が設定されている場合、この演算子はサポートされません(set-logic UFBV)。私の解決策は、代わりに「=」を使用することでしたが、オペランドに深くネストされた量指定子が含まれていて、「」が設定されている場合、これはうまく機能しませんpull-nested-quantifiers。もう 1 つの節約策は、二重含意を使用することです。

iffここで質問です: UFBVのモデル " " に対する他のより良い解決策はありますか? というのは、二重含意を使用すると、一般に、改善/単純化のためにおそらく使用可能なセマンティック情報が失われると思うからです。

http://i12www.ira.uka.de/~elghazi/tmp/

spec1とspec2は2つの (私が思うに) 意味的に同一の SMT 仕様であり、spec3は "=" をモデル化するために " " を使用した SMT 仕様であり、z3 がタイムアウトします。iff

たとえば、以下のコードでは、パス条件はになりますx>0 && x+1>0。しかし、をx>0意味するのでx+1>0、z3またはpex APIで、x>0両方ではなく、のみを取得する方法はありますか。

ありがとう

Z3 でビット ベクトルを符号付き 10 進数としてきれいに印刷するにはどうすればよいですか?

私は、用語の書き換えを使用して固定サイズのビットベクトル算術問題を解決/簡素化することに焦点を当てたプロジェクトに取り組んでいます。これは、ビットブラストに基づくものなどの決定手順の前のステップとして役立つものです。書き換えという用語は、問題をまったく解決するか、そうでなければ、はるかに単純な同等の問題を生成する可能性があるため、両方を組み合わせると、かなりの速度向上が得られます。

多くの SMT ソルバーがこの戦略を実装していることは承知しています (Boolector、Beaver、Alt-Ergo、Z3 など)。一般に、著者がそのような単純化の手順をいくつかの段落で説明している論文しか見つけられませんでした。用語の書き換えの使用法を詳細に説明しているドキュメントを見つけたいと思います: ルールの例を提供し、AC 書き換えおよび/または他の等式公理の利便性について議論し、書き換え戦略の使用など.

今のところ、CVC Lite によって実行される正規化/単純化の手順について説明しているテクニカル レポートA Decision Procedure for Fixed-Width Bit-Vectorsを見つけました。このようなテクニカル レポートをもっと見つけたいと思います! STP での用語の書き換えに関するポスターも見つけましたが、これは簡単な要約にすぎません。

私はすでにそれらの SMT ソルバーの Web サイトにアクセスし、それらの出版物ページを検索しました...

よく知られているSMTソルバーの現在のバージョンで用語の書き換えがどのように使用されているかについての参照または説明をいただければ幸いです。Z3 は最もスマートな単純化フェーズの 1 つを備えているように見えるので、特に Z3 に興味があります。たとえば、Z3 3.* では新しいビット ベクトル決定手順が導入されましたが、残念ながら、それについて説明している論文を見つけることができませんでした。

ある式Pをアサートしたと仮定し、充足可能性を確認した後、 Z3 からその部分モデルを取得し、それをMと呼びましょう。

ここで、必要に応じて現在のモデルMを拡張することで、別の式Qを満たすことができるかどうかをテストできます。つまり、式P と Qが満足できるかどうかを確認したいのですが、現在の部分モデルによって割り当てられた値を修正します。

あるいは、Z3 に特定の部分モデルを「完成」させることは可能ですか? (つまり、まだ部分モデルを取得したいのですが、場合によっては、部分モデルを拡張して、関数によって割り当てられていない定数/関数を含む可能性のある任意の式Qを評価できるようにしたいと考えています。現行モデル）