4

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

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

(set-option :produce-models true)
(set-logic QF_BV)
(set-info :smt-lib-version 2.0)
(declare-fun a ()(_ BitVec 4))
(declare-fun b ()(_ BitVec 4))
(declare-fun c ()(_ BitVec 4))
(declare-fun z ()(_ BitVec 4))
(assert (= #b1111 z))
(assert (= a b))
(assert (= (bvxor a z) c))
(assert (= b c))
(check-sat)
(get-value ( a ))
(get-value ( b ))
(get-value ( c ))

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

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

4

2 に答える 2

1

コマンドラインから CVC4 を実行するには、フラグを追加します。

--dump-models          output models after every SAT/INVALID/UNKNOWN
                       response [*]

これは get-value ほど具体的ではありません。このオプションは非標準であり、CVC4 は現在、SMT2 パーサーからのこのフラグの設定をサポートしていません。(サポートをご希望の場合はお知らせください。)

于 2014-06-25T18:14:12.923 に答える