2

列挙型のテストプログラムのソースコードは次のとおりです。

    Z3_symbol enum_names[3];
    Z3_func_decl enum_consts[3];
    Z3_func_decl enum_testers[3];
    enum_names[0]=Z3_mk_string_symbol(z3_cont,"a");
    enum_names[1]=Z3_mk_string_symbol(z3_cont,"b");
    enum_names[3]=Z3_mk_string_symbol(z3_cont,"c");
    Z3_symbol enum_nm = Z3_mk_string_symbol(z3_cont,"enumT");
    Z3_sort s = Z3_mk_enumeration_sort(z3_cont, enum_nm, 3, enum_names, enum_consts, enum_testers);
    z3::sort ss(z3_cont,s);
    z3::expr a = z3::expr(z3_cont,Z3_mk_app(z3_cont,enum_consts[0],0,0));
    z3::expr b = z3::expr(z3_cont,Z3_mk_app(z3_cont,enum_consts[1],0,0));
    z3::expr x =       z3::expr(z3_cont,Z3_mk_const(z3_cont,Z3_mk_string_symbol(z3_cont,"x"),s));
    z3::expr test = (x==a)&&(x==b);
    cout<<"1:"<<test<<endl;

    printf("%s\n", Z3_func_decl_to_string(z3_cont, enum_consts[0]));
    printf("%s\n", Z3_func_decl_to_string(z3_cont, enum_consts[1]));
    printf("%s\n", Z3_func_decl_to_string(z3_cont, enum_consts[2]));

    z3::tactic qe(z3_cont,"ctx-solver-simplify");
    z3::goal g(z3_cont);
    g.add(test);
    z3::expr res(z3_cont);
    z3::apply_result result_of_elimination = qe.apply(g);
    if ( result_of_elimination.size() == 1){
         z3::goal result_formula = result_of_elimination[0];
         res =  result_formula.operator[](0);
         for (int i = 1; i < result_formula.size(); ++i){
                  res = res && result_formula.operator[](i);
         }
    }
    cout<<"2:"<<res<<endl;

    printf("%s\n", Z3_func_decl_to_string(z3_cont, enum_consts[0]));
    printf("%s\n", Z3_func_decl_to_string(z3_cont, enum_consts[1]));
    printf("%s\n", Z3_func_decl_to_string(z3_cont, enum_consts[2]));

画面出力は次のとおりです：1 :(および（= xa）（= xb））

（declare-fun a（）enumT）

（declare-fun b（）enumT）

（declare-fun x（）enumT） ここで私は「c」を期待していましたが、なぜ「x」なのですか？

2：false

（declare-fun a（）enumT）

（declare-fun bv（）（_ BitVec 1）） なぜ「b」ではないのですか？

（declare-fun x（）enumT）

主な質問は、いくつかの戦術を呼び出した後、プログラムで列挙型定数をどのように使用する必要があるかです。

enum_consts構造が壊れているため、Z3_mk_app（z3_cont、Z3_mk_func_decl（z3_cont、Z3_mk_string_symbol（z3_cont、 "a"）、0,0、s）、0,0）が機能しません。

4

2 に答える 2

2

ニコライが指摘したように、タイプミスがあります。さらに重要なのは、C/C++ API を誤用しているということです。両方の API を同時に使用することができます。ただし、C API を使用する場合は、参照カウンターを手動でインクリメントするか、C++ API で使用可能な C++ ラッパーを使用して Z3_ast 値をラップする必要があります。そうしないと、メモリが破損します。たとえば、呼び出すとき

Z3_sort s = Z3_mk_enumeration_sort(z3_cont, enum_nm, 3, enum_names, enum_consts, enum_testers);

と の の参照カウンタを増やす必要がZ3_func_declありenum_namesますenum_consts。それ以外の場合、これらのオブジェクトは Z3 によってガベージ コレクションされます。これはあなたの例で起こります。そのため、奇妙な結果が得られます。この例でValgrindなどのツールを実行すると、多くのメモリ アクセス違反が報告されます。

あなたの例の修正版は次のとおりです。

using namespace z3;
...
context z3_cont;
...

Z3_symbol enum_names[3];
Z3_func_decl enum_consts[3];
Z3_func_decl enum_testers[3];
enum_names[0]=Z3_mk_string_symbol(z3_cont,"a");
enum_names[1]=Z3_mk_string_symbol(z3_cont,"b");
enum_names[2]=Z3_mk_string_symbol(z3_cont,"c");
Z3_symbol enum_nm = Z3_mk_string_symbol(z3_cont,"enumT");
sort s = to_sort(z3_cont, Z3_mk_enumeration_sort(z3_cont, enum_nm, 3, enum_names, enum_consts, enum_testers));
func_decl a_decl = to_func_decl(z3_cont, enum_consts[0]);
func_decl b_decl = to_func_decl(z3_cont, enum_consts[1]);
func_decl c_decl = to_func_decl(z3_cont, enum_consts[2]);
expr a = to_expr(z3_cont, Z3_mk_app(z3_cont, a_decl, 0, 0));
expr b = to_expr(z3_cont, Z3_mk_app(z3_cont, b_decl, 0, 0));
expr x = z3_cont.constant("x", s);
expr test = (x==a) && (x==b);
std::cout << "1: " << test << std::endl;

tactic qe(z3_cont,"ctx-solver-simplify");
goal g(z3_cont);
g.add(test);
expr res(z3_cont);
apply_result result_of_elimination = qe.apply(g);
if ( result_of_elimination.size() == 1){
    goal result_formula = result_of_elimination[0];
    res =  result_formula.operator[](0);
    for (int i = 1; i < result_formula.size(); ++i){
        res = res && result_formula.operator[](i);
    }
}
std::cout << "2: " << res << std::endl;

C++ オブジェクトenum_constsを使用して値をラップしていることに注意してください。func_declこれらのオブジェクトは本質的にスマート ポインターです。彼らは私たちのために参照カウンターを自動的に管理します。

また、列挙ソートの作成を簡素化するメソッドを使用して C++ API を拡張しました。 http://z3.codeplex.com/SourceControl/changeset/b2810592e6bb

この新しい API の使用方法を示す例も含めました。この拡張機能は、次のリリース (Z3 v4.3.2) で利用できるようになります。不安定な (進行中の) ブランチで既に利用可能であり、ナイトリー ビルドでも明日利用可能になります。

于 2013-02-26T16:40:32.460 に答える
1

(declare-fun x () enumT) ここでは "c" を期待していますが、なぜ "x" なのですか?

変更してみてください:

enum_names[0]=Z3_mk_string_symbol(z3_cont,"a");
enum_names[1]=Z3_mk_string_symbol(z3_cont,"b");
enum_names[3]=Z3_mk_string_symbol(z3_cont,"c");

に：

enum_names[0]=Z3_mk_string_symbol(z3_cont,"a");
enum_names[1]=Z3_mk_string_symbol(z3_cont,"b");
enum_names[2]=Z3_mk_string_symbol(z3_cont,"c");

そして、それが役立つかどうかを確認してください

于 2013-02-26T15:55:32.173 に答える