Defining a Theory of Sets with Z3 using C++

Question

I need to implement theory of Sets with Z3 using C++ and the system is supposed to work like this: 1. Building the constraint system that supports common set operations using C++;

2. Adding additional constraints in smtlib2 format and here I am using this API in C to convert a string into expr: Z3_parse_smtlib2_string

For the Set theory, I started with the original answer from Leonardo in this post: Defining a Theory of Sets with Z3/SMT-LIB2

I tried the encoding in http://rise4fun.com/Z3/DWYC and everything works fine in rise4fun. However, I run into some troubles in translating the encoding into C++ code and I couldn't find any set API in Z3 for C++. Is there any example?

Then I found that z3_api.h contains the set API for c. So I wrote a very simple code snippet and it seems to work:

//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);

If I initialize Z3_context object using z3::context, the code will raise a "Segmentation fault" error while invoking "Z3_mk_set_intersect".

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

I want to perform some set operations on string elements and I don't know how to integrate it into my C++ code since I also created my own z3:context in C++. How can I directly perform set operations in C++?

Thanks,

Answer 1

Sorry for not exposing set operations for the C++ API. The problem is that expressions need to be reference counted properly. When using the Z3_... methods, the caller is responsible for taking care of this. The C++ wrappers automatically handle the reference counting. For now you can create an ad-hoc extension of the C++ API to include set intersection by creating your own method:

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

The constructor for the "expr" class takes a reference count on 'r'. This ensures that the pointer to 'r' remains valid as long as the expression is in scope.

I will add set operations to the C++ API to facilitate other uses. Until they are integrated, this is basically what they will look like:

#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);
}