斯卡拉^ Z3（Z3版本3.2）和parsesmtlib2string（...）不工作

虽然试图用parsesmtlib2string我打了一个错误来实现测试：斯卡拉^ Z3（Z3版本3.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)

当在取消“检查饱和”我得到“未知”。取消注释“模型”时，我得到“不支持”。

在Z3中使用F＃3.2它只是给我一个Term，但是在Scala中，返回类型是Unit。我浏览了Z3-C API，但没有找到如何使用ist的好例子。

那么，使用smtlib2string获取模型的最佳方法是什么？

顺便说一句：使用Scala^Z3和构建Z3AST工作得很好，我可以使用.checkAndGetModel（）获得一个模型。上面的SMT-LIB2代码适用于F＃.NET parsesmtlib2string方法。

使用“getSMTLIBFormulas，getSMTLIBAsumptions，getSMTLIBDecls，getSMTLIBSorts”之一会产生“Error：parser（data）is not available”。

使用“getSMTLIBError.size”会产生“0”。

来源

2011-09-26 John Smith

由于报告了问题，parseSMTLIB2[...]方法确实应该返回Z3AST。这在scalaz3-3.2.b.jar中得到修复。现在关于SMT-LIB 2解析器的使用，我自己对此不太了解，所以Leo应该可以证实，但我的理解是，您只应该用它来解析公式，而不是发布诸如(check-sat)之类的命令。

这里是我工作的一个例子：现在如果你想以编程方式恢复模型x

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在之前解析并将其传递给解析器，使用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没有表现出很大的。）

来源

2011-09-26 14:15:20 Philippe

大工作！你还有一个名为“.checkAndGetAllModels（）”的函数，我甚至没有找到.NET或C等价的东西......它对我来说工作得很好。你是怎样做的？非常感谢。 Levent Erkok在另一篇文章中提到了这个特性：“Z3：一种更好的建模方式？” –

Philippe是正确的，函数'parseSMTLIB2String'应该被用来解析公式。诸如'check-sat'之类的命令被这个命令忽略。 –

checkAndGetAllModels函数只是将前面模型的否定添加到上下文中，使用推式和弹出式，没有什么太花哨。顺便说一句，你可能不应该尝试在两次调用之间推送新的约束到生成的迭代器。 – Philippe

斯卡拉^ Z3（Z3版本3.2）和parsesmtlib2string（...）不工作

回答

相关问题