From 5d17e286672ee808702972cb6da60389bb80a720 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 4 Sep 2017 21:12:43 -0700 Subject: [PATCH] support for smtlib2.6 datatype parsing Signed-off-by: Nikolaj Bjorner --- src/api/api_datatype.cpp | 57 +++++----- src/ast/ast.cpp | 35 ++----- src/ast/ast_ll_pp.cpp | 2 +- src/ast/ast_smt2_pp.cpp | 2 +- src/ast/ast_smt_pp.cpp | 32 ++++-- src/ast/datatype_decl_plugin.cpp | 24 ++--- src/ast/datatype_decl_plugin.h | 14 +-- src/ast/datatype_decl_plugin2.cpp | 85 +++++++++------ src/ast/datatype_decl_plugin2.h | 31 +++--- src/ast/decl_collector.cpp | 4 +- src/ast/rewriter/datatype_rewriter.cpp | 4 +- src/ast/rewriter/enum2bv_rewriter.cpp | 2 +- src/cmd_context/cmd_context.cpp | 21 ++-- src/cmd_context/pdecl.cpp | 127 +++++++++++++++++++++-- src/cmd_context/pdecl.h | 29 ++++-- src/muz/base/dl_rule.h | 2 +- src/muz/base/rule_properties.cpp | 2 +- src/muz/bmc/dl_bmc_engine.cpp | 18 ++-- src/muz/pdr/pdr_prop_solver.cpp | 2 +- src/muz/spacer/spacer_util.cpp | 2 +- src/parsers/smt2/smt2parser.cpp | 27 ++++- src/qe/qe_datatype_plugin.cpp | 12 +-- src/qe/qe_datatypes.cpp | 6 +- src/qe/qe_lite.cpp | 2 +- src/smt/proto_model/datatype_factory.cpp | 6 +- src/smt/smt_value_sort.cpp | 2 +- src/smt/theory_datatype.cpp | 22 ++-- src/tactic/core/elim_uncnstr_tactic.cpp | 6 +- src/tactic/portfolio/enum2bv_solver.cpp | 2 +- 29 files changed, 374 insertions(+), 206 deletions(-) diff --git a/src/api/api_datatype.cpp b/src/api/api_datatype.cpp index d670888ed..d667a7428 100644 --- a/src/api/api_datatype.cpp +++ b/src/api/api_datatype.cpp @@ -45,13 +45,13 @@ extern "C" { ptr_vector acc; for (unsigned i = 0; i < num_fields; ++i) { - acc.push_back(mk_accessor_decl(to_symbol(field_names[i]), type_ref(to_sort(field_sorts[i])))); + acc.push_back(mk_accessor_decl(m, to_symbol(field_names[i]), type_ref(to_sort(field_sorts[i])))); } constructor_decl* constrs[1] = { mk_constructor_decl(to_symbol(name), recognizer, acc.size(), acc.c_ptr()) }; { - datatype_decl * dt = mk_datatype_decl(dt_util, to_symbol(name), 1, constrs); + datatype_decl * dt = mk_datatype_decl(dt_util, to_symbol(name), 0, nullptr, 1, constrs); bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &dt, 0, 0, tuples); del_datatype_decl(dt); @@ -69,13 +69,13 @@ extern "C" { // create constructor SASSERT(dt_util.is_datatype(tuple)); SASSERT(!dt_util.is_recursive(tuple)); - ptr_vector const & decls = dt_util.get_datatype_constructors(tuple); + ptr_vector const & decls = *dt_util.get_datatype_constructors(tuple); func_decl* decl = (decls)[0]; mk_c(c)->save_multiple_ast_trail(decl); *mk_tuple_decl = of_func_decl(decl); // Create projections - ptr_vector const & _accs = dt_util.get_constructor_accessors(decl); + ptr_vector const & _accs = *dt_util.get_constructor_accessors(decl); SASSERT(_accs.size() == num_fields); for (unsigned i = 0; i < _accs.size(); i++) { mk_c(c)->save_multiple_ast_trail(_accs[i]); @@ -113,7 +113,7 @@ extern "C" { { - datatype_decl * dt = mk_datatype_decl(dt_util, to_symbol(name), n, constrs.c_ptr()); + datatype_decl * dt = mk_datatype_decl(dt_util, to_symbol(name), 0, 0, n, constrs.c_ptr()); bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &dt, 0, 0, sorts); del_datatype_decl(dt); @@ -131,7 +131,7 @@ extern "C" { // create constructor SASSERT(dt_util.is_datatype(e)); SASSERT(!dt_util.is_recursive(e)); - ptr_vector const & decls = dt_util.get_datatype_constructors(e); + ptr_vector const & decls = *dt_util.get_datatype_constructors(e); SASSERT(decls.size() == n); for (unsigned i = 0; i < n; ++i) { func_decl* decl = (decls)[i]; @@ -164,8 +164,8 @@ extern "C" { mk_c(c)->reset_last_result(); datatype_util data_util(m); accessor_decl* head_tail[2] = { - mk_accessor_decl(symbol("head"), type_ref(to_sort(elem_sort))), - mk_accessor_decl(symbol("tail"), type_ref(0)) + mk_accessor_decl(m, symbol("head"), type_ref(to_sort(elem_sort))), + mk_accessor_decl(m, symbol("tail"), type_ref(0)) }; constructor_decl* constrs[2] = { mk_constructor_decl(symbol("nil"), symbol("is_nil"), 0, 0), @@ -175,7 +175,7 @@ extern "C" { sort_ref_vector sorts(m); { - datatype_decl * decl = mk_datatype_decl(dt_util, to_symbol(name), 2, constrs); + datatype_decl * decl = mk_datatype_decl(dt_util, to_symbol(name), 0, nullptr, 2, constrs); bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &decl, 0, 0, sorts); del_datatype_decl(decl); @@ -187,7 +187,7 @@ extern "C" { sort * s = sorts.get(0); mk_c(c)->save_multiple_ast_trail(s); - ptr_vector const& cnstrs = data_util.get_datatype_constructors(s); + ptr_vector const& cnstrs = *data_util.get_datatype_constructors(s); SASSERT(cnstrs.size() == 2); func_decl* f; if (nil_decl) { @@ -211,14 +211,14 @@ extern "C" { *is_cons_decl = of_func_decl(f); } if (head_decl) { - ptr_vector const& acc = data_util.get_constructor_accessors(cnstrs[1]); + ptr_vector const& acc = *data_util.get_constructor_accessors(cnstrs[1]); SASSERT(acc.size() == 2); f = (acc)[0]; mk_c(c)->save_multiple_ast_trail(f); *head_decl = of_func_decl(f); } if (tail_decl) { - ptr_vector const& acc = data_util.get_constructor_accessors(cnstrs[1]); + ptr_vector const& acc = *data_util.get_constructor_accessors(cnstrs[1]); SASSERT(acc.size() == 2); f = (acc)[1]; mk_c(c)->save_multiple_ast_trail(f); @@ -295,7 +295,7 @@ extern "C" { *tester = of_func_decl(f2); } - ptr_vector const& accs = data_util.get_constructor_accessors(f); + ptr_vector const& accs = *data_util.get_constructor_accessors(f); for (unsigned i = 0; i < num_fields; ++i) { func_decl* f2 = (accs)[i]; mk_c(c)->save_multiple_ast_trail(f2); @@ -318,21 +318,22 @@ extern "C" { unsigned num_constructors, Z3_constructor constructors[]) { datatype_util& dt_util = mk_c(c)->dtutil(); + ast_manager& m = mk_c(c)->m(); ptr_vector constrs; for (unsigned i = 0; i < num_constructors; ++i) { constructor* cn = reinterpret_cast(constructors[i]); ptr_vector acc; for (unsigned j = 0; j < cn->m_sorts.size(); ++j) { if (cn->m_sorts[j].get()) { - acc.push_back(mk_accessor_decl(cn->m_field_names[j], type_ref(cn->m_sorts[j].get()))); + acc.push_back(mk_accessor_decl(m, cn->m_field_names[j], type_ref(cn->m_sorts[j].get()))); } else { - acc.push_back(mk_accessor_decl(cn->m_field_names[j], type_ref(cn->m_sort_refs[j]))); + acc.push_back(mk_accessor_decl(m, cn->m_field_names[j], type_ref(cn->m_sort_refs[j]))); } } constrs.push_back(mk_constructor_decl(cn->m_name, cn->m_tester, acc.size(), acc.c_ptr())); } - return mk_datatype_decl(dt_util, to_symbol(name), num_constructors, constrs.c_ptr()); + return mk_datatype_decl(dt_util, to_symbol(name), 0, nullptr, num_constructors, constrs.c_ptr()); } Z3_sort Z3_API Z3_mk_datatype(Z3_context c, @@ -359,7 +360,7 @@ extern "C" { sort * s = sorts.get(0); mk_c(c)->save_ast_trail(s); - ptr_vector const& cnstrs = data_util.get_datatype_constructors(s); + ptr_vector const& cnstrs = *data_util.get_datatype_constructors(s); for (unsigned i = 0; i < num_constructors; ++i) { constructor* cn = reinterpret_cast(constructors[i]); @@ -408,7 +409,7 @@ extern "C" { ptr_vector datas; for (unsigned i = 0; i < num_sorts; ++i) { constructor_list* cl = reinterpret_cast(constructor_lists[i]); - datas.push_back(mk_datatype_decl(c,sort_names[i], cl->size(), reinterpret_cast(cl->c_ptr()))); + datas.push_back(mk_datatype_decl(c, sort_names[i], cl->size(), reinterpret_cast(cl->c_ptr()))); } sort_ref_vector _sorts(m); bool ok = mk_c(c)->get_dt_plugin()->mk_datatypes(datas.size(), datas.c_ptr(), 0, 0, _sorts); @@ -425,7 +426,7 @@ extern "C" { mk_c(c)->save_multiple_ast_trail(s); sorts[i] = of_sort(s); constructor_list* cl = reinterpret_cast(constructor_lists[i]); - ptr_vector const& cnstrs = data_util.get_datatype_constructors(s); + ptr_vector const& cnstrs = *data_util.get_datatype_constructors(s); for (unsigned j = 0; j < cl->size(); ++j) { constructor* cn = (*cl)[j]; cn->m_constructor = cnstrs[j]; @@ -447,7 +448,7 @@ extern "C" { SET_ERROR_CODE(Z3_INVALID_ARG); return 0; } - return dt_util.get_datatype_constructors(_t).size(); + return dt_util.get_datatype_constructors(_t)->size(); Z3_CATCH_RETURN(0); } @@ -460,7 +461,7 @@ extern "C" { SET_ERROR_CODE(Z3_INVALID_ARG); return 0; } - ptr_vector const & decls = dt_util.get_datatype_constructors(_t); + ptr_vector const & decls = *dt_util.get_datatype_constructors(_t); if (idx >= decls.size()) { SET_ERROR_CODE(Z3_INVALID_ARG); return 0; @@ -490,7 +491,7 @@ extern "C" { SET_ERROR_CODE(Z3_INVALID_ARG); RETURN_Z3(0); } - ptr_vector const & decls = dt_util.get_datatype_constructors(_t); + ptr_vector const & decls = *dt_util.get_datatype_constructors(_t); if (idx >= decls.size()) { SET_ERROR_CODE(Z3_INVALID_ARG); RETURN_Z3(0); @@ -513,7 +514,7 @@ extern "C" { SET_ERROR_CODE(Z3_INVALID_ARG); RETURN_Z3(0); } - ptr_vector const & decls = dt_util.get_datatype_constructors(_t); + ptr_vector const & decls = *dt_util.get_datatype_constructors(_t); if (idx_c >= decls.size()) { SET_ERROR_CODE(Z3_INVALID_ARG); return 0; @@ -523,7 +524,7 @@ extern "C" { SET_ERROR_CODE(Z3_INVALID_ARG); RETURN_Z3(0); } - ptr_vector const & accs = dt_util.get_constructor_accessors(decl); + ptr_vector const & accs = *dt_util.get_constructor_accessors(decl); SASSERT(accs.size() == decl->get_arity()); if (accs.size() <= idx_a) { SET_ERROR_CODE(Z3_INVALID_ARG); @@ -560,12 +561,12 @@ extern "C" { SET_ERROR_CODE(Z3_INVALID_ARG); return 0; } - ptr_vector const & decls = dt_util.get_datatype_constructors(tuple); + ptr_vector const & decls = *dt_util.get_datatype_constructors(tuple); if (decls.size() != 1) { SET_ERROR_CODE(Z3_INVALID_ARG); return 0; } - ptr_vector const & accs = dt_util.get_constructor_accessors(decls[0]); + ptr_vector const & accs = *dt_util.get_constructor_accessors(decls[0]); return accs.size(); Z3_CATCH_RETURN(0); } @@ -580,12 +581,12 @@ extern "C" { SET_ERROR_CODE(Z3_INVALID_ARG); RETURN_Z3(0); } - ptr_vector const & decls = dt_util.get_datatype_constructors(tuple); + ptr_vector const & decls = *dt_util.get_datatype_constructors(tuple); if (decls.size() != 1) { SET_ERROR_CODE(Z3_INVALID_ARG); RETURN_Z3(0); } - ptr_vector const & accs = dt_util.get_constructor_accessors((decls)[0]); + ptr_vector const & accs = *dt_util.get_constructor_accessors((decls)[0]); if (accs.size() <= i) { SET_ERROR_CODE(Z3_IOB); RETURN_Z3(0); diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 1a35e710a..a905efa28 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1287,10 +1287,8 @@ decl_kind user_sort_plugin::register_name(symbol s) { decl_plugin * user_sort_plugin::mk_fresh() { user_sort_plugin * p = alloc(user_sort_plugin); - svector::iterator it = m_sort_names.begin(); - svector::iterator end = m_sort_names.end(); - for (; it != end; ++it) - p->register_name(*it); + for (symbol const& s : m_sort_names) + p->register_name(s); return p; } @@ -1410,26 +1408,20 @@ ast_manager::~ast_manager() { dec_ref(m_true); dec_ref(m_false); dec_ref(m_undef_proof); - ptr_vector::iterator it = m_plugins.begin(); - ptr_vector::iterator end = m_plugins.end(); - for (; it != end; ++it) { - if (*it) - (*it)->finalize(); + for (decl_plugin* p : m_plugins) { + if (p) + p->finalize(); } - it = m_plugins.begin(); - for (; it != end; ++it) { - if (*it) - dealloc(*it); + for (decl_plugin* p : m_plugins) { + if (p) + dealloc(p); } m_plugins.reset(); while (!m_ast_table.empty()) { DEBUG_CODE(std::cout << "ast_manager LEAKED: " << m_ast_table.size() << std::endl;); ptr_vector roots; ast_mark mark; - ast_table::iterator it_a = m_ast_table.begin(); - ast_table::iterator end_a = m_ast_table.end(); - for (; it_a != end_a; ++it_a) { - ast* n = (*it_a); + for (ast * n : m_ast_table) { switch (n->get_kind()) { case AST_SORT: { sort_info* info = to_sort(n)->get_info(); @@ -1462,9 +1454,7 @@ ast_manager::~ast_manager() { break; } } - it_a = m_ast_table.begin(); - for (; it_a != end_a; ++it_a) { - ast* n = *it_a; + for (ast * n : m_ast_table) { if (!mark.is_marked(n)) { roots.push_back(n); } @@ -1659,11 +1649,8 @@ bool ast_manager::is_bool(expr const * n) const { #ifdef Z3DEBUG bool ast_manager::slow_not_contains(ast const * n) { - ast_table::iterator it = m_ast_table.begin(); - ast_table::iterator end = m_ast_table.end(); unsigned num = 0; - for (; it != end; ++it) { - ast * curr = *it; + for (ast * curr : m_ast_table) { if (compare_nodes(curr, n)) { TRACE("nondet_bug", tout << "id1: " << curr->get_id() << ", id2: " << n->get_id() << "\n"; diff --git a/src/ast/ast_ll_pp.cpp b/src/ast/ast_ll_pp.cpp index c00053780..6b14b75a8 100644 --- a/src/ast/ast_ll_pp.cpp +++ b/src/ast/ast_ll_pp.cpp @@ -284,7 +284,7 @@ public: } unsigned num_args = to_app(n)->get_num_args(); if (num_args > 0) - m_out << "("; + m_out << "(_ "; display_name(to_app(n)->get_decl()); display_params(to_app(n)->get_decl()); for (unsigned i = 0; i < num_args; i++) { diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp index 51ccc1e7d..642983737 100644 --- a/src/ast/ast_smt2_pp.cpp +++ b/src/ast/ast_smt2_pp.cpp @@ -431,7 +431,7 @@ format_ns::format * smt2_pp_environment::pp_sort(sort * s) { fs.push_back(pp_sort(to_sort(s->get_parameter(0).get_ast()))); return mk_seq1(m, fs.begin(), fs.end(), f2f(), get_sutil().is_seq(s)?"Seq":"RegEx"); } -#if 0 +#ifdef DATATYPE_V2 if (get_dtutil().is_datatype(s)) { ptr_buffer fs; unsigned sz = get_dtutil().get_datatype_num_parameter_sorts(s); diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp index 9211c5899..fdac6c7be 100644 --- a/src/ast/ast_smt_pp.cpp +++ b/src/ast/ast_smt_pp.cpp @@ -21,17 +21,17 @@ Revision History: #include #include +#include "util/vector.h" +#include "util/smt2_util.h" #include "ast/ast_smt_pp.h" #include "ast/arith_decl_plugin.h" #include "ast/bv_decl_plugin.h" #include "ast/array_decl_plugin.h" #include "ast/datatype_decl_plugin.h" +#include "ast/seq_decl_plugin.h" #include "ast/fpa_decl_plugin.h" -#include "util/vector.h" #include "ast/for_each_ast.h" #include "ast/decl_collector.h" -#include "util/smt2_util.h" -#include "ast/seq_decl_plugin.h" // --------------------------------------- // smt_renaming @@ -210,7 +210,19 @@ class smt_printer { void pp_decl(func_decl* d) { symbol sym = m_renaming.get_symbol(d->get_name()); if (d->get_family_id() == m_dt_fid) { +#ifdef DATATYPE_V2 + std::cout << "printing " << sym << "\n"; + datatype_util util(m_manager); + if (util.is_recognizer(d)) { + std::cout << d->get_num_parameters() << "\n"; + visit_params(false, sym, d->get_num_parameters(), d->get_parameters()); + } + else { + m_out << sym; + } +#else m_out << sym; +#endif } else if (m_manager.is_ite(d)) { if (!m_is_smt2 && is_bool(d->get_range())) { @@ -366,14 +378,15 @@ class smt_printer { return; } else if (s->is_sort_of(m_dt_fid, DATATYPE_SORT)) { +#ifndef DATATYPE_V2 m_out << m_renaming.get_symbol(s->get_name()); -#if 0 +#else datatype_util util(m_manager); unsigned num_sorts = util.get_datatype_num_parameter_sorts(s); if (num_sorts > 0) { m_out << "("; } - + m_out << m_renaming.get_symbol(s->get_name()); if (num_sorts > 0) { for (unsigned i = 0; i < num_sorts; ++i) { m_out << " "; @@ -533,7 +546,8 @@ class smt_printer { pp_arg(curr, n); m_out << ")"; - } else if (m_manager.is_distinct(decl)) { + } + else if (m_manager.is_distinct(decl)) { ptr_vector args(num_args, n->get_args()); unsigned idx = 0; m_out << "(and"; @@ -915,7 +929,7 @@ public: // collect siblings and sorts that have not already been printed. for (unsigned h = 0; h < rec_sorts.size(); ++h) { s = rec_sorts[h]; - ptr_vector const& decls = util.get_datatype_constructors(s); + ptr_vector const& decls = *util.get_datatype_constructors(s); for (unsigned i = 0; i < decls.size(); ++i) { func_decl* f = decls[i]; @@ -954,11 +968,11 @@ public: m_out << "("; m_out << m_renaming.get_symbol(s->get_name()); m_out << " "; - ptr_vector const& decls = util.get_datatype_constructors(s); + ptr_vector const& decls = *util.get_datatype_constructors(s); for (unsigned i = 0; i < decls.size(); ++i) { func_decl* f = decls[i]; - ptr_vector const& accs = util.get_constructor_accessors(f); + ptr_vector const& accs = *util.get_constructor_accessors(f); if (m_is_smt2 || accs.size() > 0) { m_out << "("; } diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 1c090bc33..7ad80336d 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -34,7 +34,7 @@ public: type_ref const & get_type() const { return m_type; } }; -accessor_decl * mk_accessor_decl(symbol const & n, type_ref const & t) { +accessor_decl * mk_accessor_decl(ast_manager& m, symbol const & n, type_ref const & t) { return alloc(accessor_decl, n, t); } @@ -95,7 +95,7 @@ public: ptr_vector const & get_constructors() const { return m_constructors; } }; -datatype_decl * mk_datatype_decl(datatype_util&, symbol const & n, unsigned num_constructors, constructor_decl * const * cs) { +datatype_decl * mk_datatype_decl(datatype_util&, symbol const & n, unsigned num_params, sort * const* params, unsigned num_constructors, constructor_decl * const * cs) { return alloc(datatype_decl, n, num_constructors, cs); } @@ -803,11 +803,11 @@ func_decl * datatype_util::get_constructor(sort * ty, unsigned c_id) { return d; } -ptr_vector const & datatype_util::get_datatype_constructors(sort * ty) { +ptr_vector const * datatype_util::get_datatype_constructors(sort * ty) { SASSERT(is_datatype(ty)); ptr_vector * r = 0; if (m_datatype2constructors.find(ty, r)) - return *r; + return r; r = alloc(ptr_vector); m_asts.push_back(ty); m_vectors.push_back(r); @@ -820,7 +820,7 @@ ptr_vector const & datatype_util::get_datatype_constructors(sort * ty m_asts.push_back(c); r->push_back(c); } - return *r; + return r; } /** @@ -855,7 +855,7 @@ func_decl * datatype_util::get_non_rec_constructor_core(sort * ty, ptr_vector const & constructors = get_datatype_constructors(ty); + ptr_vector const & constructors = *get_datatype_constructors(ty); // step 1) unsigned sz = constructors.size(); ++m_start; @@ -916,11 +916,11 @@ func_decl * datatype_util::get_constructor_recognizer(func_decl * constructor) { return d; } -ptr_vector const & datatype_util::get_constructor_accessors(func_decl * constructor) { +ptr_vector const * datatype_util::get_constructor_accessors(func_decl * constructor) { SASSERT(is_constructor(constructor)); ptr_vector * res = 0; if (m_constructor2accessors.find(constructor, res)) - return *res; + return res; res = alloc(ptr_vector); m_asts.push_back(constructor); m_vectors.push_back(res); @@ -939,7 +939,7 @@ ptr_vector const & datatype_util::get_constructor_accessors(func_decl m_asts.push_back(d); res->push_back(d); } - return *res; + return res; } func_decl * datatype_util::get_accessor_constructor(func_decl * accessor) { @@ -989,7 +989,7 @@ bool datatype_util::is_enum_sort(sort* s) { bool r = false; if (m_is_enum.find(s, r)) return r; - ptr_vector const& cnstrs = get_datatype_constructors(s); + ptr_vector const& cnstrs = *get_datatype_constructors(s); r = true; for (unsigned i = 0; r && i < cnstrs.size(); ++i) { r = cnstrs[i]->get_arity() == 0; @@ -1049,12 +1049,12 @@ void datatype_util::display_datatype(sort *s0, std::ostream& strm) { todo.pop_back(); strm << s->get_name() << " =\n"; - ptr_vector const & cnstrs = get_datatype_constructors(s); + ptr_vector const & cnstrs = *get_datatype_constructors(s); for (unsigned i = 0; i < cnstrs.size(); ++i) { func_decl* cns = cnstrs[i]; func_decl* rec = get_constructor_recognizer(cns); strm << " " << cns->get_name() << " :: " << rec->get_name() << " :: "; - ptr_vector const & accs = get_constructor_accessors(cns); + ptr_vector const & accs = *get_constructor_accessors(cns); for (unsigned j = 0; j < accs.size(); ++j) { func_decl* acc = accs[j]; sort* s1 = acc->get_range(); diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h index e3e1b7b10..3b4c8dd08 100644 --- a/src/ast/datatype_decl_plugin.h +++ b/src/ast/datatype_decl_plugin.h @@ -16,7 +16,7 @@ Author: Revision History: --*/ -//define DATATYPE_V2 +// define DATATYPE_V2 #ifdef DATATYPE_V2 #include "ast/datatype_decl_plugin2.h" #else @@ -78,15 +78,11 @@ class constructor_decl; class datatype_decl; class datatype_util; -accessor_decl * mk_accessor_decl(symbol const & n, type_ref const & t); -//void del_accessor_decl(accessor_decl * d); -//void del_accessor_decls(unsigned num, accessor_decl * const * as); +accessor_decl * mk_accessor_decl(ast_manager& m, symbol const & n, type_ref const & t); // Remark: the constructor becomes the owner of the accessor_decls constructor_decl * mk_constructor_decl(symbol const & n, symbol const & r, unsigned num_accessors, accessor_decl * const * acs); -//void del_constructor_decl(constructor_decl * d); -//void del_constructor_decls(unsigned num, constructor_decl * const * cs); // Remark: the datatype becomes the owner of the constructor_decls -datatype_decl * mk_datatype_decl(datatype_util& u, symbol const & n, unsigned num_constructors, constructor_decl * const * cs); +datatype_decl * mk_datatype_decl(datatype_util& u, symbol const & n, unsigned num_params, sort * const* params, unsigned num_constructors, constructor_decl * const * cs); void del_datatype_decl(datatype_decl * d); void del_datatype_decls(unsigned num, datatype_decl * const * ds); @@ -216,7 +212,7 @@ public: bool is_recognizer(app * f) const { return is_app_of(f, m_family_id, OP_DT_RECOGNISER); } bool is_accessor(app * f) const { return is_app_of(f, m_family_id, OP_DT_ACCESSOR); } bool is_update_field(app * f) const { return is_app_of(f, m_family_id, OP_DT_UPDATE_FIELD); } - ptr_vector const & get_datatype_constructors(sort * ty); + ptr_vector const * get_datatype_constructors(sort * ty); unsigned get_datatype_num_constructors(sort * ty) { SASSERT(is_datatype(ty)); unsigned tid = ty->get_parameter(1).get_int(); @@ -236,7 +232,7 @@ public: unsigned get_recognizer_constructor_idx(func_decl * f) const { SASSERT(is_recognizer(f)); return f->get_parameter(1).get_int(); } func_decl * get_non_rec_constructor(sort * ty); func_decl * get_constructor_recognizer(func_decl * constructor); - ptr_vector const & get_constructor_accessors(func_decl * constructor); + ptr_vector const * get_constructor_accessors(func_decl * constructor); func_decl * get_accessor_constructor(func_decl * accessor); func_decl * get_recognizer_constructor(func_decl * recognizer); family_id get_family_id() const { return m_family_id; } diff --git a/src/ast/datatype_decl_plugin2.cpp b/src/ast/datatype_decl_plugin2.cpp index c059907d5..41ae2e839 100644 --- a/src/ast/datatype_decl_plugin2.cpp +++ b/src/ast/datatype_decl_plugin2.cpp @@ -37,6 +37,7 @@ namespace datatype { func_decl_ref accessor::instantiate(sort_ref_vector const& ps) const { ast_manager& m = ps.get_manager(); unsigned n = ps.size(); + SASSERT(m_range); SASSERT(n == get_def().params().size()); sort_ref range(m.substitute(m_range, n, get_def().params().c_ptr(), ps.c_ptr()), m); sort_ref src(get_def().instantiate(ps)); @@ -79,13 +80,14 @@ namespace datatype { sort_ref s(m); if (!m_sort) { vector ps; + ps.push_back(parameter(m_name)); for (sort * s : m_params) ps.push_back(parameter(s)); m_sort = m.mk_sort(u().get_family_id(), DATATYPE_SORT, ps.size(), ps.c_ptr()); } if (sorts.empty()) { return m_sort; } - return sort_ref(m.substitute(m_sort, sorts.size(), sorts.c_ptr(), m_params.c_ptr()), m); + return sort_ref(m.substitute(m_sort, sorts.size(), m_params.c_ptr(), sorts.c_ptr()), m); } enum status { @@ -135,6 +137,7 @@ namespace datatype { util & plugin::u() const { SASSERT(m_manager); + SASSERT(m_family_id != null_family_id); if (m_util.get() == 0) { m_util = alloc(util, *m_manager); } @@ -146,9 +149,11 @@ namespace datatype { sort * plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) { try { if (k != DATATYPE_SORT) { + TRACE("datatype", tout << "invalid kind parameter to datatype\n";); throw invalid_datatype(); } if (num_parameters < 1) { + TRACE("datatype", tout << "at least one parameter expected to datatype declaration\n";); throw invalid_datatype(); } parameter const & name = parameters[0]; @@ -169,13 +174,17 @@ namespace datatype { def* d = 0; if (m_defs.find(s->get_name(), d) && d->sort_size()) { obj_map S; - for (unsigned i = 1; i < num_parameters; ++i) { - sort* r = to_sort(parameters[i].get_ast()); + for (unsigned i = 0; i + 1 < num_parameters; ++i) { + sort* r = to_sort(parameters[i + 1].get_ast()); S.insert(d->params()[i], r->get_num_elements()); } sort_size ts = d->sort_size()->eval(S); + TRACE("datatype", tout << name << " has size " << ts << "\n";); s->set_num_elements(ts); } + else { + TRACE("datatype", tout << "not setting size for " << name << "\n";); + } return s; } catch (invalid_datatype) { @@ -227,14 +236,12 @@ namespace datatype { return m.mk_func_decl(symbol("update-field"), arity, domain, range, info); } +#define VALIDATE_PARAM(_pred_) if (!(_pred_)) m_manager->raise_exception("invalid parameter to datatype function"); func_decl * decl::plugin::mk_constructor(unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { ast_manager& m = *m_manager; - SASSERT(num_parameters == 1 && parameters[0].is_symbol() && range && u().is_datatype(range)); - if (num_parameters != 1 || !parameters[0].is_symbol() || !range || !u().is_datatype(range)) { - m_manager->raise_exception("invalid parameters for datatype constructor"); - } + VALIDATE_PARAM(num_parameters == 1 && parameters[0].is_symbol() && range && u().is_datatype(range)); // we blindly trust other conditions are met, including domain types. symbol name = parameters[0].get_symbol(); func_decl_info info(m_family_id, OP_DT_CONSTRUCTOR, num_parameters, parameters); @@ -245,27 +252,27 @@ namespace datatype { func_decl * decl::plugin::mk_recognizer(unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort *) { ast_manager& m = *m_manager; - SASSERT(arity == 1 && num_parameters == 1 && parameters[0].is_ast() && is_func_decl(parameters[0].get_ast())); - SASSERT(u().is_datatype(domain[0])); + VALIDATE_PARAM(arity == 1 && num_parameters == 1 && parameters[0].is_ast() && is_func_decl(parameters[0].get_ast())); + VALIDATE_PARAM(u().is_datatype(domain[0])); // blindly trust that parameter is a constructor sort* range = m_manager->mk_bool_sort(); + func_decl* f = to_func_decl(parameters[0].get_ast()); func_decl_info info(m_family_id, OP_DT_RECOGNISER, num_parameters, parameters); info.m_private_parameters = true; - symbol name = to_func_decl(parameters[0].get_ast())->get_name(); - return m.mk_func_decl(name, arity, domain, range); + return m.mk_func_decl(symbol("is"), arity, domain, range, info); } func_decl * decl::plugin::mk_accessor(unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { ast_manager& m = *m_manager; - SASSERT(arity == 1 && num_parameters == 2 && parameters[0].is_symbol() && parameters[0].is_symbol()); - SASSERT(u().is_datatype(domain[0])); + VALIDATE_PARAM(arity == 1 && num_parameters == 2 && parameters[0].is_symbol() && parameters[1].is_symbol()); + VALIDATE_PARAM(u().is_datatype(domain[0])); SASSERT(range); func_decl_info info(m_family_id, OP_DT_ACCESSOR, num_parameters, parameters); info.m_private_parameters = true; symbol name = parameters[0].get_symbol(); - return m.mk_func_decl(name, arity, domain, range); + return m.mk_func_decl(name, arity, domain, range, info); } func_decl * decl::plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, @@ -290,15 +297,20 @@ namespace datatype { return alloc(def, m, u(), name, m_class_id, n, params); } +#if 0 def& plugin::add(symbol const& name, unsigned n, sort * const * params) { ast_manager& m = *m_manager; def* d = 0; - if (m_defs.find(name, d)) dealloc(d); + if (m_defs.find(name, d)) { + TRACE("datatype", tout << "delete previous version for " << name << "\n";); + dealloc(d); + } d = alloc(def, m, u(), name, m_class_id, n, params); m_defs.insert(name, d); m_def_block.push_back(name); return *d; } +#endif void plugin::end_def_block() { ast_manager& m = *m_manager; @@ -325,7 +337,11 @@ namespace datatype { bool plugin::mk_datatypes(unsigned num_datatypes, def * const * datatypes, unsigned num_params, sort* const* sort_params, sort_ref_vector & new_sorts) { begin_def_block(); for (unsigned i = 0; i < num_datatypes; ++i) { - if (m_defs.find(datatypes[i]->name(), d)) dealloc(d); + def* d = 0; + if (m_defs.find(datatypes[i]->name(), d)) { + TRACE("datatype", tout << "delete previous version for " << datatypes[i]->name() << "\n";); + dealloc(d); + } m_defs.insert(datatypes[i]->name(), datatypes[i]); m_def_block.push_back(datatypes[i]->name()); } @@ -391,6 +407,7 @@ namespace datatype { } void plugin::get_op_names(svector & op_names, symbol const & logic) { + op_names.push_back(builtin_name("is", OP_DT_RECOGNISER)); if (logic == symbol::null) { op_names.push_back(builtin_name("update-field", OP_DT_UPDATE_FIELD)); } @@ -548,6 +565,10 @@ namespace datatype { } return param_size::size::mk_offset(s->get_num_elements()); } + + bool util::is_declared(sort* s) const { + return m_plugin->is_declared(s); + } void util::compute_datatype_size_functions(svector const& names) { map already_found; @@ -668,17 +689,18 @@ namespace datatype { m_asts(m), m_start(0) { m_plugin = dynamic_cast(m.get_plugin(m_family_id)); + SASSERT(m_plugin); } util::~util() { std::for_each(m_vectors.begin(), m_vectors.end(), delete_proc >()); } - ptr_vector const & util::get_datatype_constructors(sort * ty) { + ptr_vector const * util::get_datatype_constructors(sort * ty) { SASSERT(is_datatype(ty)); ptr_vector * r = 0; if (m_datatype2constructors.find(ty, r)) - return *r; + return r; r = alloc(ptr_vector); m_asts.push_back(ty); m_vectors.push_back(r); @@ -689,14 +711,15 @@ namespace datatype { m_asts.push_back(f); r->push_back(f); } - return *r; + return r; } - ptr_vector const & util::get_constructor_accessors(func_decl * con) { + ptr_vector const * util::get_constructor_accessors(func_decl * con) { SASSERT(is_constructor(con)); ptr_vector * res = 0; - if (m_constructor2accessors.find(con, res)) - return *res; + if (m_constructor2accessors.find(con, res)) { + return res; + } res = alloc(ptr_vector); m_asts.push_back(con); m_vectors.push_back(res); @@ -706,12 +729,14 @@ namespace datatype { for (constructor const* c : d) { if (c->name() == con->get_name()) { for (accessor const* a : *c) { - res->push_back(a->instantiate(datatype)); + func_decl_ref fn = a->instantiate(datatype); + res->push_back(fn); + m_asts.push_back(fn); } break; } } - return *res; + return res; } func_decl * util::get_constructor_recognizer(func_decl * constructor) { @@ -752,7 +777,7 @@ namespace datatype { bool r = false; if (m_is_enum.find(s, r)) return r; - ptr_vector const& cnstrs = get_datatype_constructors(s); + ptr_vector const& cnstrs = *get_datatype_constructors(s); r = true; for (unsigned i = 0; r && i < cnstrs.size(); ++i) { r = cnstrs[i]->get_arity() == 0; @@ -833,7 +858,7 @@ namespace datatype { // 1) T_i's are not recursive // If there is no such constructor, then we select one that // 2) each type T_i is not recursive or contains a constructor that does not depend on T - ptr_vector const& constructors = get_datatype_constructors(ty); + ptr_vector const& constructors = *get_datatype_constructors(ty); // step 1) unsigned sz = constructors.size(); ++m_start; @@ -928,12 +953,12 @@ namespace datatype { todo.pop_back(); strm << s->get_name() << " =\n"; - ptr_vector const& cnstrs = get_datatype_constructors(s); + ptr_vector const& cnstrs = *get_datatype_constructors(s); for (unsigned i = 0; i < cnstrs.size(); ++i) { func_decl* cns = cnstrs[i]; func_decl* rec = get_constructor_recognizer(cns); strm << " " << cns->get_name() << " :: " << rec->get_name() << " :: "; - ptr_vector const & accs = get_constructor_accessors(cns); + ptr_vector const & accs = *get_constructor_accessors(cns); for (unsigned j = 0; j < accs.size(); ++j) { func_decl* acc = accs[j]; sort* s1 = acc->get_range(); @@ -949,9 +974,9 @@ namespace datatype { } } -datatype_decl * mk_datatype_decl(datatype_util& u, symbol const & n, unsigned num_constructors, constructor_decl * const * cs) { +datatype_decl * mk_datatype_decl(datatype_util& u, symbol const & n, unsigned num_params, sort*const* params, unsigned num_constructors, constructor_decl * const * cs) { datatype::decl::plugin* p = u.get_plugin(); - datatype::def( d = p->mk(n, 0, 0); + datatype::def* d = p->mk(n, num_params, params); for (unsigned i = 0; i < num_constructors; ++i) { d->add(cs[i]); } diff --git a/src/ast/datatype_decl_plugin2.h b/src/ast/datatype_decl_plugin2.h index c79939a5b..d7173b24a 100644 --- a/src/ast/datatype_decl_plugin2.h +++ b/src/ast/datatype_decl_plugin2.h @@ -50,19 +50,19 @@ namespace datatype { class accessor { - symbol m_name; - sort* m_range; + symbol m_name; + sort_ref m_range; unsigned m_index; // reference to recursive data-type may only get resolved after all mutually recursive data-types are procssed. constructor* m_constructor; public: - accessor(symbol const& n, sort* range): + accessor(ast_manager& m, symbol const& n, sort* range): m_name(n), - m_range(range), + m_range(range, m), m_index(UINT_MAX) {} - accessor(symbol const& n, unsigned index): + accessor(ast_manager& m, symbol const& n, unsigned index): m_name(n), - m_range(0), + m_range(m), m_index(index) {} sort* range() const { return m_range; } @@ -262,8 +262,6 @@ namespace datatype { void end_def_block(); - def& add(symbol const& name, unsigned n, sort * const * params); - def* mk(symbol const& name, unsigned n, sort * const * params); void del(symbol const& d); @@ -272,7 +270,7 @@ namespace datatype { def const& get_def(sort* s) const { return *(m_defs[datatype_name(s)]); } def& get_def(symbol const& s) { return *(m_defs[s]); } - + bool is_declared(sort* s) const { return m_defs.contains(datatype_name(s)); } private: bool is_value_visit(expr * arg, ptr_buffer & todo) const; @@ -337,6 +335,7 @@ namespace datatype { util(ast_manager & m); ~util(); ast_manager & get_manager() const { return m; } + // sort * mk_datatype_sort(symbol const& name, unsigned n, sort* const* params); bool is_datatype(sort const* s) const { return is_sort_of(s, m_family_id, DATATYPE_SORT); } bool is_enum_sort(sort* s); bool is_recursive(sort * ty); @@ -348,13 +347,13 @@ namespace datatype { bool is_recognizer(app * f) const { return is_app_of(f, m_family_id, OP_DT_RECOGNISER); } bool is_accessor(app * f) const { return is_app_of(f, m_family_id, OP_DT_ACCESSOR); } bool is_update_field(app * f) const { return is_app_of(f, m_family_id, OP_DT_UPDATE_FIELD); } - ptr_vector const & get_datatype_constructors(sort * ty); + ptr_vector const * get_datatype_constructors(sort * ty); unsigned get_datatype_num_constructors(sort * ty); unsigned get_datatype_num_parameter_sorts(sort * ty); sort* get_datatype_parameter_sort(sort * ty, unsigned idx); func_decl * get_non_rec_constructor(sort * ty); func_decl * get_constructor_recognizer(func_decl * constructor); - ptr_vector const & get_constructor_accessors(func_decl * constructor); + ptr_vector const * get_constructor_accessors(func_decl * constructor); func_decl * get_accessor_constructor(func_decl * accessor); func_decl * get_recognizer_constructor(func_decl * recognizer) const; family_id get_family_id() const { return m_family_id; } @@ -362,11 +361,13 @@ namespace datatype { bool is_func_decl(op_kind k, unsigned num_params, parameter const* params, func_decl* f); bool is_constructor_of(unsigned num_params, parameter const* params, func_decl* f); void reset(); + bool is_declared(sort* s) const; void display_datatype(sort *s, std::ostream& strm); bool is_fully_interp(sort * s) const; sort_ref_vector datatype_params(sort * s) const; unsigned get_constructor_idx(func_decl * f) const; unsigned get_recognizer_constructor_idx(func_decl * f) const; + decl::plugin* get_plugin() { return m_plugin; } }; }; @@ -390,12 +391,12 @@ public: int get_idx() const { return UNBOXINT(m_data); } }; -inline accessor_decl * mk_accessor_decl(symbol const & n, type_ref const & t) { +inline accessor_decl * mk_accessor_decl(ast_manager& m, symbol const & n, type_ref const & t) { if (t.is_idx()) { - return alloc(accessor_decl, n, t.get_idx()); + return alloc(accessor_decl, m, n, t.get_idx()); } else { - return alloc(accessor_decl, n, t.get_sort()); + return alloc(accessor_decl, m, n, t.get_sort()); } } @@ -410,7 +411,7 @@ inline constructor_decl * mk_constructor_decl(symbol const & n, symbol const & r // Remark: the datatype becomes the owner of the constructor_decls -datatype_decl * mk_datatype_decl(datatype_util& u, symbol const & n, unsigned num_constructors, constructor_decl * const * cs); +datatype_decl * mk_datatype_decl(datatype_util& u, symbol const & n, unsigned num_params, sort*const* params, unsigned num_constructors, constructor_decl * const * cs); inline void del_datatype_decl(datatype_decl * d) {} inline void del_datatype_decls(unsigned num, datatype_decl * const * ds) {} diff --git a/src/ast/decl_collector.cpp b/src/ast/decl_collector.cpp index bf509aba5..e000f43df 100644 --- a/src/ast/decl_collector.cpp +++ b/src/ast/decl_collector.cpp @@ -28,9 +28,9 @@ void decl_collector::visit_sort(sort * n) { unsigned num_cnstr = m_dt_util.get_datatype_num_constructors(n); for (unsigned i = 0; i < num_cnstr; i++) { - func_decl * cnstr = m_dt_util.get_datatype_constructors(n).get(i); + func_decl * cnstr = m_dt_util.get_datatype_constructors(n)->get(i); m_decls.push_back(cnstr); - ptr_vector const & cnstr_acc = m_dt_util.get_constructor_accessors(cnstr); + ptr_vector const & cnstr_acc = *m_dt_util.get_constructor_accessors(cnstr); unsigned num_cas = cnstr_acc.size(); for (unsigned j = 0; j < num_cas; j++) { func_decl * accsr = cnstr_acc.get(j); diff --git a/src/ast/rewriter/datatype_rewriter.cpp b/src/ast/rewriter/datatype_rewriter.cpp index 8746fab86..9efa61f70 100644 --- a/src/ast/rewriter/datatype_rewriter.cpp +++ b/src/ast/rewriter/datatype_rewriter.cpp @@ -47,7 +47,7 @@ br_status datatype_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr func_decl * c_decl = a->get_decl(); if (c_decl != m_util.get_accessor_constructor(f)) return BR_FAILED; - ptr_vector const & acc = m_util.get_constructor_accessors(c_decl); + ptr_vector const & acc = *m_util.get_constructor_accessors(c_decl); SASSERT(acc.size() == a->get_num_args()); unsigned num = acc.size(); for (unsigned i = 0; i < num; ++i) { @@ -70,7 +70,7 @@ br_status datatype_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr result = a; return BR_DONE; } - ptr_vector const & acc = m_util.get_constructor_accessors(c_decl); + ptr_vector const & acc = *m_util.get_constructor_accessors(c_decl); SASSERT(acc.size() == a->get_num_args()); unsigned num = acc.size(); ptr_buffer new_args; diff --git a/src/ast/rewriter/enum2bv_rewriter.cpp b/src/ast/rewriter/enum2bv_rewriter.cpp index b2ecbcc24..eb6b195f0 100644 --- a/src/ast/rewriter/enum2bv_rewriter.cpp +++ b/src/ast/rewriter/enum2bv_rewriter.cpp @@ -130,7 +130,7 @@ struct enum2bv_rewriter::imp { m_imp.m_bounds.push_back(m_bv.mk_ule(result, m_bv.mk_numeral(nc-1, bv_size))); } expr_ref f_def(m); - ptr_vector const& cs = m_dt.get_datatype_constructors(s); + ptr_vector const& cs = *m_dt.get_datatype_constructors(s); f_def = m.mk_const(cs[nc-1]); for (unsigned i = nc - 1; i > 0; ) { --i; diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 109fe1718..21f1cfe27 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -682,8 +682,6 @@ bool cmd_context::logic_has_datatype() const { void cmd_context::init_manager_core(bool new_manager) { SASSERT(m_manager != 0); SASSERT(m_pmanager != 0); - m_dt_eh = alloc(dt_eh, *this); - m_pmanager->set_new_datatype_eh(m_dt_eh.get()); if (new_manager) { decl_plugin * basic = m_manager->get_plugin(m_manager->get_basic_family_id()); register_builtin_sorts(basic); @@ -719,6 +717,8 @@ void cmd_context::init_manager_core(bool new_manager) { } } } + m_dt_eh = alloc(dt_eh, *this); + m_pmanager->set_new_datatype_eh(m_dt_eh.get()); if (!has_logic()) { // add list type only if the logic is not specified. // it prevents clashes with builtin types. @@ -795,6 +795,7 @@ void cmd_context::insert(symbol const & s, func_decl * f) { dictionary::entry * e = m_func_decls.insert_if_not_there2(s, func_decls()); func_decls & fs = e->get_data().m_value; if (!fs.insert(m(), f)) { + UNREACHABLE(); std::string msg = "invalid declaration, "; msg += f->get_arity() == 0 ? "constant" : "function"; msg += " '"; @@ -1954,21 +1955,17 @@ cmd_context::dt_eh::~dt_eh() { void cmd_context::dt_eh::operator()(sort * dt, pdecl* pd) { TRACE("new_dt_eh", tout << "new datatype: "; m_owner.pm().display(tout, dt); tout << "\n";); - ptr_vector const & constructors = m_dt_util.get_datatype_constructors(dt); - unsigned num_constructors = constructors.size(); - for (unsigned j = 0; j < num_constructors; j++) { - func_decl * c = constructors[j]; - m_owner.insert(c); + for (func_decl * c : *m_dt_util.get_datatype_constructors(dt)) { TRACE("new_dt_eh", tout << "new constructor: " << c->get_name() << "\n";); + m_owner.insert(c); +#ifndef DATATYPE_V2 func_decl * r = m_dt_util.get_constructor_recognizer(c); m_owner.insert(r); TRACE("new_dt_eh", tout << "new recognizer: " << r->get_name() << "\n";); - ptr_vector const & accessors = m_dt_util.get_constructor_accessors(c); - unsigned num_accessors = accessors.size(); - for (unsigned k = 0; k < num_accessors; k++) { - func_decl * a = accessors[k]; - m_owner.insert(a); +#endif + for (func_decl * a : *m_dt_util.get_constructor_accessors(c)) { TRACE("new_dt_eh", tout << "new accessor: " << a->get_name() << "\n";); + m_owner.insert(a); } } if (m_owner.m_scopes.size() > 0) { diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp index 04456c076..4417061ec 100644 --- a/src/cmd_context/pdecl.cpp +++ b/src/cmd_context/pdecl.cpp @@ -170,9 +170,10 @@ public: virtual char const * hcons_kind() const { return "psort_var"; } virtual unsigned hcons_hash() const { return hash_u_u(m_num_params, m_idx); } virtual bool hcons_eq(psort const * other) const { - if (other->hcons_kind() != hcons_kind()) - return false; - return get_num_params() == other->get_num_params() && m_idx == static_cast(other)->m_idx; + return + other->hcons_kind() == hcons_kind() && + get_num_params() == other->get_num_params() && + m_idx == static_cast(other)->m_idx; } virtual void display(std::ostream & out) const { out << "s_" << m_idx; @@ -344,6 +345,53 @@ void psort_user_decl::display(std::ostream & out) const { out << ")"; } +// ------------------- +// psort_dt_decl + +psort_dt_decl::psort_dt_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n) : + psort_decl(id, num_params, m, n) { + m_psort_kind = PSORT_DT; +} + + +sort * psort_dt_decl::instantiate(pdecl_manager & m, unsigned n, sort * const * s) { +#ifndef DATATYPE_V2 + UNREACHABLE(); + return 0; +#else + SASSERT(n == m_num_params); + sort * r = find(s); + if (r) + return r; + buffer ps; + ps.push_back(parameter(m_name)); + for (unsigned i = 0; i < n; i++) + ps.push_back(parameter(s[i])); + datatype_util util(m.m()); + r = m.m().mk_sort(util.get_family_id(), DATATYPE_SORT, ps.size(), ps.c_ptr()); + cache(m, s, r); + m.save_info(r, this, n, s); + if (m_num_params > 0 && util.is_declared(r)) { + bool has_typevar = false; + // crude check .. + for (unsigned i = 0; !has_typevar && i < n; ++i) { + has_typevar = s[i]->get_name().is_numerical(); + } + if (!has_typevar) { + m.notify_new_dt(r, this); + } + } + return r; +#endif +} + +void psort_dt_decl::display(std::ostream & out) const { + out << "(datatype-sort " << m_name << ")"; +} + +// ------------------- +// psort_builtin_decl + psort_builtin_decl::psort_builtin_decl(unsigned id, pdecl_manager & m, symbol const & n, family_id fid, decl_kind k): psort_decl(id, PSORT_DECL_VAR_PARAMS, m, n), m_fid(fid), @@ -435,8 +483,8 @@ bool paccessor_decl::fix_missing_refs(dictionary const & symbol2idx, symbol accessor_decl * paccessor_decl::instantiate_decl(pdecl_manager & m, sort * const * s) { switch (m_type.kind()) { - case PTR_REC_REF: return mk_accessor_decl(m_name, type_ref(m_type.get_idx())); - case PTR_PSORT: return mk_accessor_decl(m_name, type_ref(m_type.get_psort()->instantiate(m, s))); + case PTR_REC_REF: return mk_accessor_decl(m.m(), m_name, type_ref(m_type.get_idx())); + case PTR_PSORT: return mk_accessor_decl(m.m(), m_name, type_ref(m_type.get_psort()->instantiate(m, s))); default: // missing refs must have been eliminated. UNREACHABLE(); @@ -546,7 +594,7 @@ datatype_decl * pdatatype_decl::instantiate_decl(pdecl_manager & m, sort * const cs.push_back(c->instantiate_decl(m, s)); } datatype_util util(m.m()); - return mk_datatype_decl(util, m_name, cs.size(), cs.c_ptr()); + return mk_datatype_decl(util, m_name, m_num_params, s, cs.size(), cs.c_ptr()); } struct datatype_decl_buffer { @@ -554,6 +602,12 @@ struct datatype_decl_buffer { ~datatype_decl_buffer() { del_datatype_decls(m_buffer.size(), m_buffer.c_ptr()); } }; +#ifdef DATATYPE_V2 +sort * pdatatype_decl::instantiate(pdecl_manager & m, unsigned n, sort * const * s) { + UNREACHABLE(); + return 0; +} +#else sort * pdatatype_decl::instantiate(pdecl_manager & m, unsigned n, sort * const * s) { SASSERT(m_num_params == n); sort * r = find(s); @@ -583,6 +637,7 @@ sort * pdatatype_decl::instantiate(pdecl_manager & m, unsigned n, sort * const * } return 0; } +#endif void pdatatype_decl::display(std::ostream & out) const { out << "(declare-datatype " << m_name; @@ -603,6 +658,27 @@ void pdatatype_decl::display(std::ostream & out) const { out << ")"; } +#ifdef DATATYPE_V2 +bool pdatatype_decl::commit(pdecl_manager& m) { + sort_ref_vector ps(m.m()); + for (unsigned i = 0; i < m_num_params; ++i) { + ps.push_back(m.m().mk_uninterpreted_sort(symbol(i), 0, 0)); + } + datatype_decl_buffer dts; + dts.m_buffer.push_back(instantiate_decl(m, ps.c_ptr())); + datatype_decl * d_ptr = dts.m_buffer[0]; + sort_ref_vector sorts(m.m()); + bool is_ok = m.get_dt_plugin()->mk_datatypes(1, &d_ptr, m_num_params, ps.c_ptr(), sorts); + if (is_ok) { + if (m_num_params == 0) { + m.notify_new_dt(sorts.get(0), this); + } + } + return is_ok; +} +#endif + + pdatatypes_decl::pdatatypes_decl(unsigned id, unsigned num_params, pdecl_manager & m, unsigned num_datatypes, pdatatype_decl * const * dts): pdecl(id, num_params), @@ -631,6 +707,12 @@ bool pdatatypes_decl::fix_missing_refs(symbol & missing) { return true; } +#ifdef DATATYPE_V2 +bool pdatatypes_decl::instantiate(pdecl_manager & m, sort * const * s) { + UNREACHABLE(); + return false; +} +#else bool pdatatypes_decl::instantiate(pdecl_manager & m, sort * const * s) { datatype_decl_buffer dts; for (auto d : m_datatypes) { @@ -649,6 +731,31 @@ bool pdatatypes_decl::instantiate(pdecl_manager & m, sort * const * s) { } return true; } +#endif + +#ifdef DATATYPE_V2 +bool pdatatypes_decl::commit(pdecl_manager& m) { + datatype_decl_buffer dts; + for (pdatatype_decl* d : m_datatypes) { + sort_ref_vector ps(m.m()); + for (unsigned i = 0; i < d->get_num_params(); ++i) { + ps.push_back(m.m().mk_uninterpreted_sort(symbol(i), 0, 0)); + } + dts.m_buffer.push_back(d->instantiate_decl(m, ps.c_ptr())); + } + sort_ref_vector sorts(m.m()); + bool is_ok = m.get_dt_plugin()->mk_datatypes(m_datatypes.size(), dts.m_buffer.c_ptr(), 0, nullptr, sorts); + if (is_ok) { + for (unsigned i = 0; i < m_datatypes.size(); ++i) { + pdatatype_decl* d = m_datatypes[i]; + if (d->get_num_params() == 0) { + m.notify_new_dt(sorts.get(i), this); + } + } + } + return is_ok; +} +#endif struct pdecl_manager::sort_info { psort_decl * m_decl; @@ -790,9 +897,8 @@ psort * pdecl_manager::register_psort(psort * n) { psort * r = m_table.insert_if_not_there(n); if (r != n) { del_decl_core(n); - return r; } - return n; + return r; } psort * pdecl_manager::mk_psort_var(unsigned num_params, unsigned vidx) { @@ -837,6 +943,11 @@ psort_decl * pdecl_manager::mk_psort_user_decl(unsigned num_params, symbol const return new (a().allocate(sizeof(psort_user_decl))) psort_user_decl(m_id_gen.mk(), num_params, *this, n, def); } +psort_decl * pdecl_manager::mk_psort_dt_decl(unsigned num_params, symbol const & n) { + // std::cout << "insert dt-psort: " << n << " " << num_params << "\n"; + return new (a().allocate(sizeof(psort_dt_decl))) psort_dt_decl(m_id_gen.mk(), num_params, *this, n); +} + psort_decl * pdecl_manager::mk_psort_builtin_decl(symbol const & n, family_id fid, decl_kind k) { return new (a().allocate(sizeof(psort_builtin_decl))) psort_builtin_decl(m_id_gen.mk(), *this, n, fid, k); diff --git a/src/cmd_context/pdecl.h b/src/cmd_context/pdecl.h index e7fae8dd5..414415255 100644 --- a/src/cmd_context/pdecl.h +++ b/src/cmd_context/pdecl.h @@ -87,7 +87,7 @@ typedef ptr_hashtable psort_table; #define PSORT_DECL_VAR_PARAMS UINT_MAX -typedef enum { PSORT_BASE = 0, PSORT_USER, PSORT_BUILTIN } psort_decl_kind; +typedef enum { PSORT_BASE = 0, PSORT_USER, PSORT_BUILTIN, PSORT_DT } psort_decl_kind; class psort_decl : public pdecl { protected: @@ -111,6 +111,7 @@ public: virtual void reset_cache(pdecl_manager& m); bool is_user_decl() const { return m_psort_kind == PSORT_USER; } bool is_builtin_decl() const { return m_psort_kind == PSORT_BUILTIN; } + bool is_dt_decl() const { return m_psort_kind == PSORT_DT; } }; class psort_user_decl : public psort_decl { @@ -125,7 +126,7 @@ public: virtual sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s); virtual void display(std::ostream & out) const; }; - + class psort_builtin_decl : public psort_decl { protected: friend class pdecl_manager; @@ -140,10 +141,17 @@ public: virtual void display(std::ostream & out) const; }; -//class datatype_decl_plugin; -//class datatype_decl; -//class constructor_decl; -//class accessor_decl; +class psort_dt_decl : public psort_decl { +protected: + friend class pdecl_manager; + psort_dt_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n); + virtual size_t obj_size() const { return sizeof(psort_dt_decl); } + virtual ~psort_dt_decl() {} +public: + virtual sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s); + virtual void display(std::ostream & out) const; +}; + class pdatatypes_decl; class pdatatype_decl; @@ -233,6 +241,9 @@ public: virtual void display(std::ostream & out) const; bool has_missing_refs(symbol & missing) const; bool has_duplicate_accessors(symbol & repeated) const; +#ifdef DATATYPE_V2 + bool commit(pdecl_manager& m); +#endif }; /** @@ -250,6 +261,10 @@ class pdatatypes_decl : public pdecl { virtual ~pdatatypes_decl() {} public: pdatatype_decl const * const * children() const { return m_datatypes.c_ptr(); } +#ifdef DATATYPE_V2 + // commit declaration + bool commit(pdecl_manager& m); +#endif }; class new_datatype_eh { @@ -292,7 +307,7 @@ public: psort * mk_psort_var(unsigned num_params, unsigned vidx); psort * mk_psort_app(unsigned num_params, psort_decl * d, unsigned num_args, psort * const * args); psort * mk_psort_app(psort_decl * d); - // psort_decl * mk_psort_dt_decl(unsigned num_params, symbol const & n); + psort_decl * mk_psort_dt_decl(unsigned num_params, symbol const & n); psort_decl * mk_psort_user_decl(unsigned num_params, symbol const & n, psort * def); psort_decl * mk_psort_builtin_decl(symbol const & n, family_id fid, decl_kind k); paccessor_decl * mk_paccessor_decl(unsigned num_params, symbol const & s, ptype const & p); diff --git a/src/muz/base/dl_rule.h b/src/muz/base/dl_rule.h index 51d673ba5..ea0e64e4f 100644 --- a/src/muz/base/dl_rule.h +++ b/src/muz/base/dl_rule.h @@ -65,7 +65,7 @@ namespace datalog { else if (m_dt.is_accessor(n)) { sort* s = m.get_sort(n->get_arg(0)); SASSERT(m_dt.is_datatype(s)); - if (m_dt.get_datatype_constructors(s).size() > 1) { + if (m_dt.get_datatype_constructors(s)->size() > 1) { m_found = true; m_func = n->get_decl(); } diff --git a/src/muz/base/rule_properties.cpp b/src/muz/base/rule_properties.cpp index 75487bbfb..21317a07c 100644 --- a/src/muz/base/rule_properties.cpp +++ b/src/muz/base/rule_properties.cpp @@ -191,7 +191,7 @@ void rule_properties::operator()(app* n) { else if (m_dt.is_accessor(n)) { sort* s = m.get_sort(n->get_arg(0)); SASSERT(m_dt.is_datatype(s)); - if (m_dt.get_datatype_constructors(s).size() > 1) { + if (m_dt.get_datatype_constructors(s)->size() > 1) { m_uninterp_funs.insert(n->get_decl(), m_rule); } } diff --git a/src/muz/bmc/dl_bmc_engine.cpp b/src/muz/bmc/dl_bmc_engine.cpp index 9109f6b3c..3368c7640 100644 --- a/src/muz/bmc/dl_bmc_engine.cpp +++ b/src/muz/bmc/dl_bmc_engine.cpp @@ -808,7 +808,7 @@ namespace datalog { datatype_util dtu(m); ptr_vector sorts; func_decl* p = r.get_decl(); - ptr_vector const& succs = dtu.get_datatype_constructors(m.get_sort(path)); + ptr_vector const& succs = *dtu.get_datatype_constructors(m.get_sort(path)); // populate substitution of bound variables. r.get_vars(m, sorts); sub.reset(); @@ -871,8 +871,8 @@ namespace datalog { path_var = m.mk_var(0, m_path_sort); trace_var = m.mk_var(1, pred_sort); // sort* sorts[2] = { pred_sort, m_path_sort }; - ptr_vector const& cnstrs = dtu.get_datatype_constructors(pred_sort); - ptr_vector const& succs = dtu.get_datatype_constructors(m_path_sort); + ptr_vector const& cnstrs = *dtu.get_datatype_constructors(pred_sort); + ptr_vector const& succs = *dtu.get_datatype_constructors(m_path_sort); SASSERT(cnstrs.size() == rls.size()); pred = m.mk_app(mk_predicate(p), trace_var.get(), path_var.get()); for (unsigned i = 0; i < rls.size(); ++i) { @@ -970,7 +970,7 @@ namespace datalog { _name << pred->get_name() << "_" << q->get_name() << j; symbol name(_name.str().c_str()); type_ref tr(idx); - accs.push_back(mk_accessor_decl(name, tr)); + accs.push_back(mk_accessor_decl(m, name, tr)); } std::stringstream _name; _name << pred->get_name() << "_" << i; @@ -979,7 +979,7 @@ namespace datalog { symbol is_name(_name.str().c_str()); cnstrs.push_back(mk_constructor_decl(name, is_name, accs.size(), accs.c_ptr())); } - dts.push_back(mk_datatype_decl(dtu, pred->get_name(), cnstrs.size(), cnstrs.c_ptr())); + dts.push_back(mk_datatype_decl(dtu, pred->get_name(), 0, nullptr, cnstrs.size(), cnstrs.c_ptr())); } @@ -1024,10 +1024,10 @@ namespace datalog { _name2 << "get_succ#" << i; ptr_vector accs; type_ref tr(0); - accs.push_back(mk_accessor_decl(name, tr)); + accs.push_back(mk_accessor_decl(m, name, tr)); cnstrs.push_back(mk_constructor_decl(name, is_name, accs.size(), accs.c_ptr())); } - dts.push_back(mk_datatype_decl(dtu, symbol("Path"), cnstrs.size(), cnstrs.c_ptr())); + dts.push_back(mk_datatype_decl(dtu, symbol("Path"), 0, nullptr, cnstrs.size(), cnstrs.c_ptr())); VERIFY (dtp->mk_datatypes(dts.size(), dts.c_ptr(), 0, 0, new_sorts)); m_path_sort = new_sorts[0].get(); } @@ -1039,8 +1039,8 @@ namespace datalog { sort* trace_sort = m.get_sort(trace); func_decl* p = m_sort2pred.find(trace_sort); datalog::rule_vector const& rules = b.m_rules.get_predicate_rules(p); - ptr_vector const& cnstrs = dtu.get_datatype_constructors(trace_sort); - ptr_vector const& succs = dtu.get_datatype_constructors(m_path_sort); + ptr_vector const& cnstrs = *dtu.get_datatype_constructors(trace_sort); + ptr_vector const& succs = *dtu.get_datatype_constructors(m_path_sort); for (unsigned i = 0; i < cnstrs.size(); ++i) { if (trace->get_decl() == cnstrs[i]) { svector > positions; diff --git a/src/muz/pdr/pdr_prop_solver.cpp b/src/muz/pdr/pdr_prop_solver.cpp index 1bca8e925..3055985f4 100644 --- a/src/muz/pdr/pdr_prop_solver.cpp +++ b/src/muz/pdr/pdr_prop_solver.cpp @@ -135,7 +135,7 @@ namespace pdr { func_decl* f = to_app(val)->get_decl(); func_decl* r = dt.get_constructor_recognizer(f); conjs[i] = m.mk_app(r, c); - ptr_vector const& acc = dt.get_constructor_accessors(f); + ptr_vector const& acc = *dt.get_constructor_accessors(f); for (unsigned j = 0; j < acc.size(); ++j) { conjs.push_back(m.mk_eq(apply_accessor(acc, j, f, c), to_app(val)->get_arg(j))); } diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp index 14d8899c5..a277c9ed6 100644 --- a/src/muz/spacer/spacer_util.cpp +++ b/src/muz/spacer/spacer_util.cpp @@ -711,7 +711,7 @@ void expand_literals(ast_manager &m, expr_ref_vector& conjs) func_decl* f = to_app(val)->get_decl(); func_decl* r = dt.get_constructor_recognizer(f); conjs[i] = m.mk_app(r, c); - ptr_vector const& acc = dt.get_constructor_accessors(f); + ptr_vector const& acc = *dt.get_constructor_accessors(f); for (unsigned j = 0; j < acc.size(); ++j) { conjs.push_back(m.mk_eq(apply_accessor(m, acc, j, f, c), to_app(val)->get_arg(j))); } diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 3d895668b..9526429cb 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -16,8 +16,6 @@ Author: Revision History: --*/ -#include "parsers/smt2/smt2parser.h" -#include "parsers/smt2/smt2scanner.h" #include "util/stack.h" #include "ast/datatype_decl_plugin.h" #include "ast/bv_decl_plugin.h" @@ -25,10 +23,12 @@ Revision History: #include "ast/seq_decl_plugin.h" #include "ast/ast_pp.h" #include "ast/well_sorted.h" -#include "parsers/util/pattern_validation.h" #include "ast/rewriter/rewriter.h" #include "ast/has_free_vars.h" #include "ast/ast_smt2_pp.h" +#include "parsers/smt2/smt2parser.h" +#include "parsers/smt2/smt2scanner.h" +#include "parsers/util/pattern_validation.h" #include "parsers/util/parser_params.hpp" #include @@ -885,6 +885,9 @@ namespace smt2 { } else if (sz == 1) { check_missing(new_dt_decls[0], line, pos); +#ifdef DATATYPE_V2 + new_dt_decls[0]->commit(pm()); +#endif } else { SASSERT(sz > 1); @@ -897,8 +900,13 @@ namespace smt2 { err_msg += "'"; throw parser_exception(err_msg, line, pos); } +#ifndef DATATYPE_V2 m_ctx.insert_aux_pdecl(dts.get()); +#else + dts->commit(pm()); +#endif } +#ifndef DATATYPE_V2 for (unsigned i = 0; i < sz; i++) { pdatatype_decl * d = new_dt_decls[i]; SASSERT(d != 0); @@ -911,6 +919,13 @@ namespace smt2 { s = d->instantiate(pm(), 0, 0); } } +#else + for (unsigned i = 0; i < sz; i++) { + pdatatype_decl * d = new_dt_decls[i]; + symbol duplicated; + check_duplicate(d, line, pos); + } +#endif TRACE("declare_datatypes", tout << "i: " << i << " new_dt_decls.size(): " << sz << "\n"; for (unsigned i = 0; i < sz; i++) tout << new_dt_decls[i]->get_name() << "\n";); m_ctx.print_success(); @@ -940,12 +955,16 @@ namespace smt2 { check_missing(d, line, pos); check_duplicate(d, line, pos); +#ifndef DATATYPE_V2 m_ctx.insert(d); if (d->get_num_params() == 0) { // if datatype is not parametric... then force instantiation to register accessor, recognizers and constructors... sort_ref s(m()); s = d->instantiate(pm(), 0, 0); } +#else + d->commit(pm()); +#endif check_rparen_next("invalid end of datatype declaration, ')' expected"); m_ctx.print_success(); } @@ -1909,6 +1928,8 @@ namespace smt2 { m_dt_name2idx.insert(dt_name, i); m_dt_name2arity.insert(dt_name, u); m_dt_names.push_back(dt_name); + psort_decl * decl = pm().mk_psort_dt_decl(u, dt_name); + m_ctx.insert(decl); check_rparen("invalid sort declaration, ')' expected"); } else { diff --git a/src/qe/qe_datatype_plugin.cpp b/src/qe/qe_datatype_plugin.cpp index eff230ffe..c3525aa33 100644 --- a/src/qe/qe_datatype_plugin.cpp +++ b/src/qe/qe_datatype_plugin.cpp @@ -262,7 +262,7 @@ namespace qe { } func_decl* c = a->get_decl(); func_decl* r = m_util.get_constructor_recognizer(c); - ptr_vector const & acc = m_util.get_constructor_accessors(c); + ptr_vector const & acc = *m_util.get_constructor_accessors(c); SASSERT(acc.size() == a->get_num_args()); // // It suffices to solve just the first available equality. @@ -379,7 +379,7 @@ namespace qe { return false; } func_decl* c = l->get_decl(); - ptr_vector const& acc = m_util.get_constructor_accessors(c); + ptr_vector const& acc = *m_util.get_constructor_accessors(c); func_decl* rec = m_util.get_constructor_recognizer(c); expr_ref_vector conj(m); conj.push_back(m.mk_app(rec, r)); @@ -626,7 +626,7 @@ namespace qe { // If 'x' does not yet have a recognizer, then branch according to recognizers. // if (!has_recognizer(x, fml, r, c)) { - c = m_datatype_util.get_datatype_constructors(s)[vl.get_unsigned()]; + c = m_datatype_util.get_datatype_constructors(s)->get(vl.get_unsigned()); r = m_datatype_util.get_constructor_recognizer(c); app* is_c = m.mk_app(r, x); // assert v => r(x) @@ -673,7 +673,7 @@ namespace qe { // Introduce auxiliary variable to eliminate. // if (!has_recognizer(x, fml, r, c)) { - c = m_datatype_util.get_datatype_constructors(s)[vl.get_unsigned()]; + c = m_datatype_util.get_datatype_constructors(s)->get(vl.get_unsigned()); r = m_datatype_util.get_constructor_recognizer(c); app* is_c = m.mk_app(r, x); fml = m.mk_and(is_c, fml); @@ -774,7 +774,7 @@ namespace qe { return; } - c = m_datatype_util.get_datatype_constructors(s)[vl.get_unsigned()]; + c = m_datatype_util.get_datatype_constructors(s)->get(vl.get_unsigned()); r = m_datatype_util.get_constructor_recognizer(c); app* is_c = m.mk_app(r, x); @@ -794,7 +794,7 @@ namespace qe { else { SASSERT(vl.is_unsigned()); SASSERT(vl.get_unsigned() < m_datatype_util.get_datatype_num_constructors(s)); - c = m_datatype_util.get_datatype_constructors(s)[vl.get_unsigned()]; + c = m_datatype_util.get_datatype_constructors(s)->get(vl.get_unsigned()); } subst_constructor(x, c, fml, def); } diff --git a/src/qe/qe_datatypes.cpp b/src/qe/qe_datatypes.cpp index f16bdda59..db1e6ec85 100644 --- a/src/qe/qe_datatypes.cpp +++ b/src/qe/qe_datatypes.cpp @@ -75,7 +75,7 @@ namespace qe { app_ref arg(m); SASSERT(dt.is_constructor(m_val)); func_decl* f = m_val->get_decl(); - ptr_vector const& acc = dt.get_constructor_accessors(f); + ptr_vector const& acc = *dt.get_constructor_accessors(f); for (unsigned i = 0; i < acc.size(); ++i) { arg = m.mk_fresh_const(acc[i]->get_name().str().c_str(), acc[i]->get_range()); model.register_decl(arg->get_decl(), m_val->get_arg(i)); @@ -152,7 +152,7 @@ namespace qe { } func_decl* c = a->get_decl(); func_decl* rec = dt.get_constructor_recognizer(c); - ptr_vector const & acc = dt.get_constructor_accessors(c); + ptr_vector const & acc = *dt.get_constructor_accessors(c); SASSERT(acc.size() == a->get_num_args()); // // It suffices to solve just the first available equality. @@ -230,7 +230,7 @@ namespace qe { return false; } func_decl* c = to_app(l)->get_decl(); - ptr_vector const& acc = dt.get_constructor_accessors(c); + ptr_vector const& acc = *dt.get_constructor_accessors(c); if (!is_app_of(r, c)) { lits.push_back(m.mk_app(dt.get_constructor_recognizer(c), r)); } diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index 10af3be25..257331161 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -671,7 +671,7 @@ namespace eq { else { func_decl* rec = dt.get_constructor_recognizer(d); conjs.push_back(m.mk_app(rec, r)); - ptr_vector const& acc = dt.get_constructor_accessors(d); + ptr_vector const& acc = *dt.get_constructor_accessors(d); for (unsigned i = 0; i < acc.size(); ++i) { conjs.push_back(m.mk_eq(c->get_arg(i), m.mk_app(acc[i], r))); } diff --git a/src/smt/proto_model/datatype_factory.cpp b/src/smt/proto_model/datatype_factory.cpp index 653ef034a..03f008fe6 100644 --- a/src/smt/proto_model/datatype_factory.cpp +++ b/src/smt/proto_model/datatype_factory.cpp @@ -88,7 +88,7 @@ expr * datatype_factory::get_almost_fresh_value(sort * s) { // Traverse constructors, and try to invoke get_fresh_value of one of the arguments (if the argument is not a sibling datatype of s). // If the argumet is a sibling datatype of s, then // use get_last_fresh_value. - ptr_vector const & constructors = m_util.get_datatype_constructors(s); + ptr_vector const & constructors = *m_util.get_datatype_constructors(s); for (func_decl * constructor : constructors) { expr_ref_vector args(m_manager); bool found_fresh_arg = false; @@ -151,7 +151,7 @@ expr * datatype_factory::get_fresh_value(sort * s) { // Traverse constructors, and try to invoke get_fresh_value of one of the // arguments (if the argument is not a sibling datatype of s). // Two datatypes are siblings if they were defined together in the same mutually recursive definition. - ptr_vector const & constructors = m_util.get_datatype_constructors(s); + ptr_vector const & constructors = *m_util.get_datatype_constructors(s); for (func_decl * constructor : constructors) { expr_ref_vector args(m_manager); bool found_fresh_arg = false; @@ -189,7 +189,7 @@ expr * datatype_factory::get_fresh_value(sort * s) { while(true) { ++num_iterations; TRACE("datatype_factory", tout << mk_pp(get_last_fresh_value(s), m_manager) << "\n";); - ptr_vector const & constructors = m_util.get_datatype_constructors(s); + ptr_vector const & constructors = *m_util.get_datatype_constructors(s); for (func_decl * constructor : constructors) { expr_ref_vector args(m_manager); bool found_sibling = false; diff --git a/src/smt/smt_value_sort.cpp b/src/smt/smt_value_sort.cpp index 3eeb3461d..56768b91a 100644 --- a/src/smt/smt_value_sort.cpp +++ b/src/smt/smt_value_sort.cpp @@ -52,7 +52,7 @@ namespace smt { // simple } else if (data.is_datatype(s)) { - ptr_vector const& cs = data.get_datatype_constructors(s); + ptr_vector const& cs = *data.get_datatype_constructors(s); for (unsigned i = 0; i < cs.size(); ++i) { func_decl* f = cs[i]; for (unsigned j = 0; j < f->get_arity(); ++j) { diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index 33b4b194d..616314117 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -17,13 +17,13 @@ Revision History: --*/ +#include "util/stats.h" +#include "ast/ast_pp.h" +#include "ast/ast_ll_pp.h" +#include "ast/ast_smt2_pp.h" #include "smt/smt_context.h" #include "smt/theory_datatype.h" #include "smt/smt_model_generator.h" -#include "ast/ast_pp.h" -#include "ast/ast_ll_pp.h" -#include "util/stats.h" -#include "ast/ast_smt2_pp.h" namespace smt { @@ -97,7 +97,7 @@ namespace smt { SASSERT(m_util.is_datatype(get_manager().get_sort(n->get_owner()))); ast_manager & m = get_manager(); ptr_vector args; - ptr_vector const & accessors = m_util.get_constructor_accessors(c); + ptr_vector const & accessors = *m_util.get_constructor_accessors(c); SASSERT(c->get_arity() == accessors.size()); for (func_decl * d : accessors) { SASSERT(d->get_arity() == 1); @@ -120,7 +120,7 @@ namespace smt { SASSERT(is_constructor(n)); ast_manager & m = get_manager(); func_decl * d = n->get_decl(); - ptr_vector const & accessors = m_util.get_constructor_accessors(d); + ptr_vector const & accessors = *m_util.get_constructor_accessors(d); SASSERT(n->get_num_args() == accessors.size()); unsigned i = 0; for (func_decl * acc : accessors) { @@ -168,7 +168,7 @@ namespace smt { func_decl * acc = to_func_decl(upd->get_parameter(0).get_ast()); func_decl * con = m_util.get_accessor_constructor(acc); func_decl * rec = m_util.get_constructor_recognizer(con); - ptr_vector const & accessors = m_util.get_constructor_accessors(con); + ptr_vector const & accessors = *m_util.get_constructor_accessors(con); app_ref rec_app(m.mk_app(rec, arg1), m); ctx.internalize(rec_app, false); literal is_con(ctx.get_bool_var(rec_app)); @@ -208,7 +208,7 @@ namespace smt { ast_manager & m = get_manager(); sort * s = m.get_sort(n->get_owner()); if (m_util.get_datatype_num_constructors(s) == 1) { - func_decl * c = m_util.get_datatype_constructors(s)[0]; + func_decl * c = m_util.get_datatype_constructors(s)->get(0); assert_is_constructor_axiom(n, c, null_literal); } else { @@ -709,7 +709,7 @@ namespace smt { enode * r = d->m_recognizers[unassigned_idx]; literal consequent; if (!r) { - ptr_vector const & constructors = m_util.get_datatype_constructors(dt); + ptr_vector const & constructors = *m_util.get_datatype_constructors(dt); func_decl * rec = m_util.get_constructor_recognizer(constructors[unassigned_idx]); app * rec_app = get_manager().mk_app(rec, n->get_owner()); ctx.internalize(rec_app, false); @@ -774,7 +774,7 @@ namespace smt { for (unsigned idx = 0; it != end; ++it, ++idx) { enode * curr = *it; if (curr == 0) { - ptr_vector const & constructors = m_util.get_datatype_constructors(s); + ptr_vector const & constructors = *m_util.get_datatype_constructors(s); // found empty slot... r = m_util.get_constructor_recognizer(constructors[idx]); break; @@ -793,7 +793,7 @@ namespace smt { } SASSERT(r != 0); app * r_app = m.mk_app(r, n->get_owner()); - TRACE("datatype", tout << "creating split: " << mk_bounded_pp(r_app, m) << "\n";); + TRACE("datatype", tout << "creating split: " << mk_pp(r_app, m) << "\n";); ctx.internalize(r_app, false); bool_var bv = ctx.get_bool_var(r_app); ctx.set_true_first_flag(bv); diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp index a13cd54d8..6a38f787e 100644 --- a/src/tactic/core/elim_uncnstr_tactic.cpp +++ b/src/tactic/core/elim_uncnstr_tactic.cpp @@ -174,7 +174,7 @@ class elim_uncnstr_tactic : public tactic { if (fid == m_dt_util.get_family_id()) { // In the current implementation, I only handle the case where // the datatype has a recursive constructor. - ptr_vector const & constructors = m_dt_util.get_datatype_constructors(s); + ptr_vector const & constructors = *m_dt_util.get_datatype_constructors(s); for (func_decl * constructor : constructors) { unsigned num = constructor->get_arity(); unsigned target = UINT_MAX; @@ -704,7 +704,7 @@ class elim_uncnstr_tactic : public tactic { app * u; if (!mk_fresh_uncnstr_var_for(f, num, args, u)) return u; - ptr_vector const & accs = m_dt_util.get_constructor_accessors(c); + ptr_vector const & accs = *m_dt_util.get_constructor_accessors(c); ptr_buffer new_args; for (unsigned i = 0; i < accs.size(); i++) { if (accs[i] == f) @@ -723,7 +723,7 @@ class elim_uncnstr_tactic : public tactic { return u; if (!m_mc) return u; - ptr_vector const & accs = m_dt_util.get_constructor_accessors(f); + ptr_vector const & accs = *m_dt_util.get_constructor_accessors(f); for (unsigned i = 0; i < num; i++) { add_def(args[i], m().mk_app(accs[i], u)); } diff --git a/src/tactic/portfolio/enum2bv_solver.cpp b/src/tactic/portfolio/enum2bv_solver.cpp index db7cebd6e..36a178c41 100644 --- a/src/tactic/portfolio/enum2bv_solver.cpp +++ b/src/tactic/portfolio/enum2bv_solver.cpp @@ -136,7 +136,7 @@ public: if (m.is_eq(b, u, v) && is_uninterp_const(u) && m_rewriter.bv2enum().find(to_app(u)->get_decl(), f) && bv.is_numeral(v, num, bvsize)) { SASSERT(num.is_unsigned()); expr_ref head(m); - ptr_vector const& enums = dt.get_datatype_constructors(f->get_range()); + ptr_vector const& enums = *dt.get_datatype_constructors(f->get_range()); if (enums.size() > num.get_unsigned()) { head = m.mk_eq(m.mk_const(f), m.mk_const(enums[num.get_unsigned()])); consequences[i] = m.mk_implies(a, head);