Z3列举所有令人满意的作业 [英] Z3 Enumerating all satisfying assignments

问题描述

我正在尝试解决与此处类似的问题（ Z3：找到所有令人满意的模型），我需要找到包含设置变量的SMT公式的所有令人满意的赋值。我理解链接中的想法，因为它类似于某些SAT求解器迭代解决方案的方式：添加对解决方案的求反以获得不同的解决方案。但是，当我使用set变量（在Z3中作为数组实现）时，情况变得有些复杂，或者我可能会错过一些东西。假设我向求解器添加了两个约束，如下所示：

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

现在我想在Z3中找到我的公式的所有令人满意的赋值。从理论上讲，我将在迭代过程中使用一个if块来添加变量与其当前值之间的不等式，并一直持续到UNSAT：

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 
    }

但是我不能使它起作用，因为我不能为变量构造取反子公式。是否有简单的方法可以枚举与Z3中的SMT公式相似的所有令人满意的赋值？

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?

我意识到这里的帖子（（Z3Py）检查所有方程式的解决方案）不包括在枚举中使用数组和未解释的函数。我不确定这个问题主要是与实施相关还是更根本的问题。

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.

推荐答案

我怀疑这里的问题之一是如何为数组获取模型并不明显。之前已经回答了这个问题，所以对于那部分，我指的是之前的答案：从z3模型中读取z3数组的函数插值

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

这段代码只是检查的范围fd 是一个数组排序，然后假定它是一个集合的模型，如果约束混合了数组和集合，则该模型将不起作用。在这种情况下，我们将需要检查一个特定的数组是对一组还是实际的数组进行建模。

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列举所有令人满意的作业的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！