c++ - 如何使用 c++ 在 z3 中的位向量表达式上打印“位爆炸”的输出？

Question

我创建了一个将命题逻辑公式转换为 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”的输出存储在表达式中并打印出来？有没有演示我的问题解决方案的示例程序，或者你能告诉我它是如何完成的吗？

谢谢你。

标签： c++z3smtbitvector