z3 извлекает Seq Int как std :: vector <int> - PullRequest
Новая
       54

z3 извлекает Seq Int как std :: vector <int>

0 голосов
/ 28 мая 2020

Я пытаюсь извлечь Seq Int из model в std::vector<int>. Я могу распечатать его с помощью <<, но как мне выполнить извлечение? 

void oren_example()
{
    // context + solver
    context ctx;
    solver solver(ctx);

    // sorts
    sort int_sort     = ctx.int_sort();
    sort seq_int_sort = ctx.seq_sort(int_sort);
    sort bool_sort    = ctx.bool_sort();

    // constants
    expr two   = ctx.int_val(2);
    expr five  = ctx.int_val(5);
    expr four  = ctx.int_val(4);
    expr three = ctx.int_val(3);

    // define State sort
    const char *names[4]={"x","A","b","n"};
    sort sorts[4]={int_sort,seq_int_sort,bool_sort,int_sort};
    func_decl_vector projs(ctx);
    sort state_sort = ctx.tuple_sort("State",4,names,sorts,projs).range();

    // define an arbitrary state sigma
    expr sigma = ctx.constant("sigma",state_sort);

    // define some predicate on the state
    func_decl init = function("init",state_sort,bool_sort);
    solver.add(forall(sigma,
        init(sigma) == (
            ((projs[0](sigma))          == two  ) &&
            ((projs[1](sigma).length()) == three) &&
            ((projs[1](sigma).nth(two)) == five ) &&
            ((projs[3](sigma))          == five ))));

    // find an initial state
    solver.add(init(sigma));

    // check sat + get model
    if (solver.check() == sat)
    {
        model m = solver.get_model();
        std::cout << "x = " << m.eval(projs[0](sigma)) << "\n";
        std::cout << "A = " << m.eval(projs[1](sigma)) << "\n";
        std::cout << "b = " << m.eval(projs[2](sigma)) << "\n";
        std::cout << "n = " << m.eval(projs[3](sigma)) << "\n";
    }
}

Все распечатано должным образом: 

x = 2
A = (seq.++ (seq.unit 6) (seq.unit 7) (seq.unit 5))
b = false
n = 5

1 Ответ

1 голос
/ 28 мая 2020

Попробуйте: 

        std::vector<int> output;
        int size = m.eval(projs[1](sigma).length()).get_numeral_int();
        std::cout << "size = " << size << std::endl;
        for(int i = 0; i < size; ++i)
            output.push_back(m.eval(projs[1](sigma).nth(ctx.int_val(i))).get_numeral_int());
        for(int i = 0; i < size; ++i)
            std::cout << "output[" << i << "] = " << output[i] << std::endl;

Когда я добавляю это в вашу программу и запускаю, я получаю: 

x = 2
A = (seq.++ (seq.unit 4) (seq.unit 6) (seq.unit 5))
b = false
n = 5
size = 3
output[0] = 4
output[1] = 6
output[2] = 5
...