Z3: Как получить доступ к переменным из модели () без использования жестко закодированного индекса? - PullRequest
Новая
       6

Z3: Как получить доступ к переменным из модели () без использования жестко закодированного индекса?

1 голос
/ 26 марта 2020

Вот пример кода, который я написал, чтобы получить все возможные решения. 

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

Первоначально с помощью операторов печати я смог выяснить, что значения X, Y, Z могут быть доступны с помощью 2 , 1,0 индекс из модели ().

Есть ли другой способ сделать это, где мне не нужен жестко закодированный индекс?

1 Ответ

2 голосов
/ 26 марта 2020

Вместо того, чтобы ссылаться на индексы, вы должны вместо этого использовать вектор выражения и добавить предложение блокировки, перебирая переменные. Примерно так должно работать: 

#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 различных решений, что соответствует вашему исходному выводу.

...