問題タブ [cvc4]

この例: http://pastebin.com/QyebfD1p z3 と cvc4 は、check-sat の結果として「unknown」を返します。どちらも原因についてあまり詳細ではありません.z3の実行についてより詳細にする方法はありますか?

次の SMT-LIB コードは、Z3、MathSat、および CVC4 では問題なく実行されますが、Alt-Ergo では実行されません。どうなるか教えてください。よろしくお願いします。

以前の投稿で、Z3 SMT-LIB を使用した二面体群 D3 の 1 つの定理が証明されました。この投稿では、次の SMT-LIB コードを使用して、Z3 と CVC4 の両方を使用してそのような定理を証明しようとします。

Z3 または CVC4 を使用してこのコードを実行すると、正しい結果が得られます。Z3オンラインでこのコードをここで実行してください

質問は次のとおりです。

1. Z3 の場合、メッセージunsupported ; :incrementalが生成されます。このメッセージは結果を変更しないようですが、なぜですか?

2. CVC4 の場合、unknownZ3 が生成する間にメッセージが生成されますsat。繰り返しますが、このメッセージは結果を変更しないようです。なぜですか?

3. Mathsat を使用して SMT-LIB コードを実行する方法。

SMT2 標準では、get-value の呼び出しは、check-sat の呼び出し後、および check-sat が "sat" または "unknown" を返す場合にのみ有効であると述べています。

unsat 問題の簡単な例を次に示します。

問題は未解決であるため、get-value コマンドは違法です。いずれか 1 つのアサートを取り出すと、それが sat になり、get-value コマンドが有効になります。私の質問は、check-sat の戻り値をチェックし、sat が返された場合にのみ get-value を呼び出す SMT2 スクリプトをどのように作成するのですか?

フローでさまざまな smt ソルバーを実行し、プログラムの戻り値をチェックしてから出力を解析しているため、get-value を不正に呼び出すことは私にとって問題です。get-value が不正に呼び出された場合、CVC4 はその戻り値をエラー状態に変更します。

FreeBSD でソースからCVC4をコンパイルしようとしていますが、構成時に問題が発生しています。共有オブジェクトが明らかに共通パスにあるにもかかわらず、GMP が見つかりません。

...そしてここにの出力があります./configure：

その後、少しグーグルで調べたところ、関連する可能性があると思われる ABI エラーについて説明している記事を見つけました。次に、ソースから GMP をコンパイルしましたが、configure スクリプトからはうまくいきませんでした。

このエラーの原因は何ですか? 創造的なアイデアや助けをいただければ幸いです。ありがとうございました！

これは、ネイティブ CVC 言語の例です。

CVC4 の C++ API を使用してどのように記述しますか? これを行う方法に関するドキュメントが見つかりませんでした。