1

我无法打印/显示作为 Z3 模型的一部分返回的集合对象。考虑以下示例（在 F# 中）：

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() 方法以实际打印设置的内容？

4

1 回答 1

1

Z3 允许您根据数组的理论定义一些集合操作，例如隶属度测试、并集、交集和空集。集合排序只是布尔数组。集合操作被编译到数组理论中，使得空集对应于一个布尔数组，该数组在域中的所有值上都为假。成员资格测试只是数组选择。因此，您从 Z3 获得的模型将以数组的形式表示所有内容。

数组模型使用辅助函数是正确的。这使得遍历有点困难。原则上，您可以对模型返回的术语进行模式匹配（它应该将数组值表示为“（as-array k！32）”术语），然后您可以遍历模型以查找 k！32（或者它发生了什么被调用），也就是所谓的函数解释。抱歉，这不是获取有限数组模型的最直接方法，但表示允许 Z3 作为函数在数组之间来回切换。

论文：http ://academic.research.microsoft.com/Paper/6558823展示了如何将一些集合操作表示为数组。

于 2013-04-12T01:50:23.573 回答