使用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); 
}