z3 - z3 コマンド ラインに sat/unsat ではなくモード (または unsat コア) を出力させるにはどうすればよいですか?

Question

z3 -smt2 <filename>'sat' または 'unsat' のみを出力します。制約が満たされている場合は Z3 がモデルを出力し、満たされていない場合は unsat コアを出力することを希望します。Z3 のどのオプションを使用すればよいですか?

Answer 1

これにはコマンド ライン オプションはありません。SMTLIB2 ではこれらは別個のコマンドで(get-model)あり、どちらもそれぞれ sat または unsat を返す(get-unsat-core)場合にのみ定義されます。(check-sat)

これらのコマンドを使用するか他のコマンドを使用するかに関係なく、オプションmodelとオプションを有効にする必要があります。これは、ソルバーが正しい情報を追跡できるようにするためです。そうしないと、コマンドとコマンドが後で失敗する可能性があります。unsat-core(get-model)(get-unsat-core)