斯卡拉^ 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（...）不工作

回答

相關問題