CVC4：定量化機能を持つboolの機能を合成する設定ですか？私は現在、次の形式の式を解くためにCVC4を使用してい

Question

：

ここ

exists f1, ..., fn . P(f1, ..., fn) /\ forall (b1...bk) . Q(f1,...fn,b1,...bk) 

、f1...fnはBoolにBoolのいくつかの数の関数であり、 b1...bkはブール値です。

私の問題は、SMTのUFフラグメントに正当に該当します。それは、量子はありますが、関数とブール値以外のソートはありません。

CVC4のデフォルト設定で問題を解決すると、すべての定量化が有限のドメインを超えているにもかかわらず、Unknownがすぐに返されます。そこmbqi等、だ私は、これらのほとんどはから追加されたという印象を取得し、cegqiの束、fmfの束があります：問題がある

は、CVC4は数量に対処するためのオプションの極めて多数を持っています私の解決策を得るためには20種類の論文を読む必要はありません。

私の質問：この種の問題を解決するための推奨セットがありますか？

SMTコンペのUF Trackで競技していたので、CVC4で可能であることはわかっていましたが、その競技に使用された具体的な議論が見つかりません。

Answer 1

あなたはより多くの情報はここに見つけることができる「--finiteモデル-見つける」試すことができます。 Exactly what quantifiers is SMT complete for?

問題が解決しない場合は、smt-で使用する設定を見しようとする場合がありますcomp： https://www.starexec.org/starexec/secure/details/configuration.jsp?id=220723 最初にオプションを見つけてから、スタックオーバーフローに関する質問が私に指摘されました。