在Z3中调用一些策略后如何使用枚举常量？

Question

这里是我的枚举类型测试程序的源代码：

    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:(和 (= x a) (= x b))

(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) 不起作用。

Answer 1

正如 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 在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;

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

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

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

Answer 2

(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");

看看有没有帮助