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 回答