2

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.

Community
  • 1
  • 1
fturkmen
  • 324
  • 3
  • 11
  • 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 May 16 '14 at 17:17
  • 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 May 18 '14 at 13:44
  • 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 May 19 '14 at 12:45

1 Answers1

1

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.

Community
  • 1
  • 1
Christoph Wintersteiger
  • 8,234
  • 1
  • 16
  • 30
  • Thanks a lot for the reply. I think the method getConstDecls() should have been getFuncDecls() or getDecls() to get function declarations, right? I noticed that you negate the original predicate (i.e. membership), I do something like this: ctx.mkNot((BoolExpr)decls[i].apply(fi.getEntries()[j].getArgs())). Perhaps I am doing something wrong? – fturkmen May 19 '14 at 14:01
  • getConstDecls() is right here (rID is treated as a constant of array sort, but because it's an array it's a constant with a FuncInterp model). Your negated expression doesn't provide the right inputs to decls[i] (which here is rID). It's a function of type (Array res bool), so it needs more than just getEntries[j].getArgs(), but adding the rest would essentially create the same expression as my mkSetMembership I think. – Christoph Wintersteiger May 19 '14 at 15:08
  • I see but then I can't come up with a modular enumeration method as I need to know which (negated) expression to add every time. That also means I have to carry all (raw) expressions added to the solver wherever the solve() method is called. For instance, I am not sure if adding the negation of membership predicate would work as we want if there are two such set variables with membership predicates. – fturkmen May 19 '14 at 15:19
  • Sorry, I don't understand. You need to add _all_ expressions, every time. I.e., there will be a big constraint that says at least one of all the function values currently in the model must be different. In the case of sets, this means that at least one of the elements currently in the set must now be not in the set, or, for each element currently not in the set, it must now be in the set. – Christoph Wintersteiger May 19 '14 at 16:41
  • Alternatively, its also possible to set up a new set which has exactly the elements that are listed in the model, and then assert that the set-difference between this and the old set is non-empty. Not sure this would be more efficient though. – Christoph Wintersteiger May 19 '14 at 16:46
  • Sorry, I was not clear.There were two issues:1.In my view, the (set) variables and the expressions (e.g. membership) they are involved in are defined/added to solver in one place and the s.solve() is called in another. In this setting I call the variables and the relevant expressions as raw expressions, e.g. rID is a raw variable.In the place where s.solve() is called I should be able to get (I think) variable declarations/interpretations from the model itself so that I can add their negations.If we call your piece of code as getModels() method, for instance, then rID should be opaque to it. – fturkmen May 19 '14 at 17:23
  • 2.Following the first issue, how do I choose to add the constraint in your example: "ctx.mkNot((BoolExpr) ctx.mkSetMembership(as, rID));" if I have other expressions (e.g. x + y < 10) or similar variables/expressions (e.g. rID2 and membership)? What I mean is I guess is there an automated way of adding those constraints at least for the case LIA and arrays? – fturkmen May 19 '14 at 17:35
  • Ah, I see! Yes I was lazy about that part. You can get the right funcdecl like this: Expr set_const = ctx.mkApp(fd); – Christoph Wintersteiger May 20 '14 at 14:30
  • Since set variables are represented by arrays, I don't think there's a good way of deciding which of them is a set and which of them is a different array. Perhaps you could try to identify them by the signature, which is (Array res Bool) in this example. Essentially every array that has a Bool value type could be treated as a set. – Christoph Wintersteiger May 20 '14 at 14:33