Scala^Z3（Z3 版本 3.2）和 parsesmtlib2string(...) 不工作

Question

在尝试使用 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”。

Answer 1

parseSMTLIB2[...] 方法确实应该返回Z3AST，感谢您报告问题。这是在scalaz3-3.2.b.jar 中修复的。现在关于 SMT-LIB 2 解析器的使用，我自己是新手，所以 Leo 或许应该确认一下，但我的理解是你应该只使用它来解析公式，而不是发出诸如 (check-sat) 之类的命令。

这是一个适合我的例子：

import z3.scala._
val smtlib2String = """
  (declare-fun x () bool)
  (declare-fun y () bool)
  (assert (= x y))
  (assert (= x true))"""

val ctx = new Z3Context("MODEL" -> true)
val assertions = ctx.parseSMTLIB2String(smtlib2String)
println(assertions) // prints "(and (= x y) (= x true))"
ctx.assertCnstr(assertions)
println(ctx.checkAndGetModel._1) // prints "Some(true)", i.e. SAT

现在，如果您想以编程方式恢复x 的模型，我的理解是，唯一的方法是为x 创建一个符号在解析之前将其传递给解析器，使用 parseSMTLIB2[...] 方法的重载定义。以下是你的做法：

val ctx = new Z3Context("MODEL" -> true)
val xSym = ctx.mkStringSymbol("x") // should be the same symbol as in the SMT-LIB string
val assertions = ctx.parseSMTLIB2String(smtlib2String, Map(xSym -> ctx.mkBoolSort), Map.empty)
ctx.assertCnstr(assertions)
val model = ctx.checkAndGetModel._2
val xTree = ctx.mkConst(xSym, ctx.mkBoolSort) // need a tree to evaluate using the model
println(model.evalAs[Boolean](xTree)) // prints "Some(true)"

希望这会有所帮助。

（同样，可能有更简单的方法可以做到这一点，但我不知道。解析方法直接绑定到它们的 C 等效项，only example I could find 没有显示太多。）