Решите для переменных выражения, используя Z3 в C ++ - PullRequest
Новая
       5

Решите для переменных выражения, используя Z3 в C ++

0 голосов
/ 25 марта 2020

Как я могу написать уравнение, например, с 2 выражениями z3 

z3::exp x;
Z3::exp y;

Как получить линейное уравнение в форме z3::exp Z= x+10*y

Как решить для выражения переменная, используя выражения Z3, например, у меня есть следующая система уравнений: 

 x = a+b;
 a = 2*y;
 b = 4*c;

Как я могу получить, что x = 2*y + 4*c, где x, y, b и c все выражения z3

1 Ответ

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

Как-то так должно работать: 

#include "z3++.h"

using namespace z3;

int main(void) {
    context ctx;
    expr x = ctx.int_const("x");
    expr y = ctx.int_const("y");
    expr a = ctx.int_const("a");
    expr b = ctx.int_const("b");
    expr c = ctx.int_const("c");
    solver s(ctx);

    s.add(x == a+b);
    s.add(a == 2*y);
    s.add(b == 4*c);
    s.add(x == 2*y + 4*c);

    std::cout << s.check() << "\n";
    model m = s.get_model();
    for (unsigned i = 0; i < m.size(); i++) {
        func_decl v = m[static_cast<int>(i)];
        std::cout << v.name() << " = " << m.get_const_interp(v) << "\n";
    }
    return 0;
}

Если вы поместите эту программу в файл с именем a.cpp, вы можете скомпилировать и запустить ее так: 

$ c++ a.cpp -lz3
$ ./a.out
sat
y = 0
c = 0
x = 0
b = 0
a = 0

Модель, которую вы получаете, не особенно интересна, потому что все 0 присваивает ее тривиально. Но вы можете добавить другие ограничения и получить более интересные значения.

...