0

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

1 に答える 1

0

問題は「参照カウント」です。Z3 オブジェクトは、その参照カウンターが 0 の場合、システムによってガベージ コレクションされる可能性があります。Z3 C++ API は、参照カウンターを自動的に管理するための「スマート ポインター」( expr、sort、...) を提供します。あなたのコードはZ3_ast ee[2]. for ループでは、の結果をに格納swap_tree(e.arg(0))しee[0]ます。参照カウンタはインクリメントされないため、この Z3 オブジェクトは、ループの 2 回目の繰り返しを実行するときに削除される可能性があります。

可能な修正は次のとおりです。

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;
  }
}
于 2013-05-23T15:09:44.960 に答える