Z3：如何使用C ++代码获得所有可能的解决方案？

Question

这是我为获得所有可能的解决方案而编写的示例代码。

#include"z3++.h"

using namespace z3;
using namespace std;

int main() {

    context c;
    expr X = c.int_const("x");
    expr Y = c.int_const("y");
    expr Z = c.int_const("z");

    solver s(c);
    s.add(X == Y + Z);
    s.add((X > 0) && (Y > 0) && (Z > 0));
    s.add(X <= 10);


    int j = 1;
    while (s.check() == sat)
    {
        model m = s.get_model();

        cout << "solution " << j << " :" << endl;
        for (int i = 0; i < m.size(); i++)
        {
            func_decl f1 = m[i];
            cout << f1.name() << " = " << m.get_const_interp(f1) << endl;
        }
        j++;

        s.add((Y != m.get_const_interp(m[1])) || (Z != m.get_const_interp(m[0])) || (X != m.get_const_interp(m[2])));
    }
}

最初借助打印语句，我能够确定可以使用2,1,0索引访问X，Y，Z值。还有其他方法可以使用，无需担心变量及其索引吗？

(Z3Py) checking all solutions for equation在此链接中，还有另一种使用python API的方法。如何使用C ++实现上述python逻辑？

Answer 1

而不是引用索引，您应该使用表达式向量，并通过遍历变量来添加阻塞子句。这样的事情应该起作用：

#include"z3++.h"

using namespace z3;
using namespace std;

int main() {

    context c;
    expr X = c.int_const("x");
    expr Y = c.int_const("y");
    expr Z = c.int_const("z");

    solver s(c);
    s.add(X == Y + Z);
    s.add((X > 0) && (Y > 0) && (Z > 0));
    s.add(X <= 10);

    expr_vector myVars(c);
    myVars.push_back(X);
    myVars.push_back(Y);
    myVars.push_back(Z);

    int j = 1;
    while (s.check() == sat)
    {
        model m = s.get_model();
        expr_vector blocker(c);

        cout << "solution " << j << " :" << endl;
        for(expr v : myVars)
        {
            cout << v << " = " << m.eval(v) << endl;
            blocker.push_back(v != m.eval(v));
        }
        j++;

        s.add(mk_or(blocker));
    }
}

假设您将其放在名为a.cpp的文件中，请像这样编译：

$ g++ -std=c++11 a.cpp -lz3

我将忽略输出，但是当我运行生成的可执行文件时，它将打印45种不同的解决方案，这些解决方案与您的原始输出匹配。