2

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

4

1 回答 1

2

这些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 等效项，我能找到的唯一示例并没有显示太多。）

于 2011-09-26T14:15:20.853 回答