3

可変数の論理和で長い論理和を作成するための好ましい方法は何でしょうか？

私の推測では、このようなことはexpr_vector、最初にすべての論理和を動的にpush_back使用し、次に何らかの方法でZ3_mk_or論理和を構築するために使用することで可能になるはずです。

しかし、3番目の引数として渡すためにZ3_astの配列を取得するにはどうすればよいですか？expr_vectorZ3_mk_or

ところで、単一の長いn-ary論理和ではなく、バイナリ論理和の長いシーケンスを作成する場合、効率の低下はありますか？

4

1 に答える 1

3

expr_vectorZ3 C ++ APIは、オブジェクトからのn-ary論理和の作成をサポートしていません。これが便利な機能であることに同意します。次のZ3リリースで追加する予定です。次のコードを使用して、この機能をシミュレートできます。次のコードは、expr_vectorの「コピー」を作成するため完全ではありませんが、一時的な回避策として使用できます。上で述べたように、次のバージョンにはこの種の操作のサポートが組み込まれ、コピーは回避されます。

#include<vector>
#include<z3++.h>
using namespace z3;

expr mk_or(expr_vector args) {
    std::vector<Z3_ast> array;
    for (unsigned i = 0; i < args.size(); i++) 
        array.push_back(args[i]);
    return to_expr(args.ctx(), Z3_mk_or(args.ctx(), array.size(), &(array[0])));
}

int main() {
    context      c;
    expr_vector  args(c);

    args.push_back(c.bool_const("p"));
    args.push_back(c.bool_const("q"));
    args.push_back(c.bool_const("r"));

    std::cout << mk_or(args) << std::endl;
    return 0;
}

2番目の質問に関しては、単一のn-ary分離ではなく、長いシーケンスのバイナリ分離を作成しても、パフォーマンスが大幅に低下することはありません。内部的には、Z3はバイナリ形式とn-ary形式の間で非常に効率的に変換できます。

于 2012-05-30T20:35:03.290 に答える