z3求解器:使用"parseSMTLIB2String“与rise4fun在线工具获得不同的结果

Question

我正在使用z3开发一个Java程序，但是当我使用"parseSMTLIB2String“方法和rise4fun在线工具测试一个非常简单的编码时，我得到了不同的结果。

下面是我对测试的编码：

(declare-const s Bool)
(assert (exists ((p Bool))(or (not s) p)))
(check-sat)
(get-model)

当我使用rise4fun在线工具测试它时，它给出了结果：

sat
(model
(define-fun s () Bool
false)
)

但是，当我尝试在Java语言中使用"parseSMTLIB2String“方法时，它给出了以下结果：

sat
(define-fun s () Bool
true)

所以我想知道为什么他们给了我不同的结果。

我是不是用错了"parseSMTLIB2String“方法？

下面是我用Java编写的小测试类：

HashMap<String, String> cfg = new HashMap<String, String>();
cfg.put("model", "true");
@SuppressWarnings("resource")
Context ctx = new Context(cfg);

BoolExpr[] formula = ctx.parseSMTLIB2String("(declare-fun s () Bool)\n" + 
  "(assert (exists ((p Bool))(or (not s) p)))", null, null, null, null);

Solver s = ctx.mkSolver();
s.add(formula);

Status result = s.check();

if (result == Status.SATISFIABLE){  
  System.out.println("sat");
  Model m = s.getModel();
  System.out.println(m.toString());
}  

Answer 1

rise4fun没有运行最新版本的Z3；很可能它现在已经相当旧了。对于约束(exists ((p Bool))(or (not s) p))，true和false都是s的正确解决方案。

(仅供参考：parseSMTLIB2String只解析输入文件中的断言，这与在SMT2文件上运行命令行Z3不完全相同。)