在尝试使用 parsesmtlib2string 实现测试时,我遇到了一个错误:
println("Hello World!");
var smtlib2String = ""
smtlib2String += "(declare-fun x () bool)" + "\n"
smtlib2String += "(declare-fun y () bool)" + "\n"
smtlib2String += "(assert (= x y))" + "\n"
smtlib2String += "(assert (= x true))" + "\n"
// smtlib2String += "(check-sat)" + "\n"
// smtlib2String += "(model)" + "\n"
smtlib2String += "(exit)" + "\n"
val cfg = new Z3Config
val z3 = new Z3Context(cfg)
z3.parseSMTLIB2String(smtlib2String)
取消注释“Check-sat”时,我得到“未知”。取消注释“模型”时,我得到“不受支持”。
在 Z3 3.2 中使用 F# 只会给我一个 Term,但在 Scala 中,返回类型是 Unit。我查看了 Z3-C API,但没有找到关于如何使用 ist 的好例子。
那么,使用 smtlib2string 获取模型的最佳方法是什么?
顺便说一句:使用 Scala^Z3 和构建 Z3AST 工作得很好,我可以使用 .checkAndGetModel() 获得模型。上面的 SMT-LIB2 代码适用于 F# .NET parsesmtlib2string 方法。
使用“getSMTLIBFormulas、getSMTLIBAssumptions、getSMTLIBDecls、getSMTLIBSorts”之一会产生“错误:解析器(数据)不可用”。
使用“getSMTLIBError.size”产生“0”。