如何打印Z3設置對象？

我一直無法打印/顯示作爲Z3模型的一部分返回的設置對象。考慮下面的例子（在F＃）：如何打印Z3設置對象？

let ctx:Context = new Context() 
let ASort = ctx.MkEnumSort("S",[| "A"; "B"; "C"|]) 
let ASetSort = ctx.MkSetSort(ASort) 
let xs = ctx.MkConst("xs",ASetSort) 
let p = mkPredDecl ctx ("p",[|ASetSort|]) 
let px = ctx.MkApp(p,xs) :?> BoolExpr 
let s = ctx.MkSolver() 
s.Assert (ctx.MkAnd(px, ctx.MkNot(ctx.MkEq(xs,ctx.MkEmptySet(ASort))))) 
assert (s.Check() = Status.SATISFIABLE) 
let xs_interp = s.Model.Eval(xs) 
xs_interp

求解器返回一組（在此情況下一個單獨集合{A}，但它沒有重要性）。我看不到任何實際打印的方式。標準的ToString()方法只是說它的一個數組，並顯示模型顯示該集合內部使用查詢函數表示。我試過以下

let foo xs x = 
    let mem= ctx.MkSetMembership(x,xs_interp) :?> BoolExpr 
    s.Assert mem 
    s.Check()= Status.SATISFIABLE 
Array.filter (foo xs) ASort.Consts

不僅它笨重，它不工作！我想我可以遍歷集合的查詢函數表達式，但是如果Z3中的集合表示改變了它會破壞我的代碼，那對我來說似乎不是那麼好。我缺少API中的某些東西嗎？ ToString（）方法是否可能被修改爲實際打印設置的內容？

來源

2013-04-10 S.N.

Z3通過依賴數組的理論，您可以定義幾個集合操作，例如成員測試，聯合，交集和空集。集合排序只是布爾數組。設置的操作被編譯爲數組的理論，，使得空集對應於布爾數組，該數組對於域中的所有值都爲假。成員資格測試只是陣列選擇。所以你從Z3中得到的模型將代表所有的數組。

數組模型使用輔助函數是正確的。這使得遍歷有點困難。原則上，您可以模式匹配模型返回的術語（它應該將數組值表示爲「（as-array k！32）」term），然後您可以遍歷k！32的模型（或者它恰好被稱爲），這是一個所謂的功能解釋。對不起，這不是獲得有限數組模型的最直接方式，但表示法允許Z3在數組之間來回切換作爲函數。

論文：http://academic.research.microsoft.com/Paper/6558823顯示瞭如何將一些集操作表示爲數組。

來源

2013-04-12 01:50:23

如何打印Z3設置對象？

回答

相關問題