0

このチュートリアルに続いて、チュートリアルのこの最初の例を試しました。

(set-option :print-success false)
(set-logic QF_UF)
(declare-fun p () Bool)
(assert (and p (not p)))
(check-sat)
(exit)

このコマンドを実行しました

java -jar jsmtlib.jar test1.smt

チュートリアルのように取得しunknownないため。unsat

これの何が問題になっているのでしょうか？

4

2 に答える 2

2

使用するソルバーを指定する必要がありました。サーバーとしてyicesを選択しましたが、を使用するとjava -jar jsmtlib.jar --solver yices --exec ./yices test1.smt、すべてが正常に機能します。

于 2012-09-21T18:30:27.287 に答える
1

jsmtlib.jarSMTソルバーのラッパーのようなものだと思います。「不明」の答えはZ3とは何の関係もありません。jsmtlib.jarこの問題については、作者に連絡する必要があります。

Z3を直接使用しようとしましたか？unsatこのスクリプトに戻ります。Z3はオンラインで試すことができます：http： //rise4fun.com/Z3/chyM

オンラインチュートリアルもあります：http： //rise4fun.com/Z3/tutorial/guide

Z3をダウンロードしてマシンにインストールすることもできます： http ：//research.microsoft.com/en-us/um/redmond/projects/z3/download.html

于 2012-09-21T17:58:11.627 に答える