add API and example for one dimensional algebraic datatype #6179

examples/c++/example.cpp

@@ -956,6 +956,27 @@ void tuple_example() {
     std::cout << pair2 << "\n";
 }
 
+void datatype_example() {
+    std::cout << "datatype example\n";
+    context ctx;
+    constructors cs(ctx);
+    symbol ilist = ctx.str_symbol("ilist");
+    symbol accs[2] = { ctx.str_symbol("hd"), ctx.str_symbol("tl") };
+    sort sorts[2] = { ctx.int_sort(), ctx.datatype_sort(ilist) };
+    cs.add(ctx.str_symbol("nil"), ctx.str_symbol("is-nil"), 0, nullptr, nullptr);
+    cs.add(ctx.str_symbol("cons"), ctx.str_symbol("is-cons"), 2, accs, sorts);
+    sort ls = ctx.datatype(ilist, cs);
+    std::cout << ls << "\n";
+    func_decl nil(ctx), is_nil(ctx);
+    func_decl_vector nil_acc(ctx);
+    cs.query(0, nil, is_nil, nil_acc);
+    func_decl cons(ctx), is_cons(ctx);
+    func_decl_vector cons_acc(ctx);
+    cs.query(1, cons, is_cons, cons_acc);
+    std::cout << nil << " " << is_nil << " " << nil_acc << "\n";
+    std::cout << cons << " " << is_cons << " " << cons_acc << "\n";
+}
+
 void expr_vector_example() {
     std::cout << "expr_vector example\n";
     context c;
@@ -1307,7 +1328,7 @@ void iterate_args() {
 
 int main() {
 
-    try {
+    try {        
         demorgan(); std::cout << "\n";
         find_model_example1(); std::cout << "\n";
         prove_example1(); std::cout << "\n";
@@ -1343,6 +1364,7 @@ int main() {
         incremental_example3(); std::cout << "\n";
         enum_sort_example(); std::cout << "\n";
         tuple_example(); std::cout << "\n";
+        datatype_example(); std::cout << "\n";
         expr_vector_example(); std::cout << "\n";
         exists_expr_vector_example(); std::cout << "\n";
         substitute_example(); std::cout << "\n";

src/api/c++/z3++.h

@@ -57,6 +57,8 @@ namespace z3 {
     class param_descrs;
     class ast;
     class sort;
+    class constructors;
+    class constructor_list;
     class func_decl;
     class expr;
     class solver;
@@ -313,6 +315,24 @@ namespace z3 {
         */
         func_decl tuple_sort(char const * name, unsigned n, char const * const * names, sort const* sorts, func_decl_vector & projs);
 
+
+        /**
+           \brief Create a recursive datatype over a single sort.
+           \c name is the name of the recursive datatype
+           \c n - the numer of constructors of the datatype
+           \c cs - the \c n constructors used to define the datatype
+
+           References to the datatype can be created using \ref datatype_sort.
+         */
+        sort datatype(symbol const& name, constructors const& cs);
+
+        /**
+           \brief a reference to a recursively defined datatype.
+           Expect that it gets defined as a \ref datatype.
+        */
+        sort datatype_sort(symbol const& name);
+
+
         /**
            \brief create an uninterpreted sort with the name given by the string or symbol.
          */
@@ -3330,6 +3350,80 @@ namespace z3 {
         return func_decl(*this, tuple);
     }
 
+    class constructor_list {
+        context& ctx;
+        Z3_constructor_list clist;
+    public:
+        constructor_list(context& ctx, unsigned n, Z3_constructor const* cons): ctx(ctx) {
+            clist = Z3_mk_constructor_list(ctx, n, cons);
+        }
+        ~constructor_list() {
+            Z3_del_constructor_list(ctx, clist);
+        }
+    };
+
+    class constructors {
+        context&       ctx;
+        std::vector<Z3_constructor> cons;
+        std::vector<unsigned> num_fields;
+    public:
+        constructors(context& ctx): ctx(ctx) {}
+
+        ~constructors() {
+            for (auto con : cons)
+                Z3_del_constructor(ctx, con);           
+        }
+
+        void add(symbol const& name, symbol const& rec, unsigned n, symbol const* names, sort const* fields) {
+            array<unsigned> sort_refs(n);
+            array<Z3_sort> sorts(n);
+            array<Z3_symbol> _names(n);            
+            for (unsigned i = 0; i < n; ++i) sorts[i] = fields[i], _names[i] = names[i];
+            cons.push_back(Z3_mk_constructor(ctx, name, rec, n, _names.ptr(), sorts.ptr(), sort_refs.ptr()));
+            num_fields.push_back(n);
+        }
+
+        Z3_constructor operator[](unsigned i) const { return cons[i]; }
+
+        unsigned size() const { return (unsigned)cons.size(); }
+
+        constructor_list get_constructors() const {
+            return constructor_list(ctx, (unsigned)cons.size(), cons.data());
+        }
+
+        void query(unsigned i, func_decl& constructor, func_decl& test, func_decl_vector& accs) {
+            Z3_func_decl _constructor;
+            Z3_func_decl _test;
+            array<Z3_func_decl> accessors(num_fields[i]);
+            Z3_query_constructor(ctx,
+                                 cons[i],
+                                 num_fields[i],
+                                 &_constructor,
+                                 &_test,
+                                 accessors.ptr());
+            constructor = func_decl(ctx, _constructor);
+
+            test = func_decl(ctx, _test);
+            for (unsigned j = 0; j < num_fields[i]; ++j)
+                accs.push_back(func_decl(ctx, accessors[j]));
+        }
+    };
+
+    inline sort context::datatype(symbol const& name, constructors const& cs) {
+        array<Z3_constructor> _cs(cs.size());
+        for (unsigned i = 0; i < cs.size(); ++i) _cs[i] = cs[i];
+        Z3_sort s = Z3_mk_datatype(*this, name, cs.size(), _cs.ptr());
+        check_error();
+        return sort(*this, s);
+    }
+
+    inline sort context::datatype_sort(symbol const& name) {
+        Z3_sort s = Z3_mk_datatype_sort(*this, name);
+        check_error();
+        return sort(*this, s);            
+    }
+
+
     inline sort context::uninterpreted_sort(char const* name) {
         Z3_symbol _name = Z3_mk_string_symbol(*this, name);
         return to_sort(*this, Z3_mk_uninterpreted_sort(*this, _name));