Z3：在 C++ 中找到所有令人满意的模型答案

【问题标题】：Z3: Finding all satisfying models in c++Z3：在 C++ 中找到所有令人满意的模型
【发布时间】：2015-09-14 21:25:33
【问题描述】：

我正在尝试在 c++ 中找到线性系统的所有整数解。但它没有找到所有解决方案（只有一些）。问题出在哪里？

expr mk_and(expr_vector args) {
    vector<Z3_ast> array;

    for (int i = 0; i < args.size(); i++)
      array.push_back(args[i]);

    return to_expr(args.ctx(), Z3_mk_and(args.ctx(), array.size(), &(array[0])));
}

expr mk_or(expr_vector args) {
    vector<Z3_ast> array;

    for (int i = 0; i < args.size(); i++)
      array.push_back(args[i]);

    return to_expr(args.ctx(), Z3_mk_or(args.ctx(), array.size(), &(array[0])));
}

expr mk_add(expr_vector args) {
    vector<Z3_ast> array;

    for (int i = 0; i < args.size(); i++)
      array.push_back(args[i]);

    return to_expr(args.ctx(), Z3_mk_add(args.ctx(), array.size(), &(array[0])));
}

vector<vector<int>> solveLinearEquations(vector<vector<int>> linEquations, vector<int> vect, int from, int to){

    context c;
    const unsigned N = linEquations[0].size();
    expr_vector x(c);
    for (unsigned i = 0; i < N; i++) { 
        std::stringstream x_name; 
        x_name << "x_" << i;
        x.push_back(c.int_const(x_name.str().c_str()));
    }

    solver s(c);

    for (unsigned i = 0; i < N; i++) {
        s.add(x[i] >= from);
        s.add(x[i] <= to);
    }

    for (int i = 0; i < linEquations.size(); i++) {
        expr_vector linVector(c);
        for (int j = 0; j< linEquations[i].size(); j++) {
            if (linEquations[i][j] != 0) {
                linVector.push_back(linEquations[i][j] * x[j]);
            }
        }
        s.add(mk_add(linVector) == vect[i]);
    }

    vector<vector<int> > solutions;

    while(true) {
        if (s.check() == sat) {
            model m = s.get_model();
            expr_vector ve(c);
            vector<int> sol; sol.clear();
            for (unsigned i = 0; i < N; i++) {
                ve.push_back(x[i] != m.eval(x[i]));
                int val;
                Z3_get_numeral_int(c, m.eval(x[i]), &val);
                sol.push_back(val);
            }
            solutions.push_back(sol); 
            expr_vector ve2(c);
            ve2.push_back(mk_and(ve));
            s.add(mk_or(ve2));
        }
        else {
            break; 
        }
    }

    return solutions;
}

例如：linearSystem {{1,1,0,0,0,0}, {0,0,1,1,1,1}, {0,1,0,1,2,3} , {0,3,0,1,4,9}}, vect{3,4,6,12}, from=0, to=3 只找到 2 个解，但有 5 个。有什么想法吗？

【问题讨论】：

标签： z3

【解决方案1】：

ve2.push_back(mk_and(ve)); 是做什么的？删除它。另外，您需要将s.add(mk_or(ve2)); 更改为s.add(mk_or(ve));。

不确定您要在那里构建什么样的表达式。你需要像x0 != 1 || x1 != 7 || ... 这样的东西。

【讨论】：