在 C/C++ 中遍历 Z3_ast 树 [英] Traversing Z3_ast tree in C/C++

问题描述

简而言之，我需要能够遍历 Z3_ast 树并访问与其节点关联的数据.似乎无法找到有关如何执行此操作的任何文档/示例.任何指针都会有所帮助.

In short, I need to be able to traverse Z3_ast tree and access the data associated with its nodes. Cannot seem to find any documentation/examples on how to do that. Any pointers would be helpful.

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

At length, I need to parse smt2lib type formulae into Z3, make some variable to constant substitutions and then reproduce the formula in a data structure which is compatible with another unrelated SMT sovler (mistral to be specific, I don't think details about mistral are important to this question but funnily enough it does not have a command line interface where I can feed it text formulae. It just has a C API). I have figured that to generate the formula in mistral's format, I would need to traverse the Z3_ast tree and reconstruct the formula in the desired format. I cannot seem to find any documentation/examples that demonstrate how to do this. Any pointers would be helpful.

推荐答案

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

Consider using the C++ auxiliary classes defined at z3++.h. The Z3 distribution also includes an example using these classes. Here is a small code fragment that traverses a Z3 expression. If your formulas do not contain quantifiers, then you don't even need to handle the is_quantifier() and is_var() branches.

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);
}

这篇关于在 C/C++ 中遍历 Z3_ast 树的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！