c++ - Z3:如何在不使用硬编码索引的情况下从model()访问变量？

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

最初，借助打印语句，我能够确定可以使用来自model()的2,1,0索引来访问X，Y，Z值。

还有其他不需要硬编码索引的方式吗？

Answer 1

与其引用索引，不如使用表达式 vector 并通过遍历变量来添加阻塞子句。这样的事情应该起作用:

#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种不同的解决方案，这些解决方案与您的原始输出匹配。