10

つまり、Z3_astツリーをトラバースして、そのノードに関連付けられているデータにアクセスできる必要があります。その方法に関するドキュメント/例が見つからないようです。任意のポインタが役立ちます。

長い間、smt2libタイプの数式をZ3に解析し、定数置換に変数を作成してから、別の無関係なSMTソブラーと互換性のあるデータ構造で数式を再現する必要があります（具体的にはミストラル、ミストラルについての詳細は考えていません）この質問にとって重要ですが、おかしなことに、テキスト式を入力できるコマンドラインインターフェイスがありません。CAPIがあるだけです）。ミストラルの形式で式を生成するには、Z3_astツリーをトラバースして、目的の形式で式を再構築する必要があると考えました。これを行う方法を示すドキュメント/例が見つからないようです。任意のポインタが役立ちます。

4

1 に答える 1

6

で定義されている 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);
}
于 2012-09-19T20:02:41.307 に答える