Как напечатать вывод "bit-blast" для выражения битового вектора в z3 с c ++? - PullRequest
Новая
       103

Как напечатать вывод "bit-blast" для выражения битового вектора в z3 с c ++?

1 голос
/ 26 июня 2019

Я создал функцию, которая преобразует логические формулы предложений в qdimacs. Я хочу преобразовать даже некоторые выражения bit_vector в pl форму, а затем QDIMACS. У меня есть этот метод с именем 'bit-blast' и пример, такой как: 

std::cout << "tactic example 2\n";
    context c;
    expr x = c.real_const("x");
    expr y = c.real_const("y");
    goal g(c);
    g.add(x < 0 || x > 0);
    g.add(x == y + 1);
    g.add(y < 0);
    tactic t(c, "bit-blast");
    apply_result r = t(g);
    for (unsigned i = 0; i < r.size(); i++)
    {
        std::cout << "subgoal " << i << "\n" << r[i] << "\n";
    }

В этом примере они используют "real_const", но мне нужно, чтобы мои выражения были "bv_const". Я попытался выполнить его с помощью bv_const, но он показывает ошибку: Aborted(core dumped)

Я даже пробовал такую ​​программу: 

#include<z3++.h>  
#include<iostream>
using namespace std;
using namespace z3;

int main()
{   context c;
    tactic t = tactic(c, "bit-blast");

    goal g(c);
    expr x = c.bv_const("x", 16);
    expr y = c.bv_const("y", 16);
   expr z = c.bv_const("z", 16);

    g.add(z = x +y);
    apply_result r = t(g);
    for (unsigned i = 0; i < r.size(); i++) {
        std::cout << "subgoal " << i << "\n" << r[i] << "\n";
    }

}

Даже это выдает ту же ошибку: Aborted(core dumped).

Есть ли способ сохранить вывод «bit-blast» в выражении и распечатать его? Есть ли пример программы, которая демонстрирует решение моей проблемы, или вы можете показать мне, как это делается?

Спасибо.

...