C/C++のZ3_astツリーをトラバースする

Question

要するに、私はZ3_astツリーを走査し、そのノードに関連するデータにアクセスできる必要があります。それを行う方法に関するドキュメントや例は見つかりません。任意のポインタが役立つだろう。

長々として、smt2lib型の式をZ3に解析し、一定の変数を定数の代入にして、別の無関係なSMT sovlerと互換性のあるデータ構造で式を再現する必要があります。 mistralについての詳細はこの質問にとって重要だと思うが、面倒なことに、コマンドラインインターフェースを持たないので、テキスト式にフィードを送ることができる.C APIだけである。私はmistralの形式で数式を生成することを考えて、私はZ3_astツリーを横断し、希望の形式で数式を再構築する必要があります。私はどのようにこれを行う方法を示すドキュメント/例を見つけることができないようです。任意のポインタが役立つだろう。

Answer 1

z3++.hで定義されているC++補助クラスの使用を検討してください。 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); 
}