总之，我需要能够遍历Z3_ast树并访问其节点相关联的数据。 似乎无法找到如何做到这一点的任何文档/例子。 任何指针将是有益的。
在长度，我需要解析smt2lib类型公式成Z3，使一些变量恒定置换，然后再现该公式中的数据结构是与另一不相关的SMT兼容sovler（米斯特拉尔具体而言，我不认为约米斯特拉尔细节对这个问题很重要，但有趣的是它不会有一个命令行界面，我可以养活它的文本的公式，它只是有一个C API）。 我已经计算过，以产生米斯特拉尔的格式的公式，我需要遍历Z3_ast树和重建公式中所需的格式。 我似乎无法找到任何文档/示例演示如何做到这一点。 任何指针将是有益的。
考虑使用在所定义的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);
}
