1

I have been unable to print/display a set object returned as part of a Z3 model. Consider the following example (in 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

The solver returns a set (in this case a singleton set {A} but it doesnt matter). I couldn't see any way of actually printing it out. The standard ToString() method simply says its an array and displaying the model shows that the set is internally represented using a query function. I tried the following

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

Not only is it clunky but it doesnt work! I suppose I could walk over the query function representation of the set but that doesnt seem so good to me if the representation of sets in Z3 changes it would break my code. Is there something in the API i am missing? Could the ToString() method be perhaps modified to actually print the set contents?

Motorhead
  • 928
  • 6
  • 16

1 Answers1

1

Z3 lets you define a few set operations, such as membership test, union, intersection, and empty sets by relying on the theory of arrays. Set sorts are just arrays of Booleans. The set operations are compiled into the theory of arrays, such that the empty set corresponds to a Boolean array that is false on all values in the domain. Membership testing is just array selection. So the models you get back from Z3 will represent everything in terms of arrays.

It is correct that the model for arrays use an auxiliary function. This makes it a bit difficult to traverse. In principle you can pattern match the terms returned by the model (it should represent an array value as an "(as-array k!32)" term), you can then traverse the model for k!32 (or what it happens to be called), which is an so-called function interpretation. Sorry, this is not the most direct way to get models for finite arrays, but representation allows Z3 to go back and forth between arrays as functions.

The paper: http://academic.research.microsoft.com/Paper/6558823 shows how some set operations can be represented as arrays.

Nikolaj Bjorner
  • 8,229
  • 14
  • 15