如何在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中提供。