問題タブ [smt]

既成のSMTソルバーを使用して、Cコードのシンボリック実行でいくつかの実験を計画しており、どのソルバーを使用するかを考えています。たとえば、SMTコンテストの参加者を見て、オープンソースシステムのみを取り上げ、ビーバー、ブーレクター、CVC3、OpenSMT、サテン、ソノラー、STP、ベリットに絞り込みます。これはまだ長いリストです。

もう少し絞り込んでみると、一部のシステムはビットベクトル演算を処理する機能をアドバタイズしているのに対し、他のシステムは一般的な整数演算を処理する機能のみをアドバタイズしていることに気付きました。原則として、前者はCに対して正しいです。ここで、変数はマシンワードであり、無制限の整数ではありません。実際にはどのくらいの違いがありますか？この種の仕事に一般的な整数システムを使おうとするとどうなりますか？次のシナリオのいずれかが当てはまりますか？

1. ビットベクトルシステムの方が少し効率的ですが、どちらでも問題ありません。

2. 少し調整を加えた一般的な整数システムを使用できます。

3. 一般的な整数システムはsignedintには問題ありませんが（オーバーフローの結果が未定義であるため）、unsignedには間違った答えが返されます。

4. 一般的な整数システムは、マシンワード演算には正しくありません。短いリストを、ビットベクトル演算を提供するシステムのみに減らすことができます。

5. 他に…？

私はできるだけ具体的な質問をしようとしましたが、誰かがリストを絞り込むための他の基準を提案できるなら、それは素晴らしいことです！

SMTLib2 ディレクティブ(get-info all-statistics)は、いくつかの数字を表示します。

さまざまな公理化とエンコーディングをテストするために、ある Z3 の実行が別の Z3 の実行よりも優れている/効率的であると宣言するのに適切な数値を知りたいです。

名前から推測するとnum. qa. inst、量指定子のインスタンス化の数は良い指標 (低いほど良い) ですが、他のものはどうでしょうか?

再帰関数を含むZ3 チュートリアルの例をいくつか試しています。次の例を試してみました。

1. フィボナッチ(セクション 8.3)
2. IsNat (セクション 8.3)
3. 誘導性(セクション 10.5)

Z3は、上記のすべての例でタイムアウトします。しかし、チュートリアルは、誘導のみが非終了であることを暗示しているようです。

Z3 は、再帰関数を含む式の充足可能性をチェックできますか? または帰納的な事実を処理できませんか?

Z3プログラムで次のルールを使用してs、sortの可能な唯一の値を作成していますS。

ただし、上記の式により、Z3は次のエラーを報告します。

特定の種類のドメインに単一の値のみがあることを確認する正しい方法は何ですか？

Z3 を使用して部分文字列について推論しようとしていますが、直感的でない動作に遭遇しました。Z3 は、「xy」が「xy」内にあるかどうかを判断するように求められると「sat」を返しますが、「x」が「x」にあるか、「x」が「xy」にあるかを尋ねられると「unknown」を返します。

この動作を説明するために、次のコードにコメントを付けました。

問題が設定されたので、部分文字列を見つけようとします。

findMeXY代わりにinを検索するとxy、ソルバーは予想どおり 'sat' を返します。ソルバーは「xy」についてこのクエリを処理できるため、「x」についても処理できるはずです。さらに、 で検索するfindMeX='x'と'xy='xy'、「不明」が返されます。

SMTソルバー内でこの問題を表現するための説明、またはおそらく代替モデルを提案できる人はいますか?

Z3 の QBVF ソルバーをいじっていて、存在するアサーションから値を抽出できるかどうか疑問に思っています。つまり、私が次のものを持っているとしましょう：

これは基本的に、「最小」の 16 ビット符号なし値があることを示しています。次に、私は言うことができます：

Z3-3.0 は喜んでこう答えます。

これは本当にクールです。しかし、私がやりたいのは、get-value を介してそのモデルの一部を抽出できるようにすることです。当然のことながら、次のいずれも機能していないようです

いずれの場合も、Z3 は当然、そのような定数はないと不平を言います。(check-sat)呼び出しへの応答によって証明されるように、Z3 がその情報を持っていることは明らかです。get-valueまたは他のメカニズムを介して、存在する値に自動的にアクセスする方法はありますか?

ありがとう..

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

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

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

z3 がこの命名方法を理解していないことは理解していますが、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秒しかかかりません。小さいサイズのビットベクトルに切り替えると、パフォーマンスは少し向上しますが、それでも指数関数的です。

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

これが私が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