使用C++定義Z3的集合理論

Question

我需要使用C++來實現Z3集合的理論，系統應該像這樣工作： 1.構建支持使用C++的通用集合操作的約束系統;

添加在smtlib2格式附加約束，在這裏我使用 在C這個API將字符串轉換成EXPR：Z3_parse_smtlib2_string

對於集理論，我開始與萊昂納多在這篇文章中的原始答案： Defining a Theory of Sets with Z3/SMT-LIB2

我試過編碼在http://rise4fun.com/Z3/DWYC和一切工作正常rise4fun。但是，我將編碼轉換爲C++代碼時遇到了一些麻煩，我無法在Z3中爲C++找到任何設置的API。 有沒有例子？

然後我發現z3_api.h包含c的set API。所以我寫了一個非常簡單的代碼片段，它似乎工作：

//https://github.com/Z3Prover/z3/blob/master/examples/c/test_capi.c#L105 
Z3_context c = mk_context(); 
Z3_solver s = mk_solver(c); 
Z3_sort ty = Z3_mk_int_sort(c); 
Z3_ast emp = Z3_mk_empty_set(c, ty); 
Z3_ast s1 = Z3_mk_empty_set(c, ty); 
Z3_ast s2 = Z3_mk_empty_set(c, ty); 
Z3_ast one = Z3_mk_int(c, 1, ty); 
Z3_ast two = Z3_mk_int(c, 2, ty); 
Z3_ast three = Z3_mk_int(c, 3, ty); 

s1 = Z3_mk_set_add(c, s1, one); 
s1 = Z3_mk_set_add(c, s1, two); 
s2 = Z3_mk_set_add(c, s2, three); 

Z3_ast intersect_array[2]; 
intersect_array[0] = s1; 
intersect_array[1] = s2; 
Z3_ast s3 = Z3_mk_set_intersect(c, 2, intersect_array); 
Z3_ast assert1 = Z3_mk_eq(c, s3, emp); 
Z3_solver_assert(c, s,assert1); 
check(c, s, Z3_L_TRUE); 

如果我使用Z3 ::上下文初始化Z3_context對象，而調用「Z3_mk_set_intersect」的代碼將拋出一個「分段故障」錯誤。

context ctx; 
Z3_context c = ctx.operator _Z3_context *(); 

我想對字符串元素執行一些操作集，我不知道如何將它融入我的C++代碼，因爲我還創建了自己的Z3：用C++方面。我如何直接在C++中執行set操作？

謝謝，

Answer 1

抱歉不公開C++ API的設置操作。 問題是表達式需要適當的引用計數。 當使用Z3 _...方法時，調用者負責處理這個問題。 C++包裝器自動處理引用計數。 現在可以創建C++ API的一個特設的擴展創建自己的方法，包括設置路口：

inline expr set_intersect(expr const& a, expr const& b) { 
    check_context(a, b); 
    Z3_ast es[2] = { a, b }; 
    Z3_ast r = Z3_mk_set_intersect(a.ctx(), 2, es); 
    a.check_error();      
    return expr(a.ctx(), r); 
} 

爲「EXPR」類的構造函數的「R」的引用計數。這確保只要表達式在範圍內，指向'r'的指針仍然有效。

我會將設置操作添加到C++ API以便於其他用途。 直到它們被整合，這基本上是他們的樣子：

#define MK_EXPR1(_fn, _arg)      \ 
    Z3_ast r = _fn(_arg.ctx(), _arg);   \ 
    _arg.check_error();       \ 
    return expr(_arg.ctx(), r); 

#define MK_EXPR2(_fn, _arg1, _arg2)    \ 
    check_context(_arg1, _arg2);    \ 
    Z3_ast r = _fn(_arg1.ctx(), _arg1, _arg2); \ 
    _arg1.check_error();      \ 
    return expr(_arg1.ctx(), r); 

inline expr empty_set(sort const& s) { 
    MK_EXPR1(Z3_mk_empty_set, s); 
} 

inline expr full_set(sort const& s) { 
    MK_EXPR1(Z3_mk_full_set, s); 
} 

inline expr set_add(expr const& s, expr const& e) { 
    MK_EXPR2(Z3_mk_set_add, s, e); 
} 

inline expr set_del(expr const& s, expr const& e) { 
    MK_EXPR2(Z3_mk_set_del, s, e); 
}  

inline expr set_union(expr const& a, expr const& b) { 
    check_context(a, b); 
    Z3_ast es[2] = { a, b }; 
    Z3_ast r = Z3_mk_set_union(a.ctx(), 2, es); 
    a.check_error();      
    return expr(a.ctx(), r); 
} 

inline expr set_intersect(expr const& a, expr const& b) { 
    check_context(a, b); 
    Z3_ast es[2] = { a, b }; 
    Z3_ast r = Z3_mk_set_intersect(a.ctx(), 2, es); 
    a.check_error();      
    return expr(a.ctx(), r); 
} 

inline expr set_difference(expr const& a, expr const& b) { 
    MK_EXPR2(Z3_mk_set_difference, a, b); 
} 

inline expr set_complement(expr const& a) { 
    MK_EXPR1(Z3_mk_set_complement, a); 
} 

inline expr set_member(expr const& s, expr const& e) { 
    MK_EXPR2(Z3_mk_set_member, s, e); 
} 

inline expr set_subset(expr const& a, expr const& b) { 
    MK_EXPR2(Z3_mk_set_subset, a, b); 
}