在C/C++中遍历Z3_ast树

Question

简而言之,我需要能够遍历Z3_ast树并访问与其节点相关的数据.似乎无法找到有关如何做到这一点的任何文档/示例.任何指针都会有所帮助.

最后,我需要将smt2lib类型的公式解析为Z3,将一些变量变为常量替换,然后在数据结构中重现公式,该数据结构与另一个不相关的SMT sovler兼容(具体来说,我不认为有关misral的详细信息)对于这个问题很重要但有趣的是它没有命令行界面,我可以在其中提供文本公式.它只有一个C API).我已经想过要以mistral的格式生成公式,我需要遍历Z3_ast树并以所需的格式重建公式.我似乎无法找到任何演示如何执行此操作的文档/示例.任何指针都会有所帮助.

Answer 1

考虑使用定义的C++辅助类z3++.h.Z3发行版还包括使用这些类的示例.这是一个遍历Z3表达式的小代码片段.如果您的公式不包含量词,那么您甚至不需要处理is_quantifier()和is_var()分支.

void visit(expr const & e) {
    if (e.is_app()) {
        unsigned num = e.num_args();
        for (unsigned i = 0; i < num; i++) {
            visit(e.arg(i));
        }
        // do something
        // Example: print the visited expression
        func_decl f = e.decl();
        std::cout << "application of " << f.name() << ": " << e << "\n";
    }
    else if (e.is_quantifier()) {
        visit(e.body());
        // do something
    }
    else { 
        assert(e.is_var());
        // do something
    }
}

void tst_visit() {
    std::cout << "visit example\n";
    context c;

    expr x = c.int_const("x");
    expr y = c.int_const("y");
    expr z = c.int_const("z");
    expr f = x*x - y*y >= 0;

    visit(f);
}