Z3 Enumerating all satisfying assignments

Question

I am trying to solve a problem similar to the one here (Z3: finding all satisfying models) where I need to find all satisfying assignments of SMT formulae that contain set variables. I understand the idea in the link since it is similar to what some SAT solvers do to iterate through solutions: add the negation of the solution to obtain a different solution. However, when I use the set variables (which are implemented as arrays in Z3) the things get a little complicated or perhaps I miss something. Assume that I have two constraints added to the solver as follows:

    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);

    BoolExpr c2 = ctx.mkGt(ctx.mkIntConst("x"), ctx.mkInt(10));

    Solver s = ctx.mkSolver();
    s.add(ctx.mkAnd(c1,c2));

Now I would like to find all satisfying assignments for my formula in Z3. Theoretically I would have an if block inside an iteration to add the inequalities between variables and their current values, and continue until UNSAT:

    while (s.check() == Status.SATISFIABLE){
    Model m = s.getModel()
     //for each decl in m
       //if (funcDecl) getValue and add negation for the declaration
       //if (consDecl) getValue and add negation for the declaration
    //add disjunction of negation formulae to s 
    }

However I couldn't make it work since I can't construct the negation subformula for the variables. Is there an easy way to enumerate all satisfying assignments of an SMT formulae similar to the one above in Z3? Is there any example code somewhere that does something similar?

[EDIT] I realized that the post here ((Z3Py) checking all solutions for equation) excludes the use of arrays and uninterpreted functions in enumeration. I am not sure if the issue is mainly implementation related or a more fundamental one.

The models for arrays are essentially functions that map indices to values. The negation of a model with functions requires a constraint that says at least one of the function values must be different. This can be done, but it might result in very big formulas. Not sure what you couldn't make work, is this a conceptual problem or is there a technical one? — Christoph Wintersteiger
The problem is my variables are of set type which are in turn implemented as arrays in Z3. When I want to add the negation of a model, I iterate through the declarations/interpretations. When the declaration's range sort is Z3_ARRAY_SORT I try to add the constraint "at least one of the function values must be different" by disjunctions of inequalities on array elements. However since I have (declare-fun k!2 (rSet) Bool) and (declare-fun rID () (Array rSet Bool)) I fail to produce the negations. Could you perhaps provide an example of next-sat for formulas with sets or arrays? — fturkmen
Hi, I think I solved the problem by just adding a constraint on the function values (of array interpretation) rather than the (set) variable itself. — fturkmen

Christoph Wintersteiger Christoph Wintersteiger · Accepted Answer · 2014-05-19T13:34:02

I suspect one of the problems here is that it's not obvious how to get the model for an array. This question has been answered before, so for that part I refer to the previous answer: Read func interp of a z3 array from the z3 model

For the particular example given here, we can do something along these lines:

while (s.check() == Status.SATISFIABLE) {
  Model m = s.getModel();
  FuncDecl const_decls [] = m.getConstDecls();
  BoolExpr ncs = ctx.mkFalse();
  for (int i = 0; i < m.getNumConsts(); i++) {
    FuncDecl fd = const_decls[i];                                       
    if (fd.getRange().getSortKind()==Z3_sort_kind.Z3_ARRAY_SORT) {
      FuncInterp fi = m.getFuncInterp(const_decls[i]);
      Entry [] entries = fi.getEntries();
      BoolExpr [] new_es = new BoolExpr[fi.getNumEntries()];
      for (int j = 0; j < fi.getNumEntries(); j++) {
        Expr as = entries[j].getArgs()[0];
        if (entries[j].getValue().isTrue())
          new_es[j] = ctx.mkNot((BoolExpr) ctx.mkSetMembership(as, rID));
        else
          new_es[j] = (BoolExpr) ctx.mkSetMembership(as, rID);
      }
      BoolExpr nc = (new_es.length == 1) ? new_es[0] : ctx.mkOr(new_es);                        
      ncs = ctx.mkOr(nc, ncs);
    } else if (fd.getArity() == 0) {
      Expr cnst = ctx.mkApp(fd);                    
      Expr mv = m.getConstInterp(const_decls[i]);                    
      BoolExpr nc = ctx.mkNot(ctx.mkEq(cnst, mv));                        
      ncs = ctx.mkOr(nc, ncs);
    }                    
  }
  s.add(ncs);
}

This piece of code just checks whether the range of fd is an array sort, and then assumes that it is the model of a set, which wouldn't work if the constraints mix arrays and sets. In those cases we would need to check whether one particular array models a set or an actual array.

Z3 Enumerating all satisfying assignments

1 Answers