Z3_ast 在 C++ 中遍历期间的重写

【问题标题】：rewriting of Z3_ast during its traversing in C++Z3_ast 在 C++ 中遍历期间的重写
【发布时间】：2013-05-22 15:57:20
【问题描述】：

to_expr 函数导致错误。你能告诉我下面有什么问题吗？

context z3_cont;
expr x = z3_cont.int_const("x");
expr y = z3_cont.int_const("y");
expr ge = ((y==3) && (x==2));
ge = swap_tree( ge );

其中swap_tree 是一个交换所有二元运算操作数的函数。定义如下。

expr swap_tree( expr e ) {
  Z3_ast ee[2];
  if ( e.is_app() && e.num_args() == 2) {
    for ( int i = 0; i < 2; ++i ) {
     ee[ 1 - i ] = swap_tree( e.arg(i) );
    }   
    for ( int i = 0; i < 2; ++i ) {
      cout <<" ee[" << i << "] : " << to_expr( z3_cont, ee[ i ] ) << endl;
    }
    return to_expr( z3_cont, Z3_update_term( z3_cont, e, 2, ee ) );
  }
  else 
    return e;
}

【问题讨论】：

标签： z3 abstract-syntax-tree

【解决方案1】：

问题是“引用计数”。如果 Z3 对象的引用计数器为 0，则系统可以对 Z3 对象进行垃圾回收。Z3 C++ API 提供“智能指针”（expr，sort，...）为我们自动管理引用计数器。您的代码使用Z3_ast ee[2]。在 for 循环中，您将 swap_tree(e.arg(0)) 的结果存储到 ee[0] 中。由于引用计数器不递增，因此在执行循环的第二次迭代时，可能会删除此 Z3 对象。

这是一个可能的解决方法：

expr swap_tree( expr e ) {
  if ( e.is_app() && e.num_args() == 2) {
    // using smart-pointers to store the intermediate results.
    expr ee0(z3_cont), ee1(z3_cont);
    ee0 = swap_tree( e.arg(0) );
    ee1 = swap_tree( e.arg(1) );
    Z3_ast ee[2] = { ee1, ee0 };
    return to_expr( z3_cont, Z3_update_term( z3_cont, e, 2, ee ) );
  }
  else {
    return e;
  }
}

【讨论】：