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

Question

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

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

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