z3 - Dose SMTLIB 1.2 には、SMTLIB 2 のような (get-value) 関数があります。

Question

の ( )SMTLIB1.2に相当するものがあるのだろうか。と を使用してさまざまなエンコード テストを実行しています。問題は出力にあり、モデルが数百の補助変数値と混合されたすべての値を取得し続けます。SMTLIB2get-valueSMTZ3 SMT solverSMTLIB1.2

ありがとう

Answer 1

申し訳ありませんが、SMTLIB 1.2 の get-value はありません。

SMTLIB 1.2 は非推奨であり、代わりに SMTLIB 1.2 を 2.0 形式で使用して可能なすべてのことを行うことができるため、構文の v1.2 を使用する本当の理由はありません。