dreal

0熱

1答えて

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