2

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?

Community
  • 1
  • 1
fturkmen
  • 324
  • 3
  • 11

1 Answers1

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.

Christoph Wintersteiger
  • 8,234
  • 1
  • 16
  • 30
  • That works, thanks! I realized that if I set the solver explicitly to QF_LIA I get that error. I haven't given a thorough thought about why but I assume set variables don't work in LIA. – fturkmen Apr 09 '14 at 12:39
  • Another question related to handling sets, is there an implementation of cardinality constraints on sets? Here (https://github.com/psuter/bapa-z3) I see that there is a Scala implementation but I am not sure if there is any in the other implementations of Z3. – fturkmen Apr 16 '14 at 16:03