如何在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：（和（= XA）（= XB））

（声明芬一（）enumT）

（声明乐趣b（）enumT）

（声明乐趣X（）enumT）这里我预期的 “C”，为什么 “X”？

2：假

（声明-乐趣（）enumT）

（声明乐趣BV（）（_ BitVec 1））为什么不 “B”？

（声明乐趣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

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

，并看看是否有帮助

Answer 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 S的引用计数器在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中提供。