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:(and (= xa) (= xb))

(declare-fun a () enumT)

(declare-fun b () enumT)

(declare-fun x() enumT) 这里我期待“c”，为什么是“x”？

2：假

(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

正如 Nikolaj 所指出的，你有一个错字。更重要的是，您正在滥用 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_decls的引用计数器。否则，这些对象将被 Z3 垃圾回收。这发生在您的示例中。这就是为什么你会得到奇怪的结果。如果我们在您的示例中运行诸如Valgrind之类的工具，它将报告许多内存访问冲突。enum_namesenum_consts

这是您的示例的固定版本：

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;

请注意，我将值包装在enum_consts使用func_declC++ 对象中。这些对象本质上是智能指针。他们自动为我们管理引用计数器。

我还使用一种方法扩展了 C++ API，以简化枚举排序的创建。 http://z3.codeplex.com/SourceControl/changeset/b2810592e6bb

我还提供了一个示例，展示了如何使用这个新的 API。此扩展将在下一个版本 (Z3 v4.3.2) 中可用。它已经在不稳定（工作中）分支中可用，明天也将在nightly builds中可用。

于 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 回答