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作为服务器，使用yices java -jar jsmtlib.jar --solver yices --exec ./yices test1.smt，一切正常。

于 2012-09-21T18:30:27.287 回答
1

我相信这jsmtlib.jar是 SMT 求解器的某种包装器。“未知”的答案与 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 回答