問題タブ [cvc4]

問題を SMT に変換していますが、sat インスタンスを解くときに SMT ソルバー (MathSat5 および CVC4) が遅いことに気付きました。私の中断は、私の翻訳に何かがあり、翻訳が遅くなっているためです。

サンプルの cnf インスタンスと smt2 の翻訳を参照用に添付しています。以下に、MathSat5、CVC4、および MiniSat を比較するためのより大きなインスタンスのソルバー時間 (翻訳時間を除く) を示しています。

では、これらの時間が大幅に異なる理由を誰かが知っていますか? PS。cvc4 は、5.862 秒を費やしたと言います: 理論 uf symmetry_breaker

ありがとう

秒によると。The SMT- LIBv2 Language and Tools: A Tutorialの 3.9.3 では、SMT-LIBv2 で次のような複合ソートを宣言できます。

私は CVC4 を使用していますが、この構文を受け入れるようです。しかし、要素にアクセスするにはどうすればよいでしょうか? 私は次のことを試しました（およびそのさまざまなバリエーションと、オンラインで見つけた他のもの）：

しかし、これらの演算子はベクトルと配列でしか機能しないようです。このような複合ソートを使用する例は見つかりませんし、チュートリアルや言語標準でそれらの要素へのアクセスについて何も見つけることができません。それはどのように行われますか？それとも、この機能の目的を完全に誤解していましたか?

私のアプリケーション: 一時的な問題をエンコードし、古い状態を新しい状態に変換する状態遷移関数の形式でそれを実行したいので、システムで実験するときに次のようなものを書くことができます:

次のファイルを cvc4 に入力すると、次のエラーが発生します。

ファイルtest.txtは次のとおりです。

コマンドライン:

CVC4 は、Z3のようにビットベクトルの結果モデルを最大化または最小化するオプションですか?

ありがとう。

SMT-LIB では:

このモデルは SAT と UNSAT のどちらである必要がありますか?

いくつかの SMT2 ベンチマークでは(_ bv0 32)、 、(_ bv16 32)、 ... などの表記が次のように使用されていることに気付きました。

QF_FP/schanda/spark/zeros_consistent_2.smt2

http://cvc4.cs.nyu.edu/benchmarks/smtlib2/QF_AUFBV/dwp_formulas/try5_small_difret_functions_wp_vdir.rev_xstrcoll_mtime.il.wp.smt2

http://rise4fun.com/Z3/e1s

ただし、これは理論宣言内のそのような記号への参照ではありません。

http://smtlib.cs.uiowa.edu/theories.shtml

それについて何かコメントはありますか？それらの意味は何ですか？

ありがとう ！