問題タブ [z3]

次の単純な SMT-LIB プログラムに示すような問題を見つけました。

SMT-LIB コード:

これにより、次の警告が表示されます。

警告メッセージが気になります。何かが欠けていることはわかっていますが、理解できません。誰でもこの問題で私を助けることができますか?

こんにちは私はZ3SMTソルバーを初めて使用します。関連するAPIを使用して、プログラムでZ3を呼び出すことができることを知っています。しかし、私はZ3SMTソルバーで次のことをしたいと思います。

1. プログラムで1つの入力ファイルをZ3にフィードするにはどうすればよいですか？
2. ソリューションを段階的に取得するにはどうすればよいですか？

例えば：

最後に、数式を解いた後、結果を1つの出力ファイルに保存するようにZ3に依頼するにはどうすればよいですか？

私が見ることができるアイデアやドキュメントはありますか？

百万ありがとう!!!

QF_AUFBV の問題を解決するために、Z3-3.2 の c-api (Linux 上) を使用しています。

式が満足できるものであれば、モデルから自由配列変数の値を読み出したいと思います。

次のコードの行に沿って何かを試しましたが、これを行う方法の一般的な考え方が正しいかどうかを知りたいです:

入力 Z3_ast 配列は、間違いなく自由な配列式です。Z3_eval は true を返すので、式の評価は成功したように見えますが、Z3_is_array_value は false を返します。配列式で成功した Z3_eval の結果が配列値になると予想していたのに、そうでないのはなぜですか?

ところで、すべての model_func_decl を反復処理し、get_symbol_string を比較してその配列に適したものを見つけようとすることで、目的の情報を取得することができました。そのため、情報は Z3 のどこかで入手できるようですが、それは優れた解決策とは言えません。

これについて助けてくれてありがとう。

よろしく、フロリアン

こんにちは Leonardo: z3 (v3.2) は、Mac と Linux でタイムアウトを指定するためのコマンド ライン スイッチ "-T:10" を受け入れますが、無視しているようです。(Windows で試したことはありません。) Linux/Mac リリースでもタイムアウトがサポートされていれば、本当に素晴らしいことです。

(これは私の 2 回目のヘルプの試みです。質問/アプローチが意味をなさない、または明確でない場合は、私に知らせてください。 Z3 と私の SBA)

UFBV Z3 ロジックを使用したリレーショナル仕様の境界検証に取り組んでいます。私が調査している現在の問題は、すべての可能なモデルの改ざんを必要とし (到達可能性述語の否定的な使用のため)、高い境界でのソルバーのパフォーマンスを殺します。

可能性のあるモデルの一部だけが実際に興味深い (他と同形ではない) ため、対称性を破る手法 (SAT 分野で知られている) を導入しようとしています。

ただし、私が対称性破りの公理と呼んでいるものを使用すると、場合によっては Z3 のパフォーマンスを向上させることができますが、ソルバーの一般的な動作は不安定になります。

私のアプローチの 1 つ (最も有望なアプローチだと思います) は、ドメイン間の関係の対称性を破ることに基づいています。これは、関係 R の各ドメイン D と各原子 a \in D 公理を導入し、R^{M} と R^{M[a+1/a]} のバイナリ表現に順序を強制します。ここで、M は仕様のモデル。同種の関係の場合、公理は緩和されます。

R \subset AxA を関係とする。R に対する私のリラックスした対称性の破れの公理は次のようになります。

私の問題は、この SBA を使用した効果が安定していない/一貫していないことです。バインドとバインド、フォーム仕様とは異なります。また、SBA のすべてまたは 1 つだけを使用すると、パフォーマンスに影響します。

SAT のコンテキストでは、いわゆる対称性破りの述語 (SBP) アプローチの成功は、SAT ソルバーのバックトラッキング機能に基づいています。とりわけ、SBP。

• Z3 のコンテキストでの相違点 (ある場合) は何ですか?
• これらの公理を使用して探索空間を剪定するように解決を強制するにはどうすればよいですか (バックトラックする場合)。
• SBA に (量指定子) パターンを使用すると役立ちますか?

よろしく、

アブバクル アクラフ エル ガジ

Z3初心者です。しかし、Z3に入力された次のプログラムでのタイムアウトの理由を理解したい：

もう 1 つの質問は、バージョン 3.2 の forall に何か新しいものはありますか? (x Int) の周りに追加の括弧を配置する必要がありました。そうしないと、エラーがスローされました。

ありがとう。

基本的に、私はZ3に、値が10より大きい任意の整数を与えるように依頼したいと思います。したがって、次のステートメントを記述します。

この数量詞をモデルに適用するにはどうすればよいですか？これを達成するために（assert（> x 10））と書くことができることを私は知っています。ただし、モデルに数量詞が必要なので、値が10を超えることが保証されている整数定数を宣言するたびに、整数定数ごとにステートメント（assert（> x 10））を挿入する必要はありません。宣言しました。

x86命令のシンボリック解釈を行っています。たとえば cmp 命令の場合、比較の符号とオペランドが等しいかどうかは eflags レジスタの 2 ビットに格納されます。

これが私のコードです：

問題は、z3 API に (想定される) ブール型の並べ替え (私の例では ZF) を (任意の長さの) ビットベクトルに変換する関数が見つからないことです。

ビットベクトルを返すZFのiteステートメントを使用して関数を作成することを考えましたが、これを行う従来の方法を知りたいです。

ありがとう、

ヘイジ。

how can I make a datatype that contains a set of another objects. Basically, I am doing the following code:

But Z3 tells me unknown sort for A and B. If I remove "Set" it works just as the guide states. I was trying to use List instead but it does not work. Anyone knows how to make it work?

TPTP ファイル (例: http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Problems&Domain=SYN&File=SYN054+1.p ) で Z3 を使用する場合、どの公理を見つける方法がありますか?予想を証明するために使用されましたか？あるいは、Z3 は TPTP プルーフを作成できますか?

乾杯