Values of a set in a model found by Z3

Question

I have a similar question to the one here : How to print a Z3 Set object? from which I couldn't figure how to print the values of a set in a model. I have one enumeration sort (code in Java):

• EnumSort rSort = ctx.mkEnumSort(ctx.mkSymbol("res"), ctx.mkSymbol("res1"));

from which I create a set sort:

• SetSort rSet = ctx.mkSetSort(rSort)

By using this set sort, I create a Z3 constant rID and define a simple membership expression:

• BoolExpr c1 = (BoolExpr)ctx.mkSetMembership(rSort.getConsts()[0], rID);

When c1 is satisfiable, I would like to see one possible value for rID in the model. If I try with a const interpretation (i.e. m.getConstInterp(e) where e is a FuncDecl from the model), I get : "Non-zero arity functions and arrays have FunctionInterpretations as a model. Use FuncInterp.".

When I try with func interpretation (i.e. m.getFuncInterp(e)), I get "Argument was not an array constant". Am I doing something wrong here? Isn't it possible to print the values of set object? Alternatively, is there a better way of representing a variable that may contain multiple values from a sort?

Answer 1

Sets are internally represented by arrays, which in turn have functions as models. getConstInterp fails, because rID is of set-type (internally array-type) and it throws an according exception. From the example it's not clear what e is, but here is an example of how to get at the FuncInterp for rID:

Context ctx = new Context(cfg);

EnumSort rSort = ctx.mkEnumSort(ctx.mkSymbol("res"), ctx.mkSymbol("res1"));
SetSort rSet = ctx.mkSetSort(rSort);
Expr rID = ctx.mkConst("rID", rSet);
BoolExpr c1 = (BoolExpr)ctx.mkSetMembership(rSort.getConsts()[0], rID);

Solver s = ctx.mkSolver();
s.add(c1);
Status status = s.check();
Model m = s.getModel();

System.out.println(status);
System.out.println("Model = " + m);

FuncInterp fi = m.getFuncInterp(rID.getFuncDecl());
System.out.println("fi="+ fi);

Note that the call to getFuncInterp gets the FuncDecl of the constant rID, which may be the source of the confusion.