如何打印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设置对象？

回答

相关问题