dReal SMTソルバー反例

Question

dReal SMTソルバーは反例を返しますか？私は生産モデルが真である例を見ましたが、反例を生成する方法はわかりません。また、dReachツールには--visualizeオプションがあるため、dRealはいくつかのモデル情報を生成する必要があります。しかし、.smt2ファイルを実行すると、反例を表示する方法が見つからないようです。

Answer 1

O.k.それは簡単です:)。 dRealは（get-model）を使用する通常の.smt2規則に従いませんが、コマンドラインオプション--modelを使用してモデルを取得できます。

例：dReal - モデルmicrowave1.smt2