From 2e13c0bf4162567df007c27b431030ffdb761691 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 20 Jul 2022 19:43:18 -0700 Subject: [PATCH] add API and example for one dimensional algebraic datatype #6179 --- examples/c++/example.cpp | 24 +++++++++- src/api/c++/z3++.h | 94 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 117 insertions(+), 1 deletion(-) diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index c71c3ff2f..980243761 100644 --- a/examples/c++/example.cpp +++ b/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"; diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 8aaeb31ab..50da0fcab 100644 --- a/src/api/c++/z3++.h +++ b/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 cons; + std::vector 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 sort_refs(n); + array sorts(n); + array _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 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 _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));