From a3dba5b2f97341269e205dbfb18d4c127e084f56 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 3 Sep 2017 20:01:59 -0700 Subject: [PATCH] hide new datatype plugin Signed-off-by: Nikolaj Bjorner --- src/api/api_datatype.cpp | 107 +++++++++-------------- src/ast/ast_smt_pp.cpp | 17 ++-- src/ast/datatype_decl_plugin.cpp | 37 ++++---- src/ast/datatype_decl_plugin.h | 11 ++- src/ast/datatype_decl_plugin2.cpp | 12 ++- src/ast/datatype_decl_plugin2.h | 74 ++++++++++++---- src/ast/decl_collector.cpp | 4 +- src/ast/rewriter/datatype_rewriter.cpp | 16 ++-- src/ast/rewriter/enum2bv_rewriter.cpp | 2 +- src/cmd_context/cmd_context.cpp | 12 +-- src/muz/base/dl_rule.h | 2 +- src/muz/base/rule_properties.cpp | 2 +- src/muz/bmc/dl_bmc_engine.cpp | 10 +-- src/muz/pdr/pdr_prop_solver.cpp | 2 +- src/muz/spacer/spacer_util.cpp | 2 +- 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 | 12 +-- src/smt/smt_value_sort.cpp | 2 +- src/smt/theory_datatype.cpp | 37 ++++---- src/tactic/core/elim_uncnstr_tactic.cpp | 17 ++-- src/tactic/portfolio/enum2bv_solver.cpp | 2 +- src/test/get_consequences.cpp | 2 +- 24 files changed, 211 insertions(+), 191 deletions(-) diff --git a/src/api/api_datatype.cpp b/src/api/api_datatype.cpp index 851d96a4e..39d147ed1 100644 --- a/src/api/api_datatype.cpp +++ b/src/api/api_datatype.cpp @@ -69,18 +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); - func_decl* decl = (*decls)[0]; + 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); - if (!accs) { - SET_ERROR_CODE(Z3_INVALID_ARG); - RETURN_Z3(0); - } - ptr_vector const & _accs = *accs; + 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]); @@ -136,10 +131,10 @@ 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); - SASSERT(decls && decls->size() == n); + 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]; + func_decl* decl = (decls)[i]; mk_c(c)->save_multiple_ast_trail(decl); enum_consts[i] = of_func_decl(decl); decl = dt_util.get_constructor_recognizer(decl); @@ -191,7 +186,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) { @@ -215,18 +210,16 @@ extern "C" { *is_cons_decl = of_func_decl(f); } if (head_decl) { - ptr_vector const* acc = data_util.get_constructor_accessors(cnstrs[1]); - SASSERT(acc); - SASSERT(acc->size() == 2); - f = (*acc)[0]; + 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]); - SASSERT(acc); - SASSERT(acc->size() == 2); - f = (*acc)[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); *tail_decl = of_func_decl(f); } @@ -301,13 +294,9 @@ extern "C" { *tester = of_func_decl(f2); } - ptr_vector const* accs = data_util.get_constructor_accessors(f); - if (!accs && num_fields > 0) { - SET_ERROR_CODE(Z3_INVALID_ARG); - return; - } + ptr_vector const& accs = data_util.get_constructor_accessors(f); for (unsigned i = 0; i < num_fields; ++i) { - func_decl* f2 = (*accs)[i]; + func_decl* f2 = (accs)[i]; mk_c(c)->save_multiple_ast_trail(f2); accessors[i] = of_func_decl(f2); } @@ -368,11 +357,11 @@ 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]); - cn->m_constructor = (*cnstrs)[i]; + cn->m_constructor = cnstrs[i]; } RETURN_Z3_mk_datatype(of_sort(s)); Z3_CATCH_RETURN(0); @@ -434,10 +423,10 @@ 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]; + cn->m_constructor = cnstrs[j]; } } RETURN_Z3_mk_datatypes; @@ -456,12 +445,7 @@ extern "C" { SET_ERROR_CODE(Z3_INVALID_ARG); return 0; } - ptr_vector const * decls = dt_util.get_datatype_constructors(_t); - if (!decls) { - SET_ERROR_CODE(Z3_INVALID_ARG); - return 0; - } - return decls->size(); + return dt_util.get_datatype_constructors(_t).size(); Z3_CATCH_RETURN(0); } @@ -474,12 +458,12 @@ extern "C" { SET_ERROR_CODE(Z3_INVALID_ARG); return 0; } - ptr_vector const * decls = dt_util.get_datatype_constructors(_t); - if (!decls || idx >= decls->size()) { + ptr_vector const & decls = dt_util.get_datatype_constructors(_t); + if (idx >= decls.size()) { SET_ERROR_CODE(Z3_INVALID_ARG); return 0; } - func_decl* decl = (*decls)[idx]; + func_decl* decl = (decls)[idx]; mk_c(c)->save_ast_trail(decl); return of_func_decl(decl); } @@ -504,12 +488,12 @@ extern "C" { SET_ERROR_CODE(Z3_INVALID_ARG); RETURN_Z3(0); } - ptr_vector const * decls = dt_util.get_datatype_constructors(_t); - if (!decls || idx >= decls->size()) { + ptr_vector const & decls = dt_util.get_datatype_constructors(_t); + if (idx >= decls.size()) { SET_ERROR_CODE(Z3_INVALID_ARG); RETURN_Z3(0); } - func_decl* decl = (*decls)[idx]; + func_decl* decl = (decls)[idx]; decl = dt_util.get_constructor_recognizer(decl); mk_c(c)->save_ast_trail(decl); RETURN_Z3(of_func_decl(decl)); @@ -527,23 +511,23 @@ extern "C" { SET_ERROR_CODE(Z3_INVALID_ARG); RETURN_Z3(0); } - ptr_vector const * decls = dt_util.get_datatype_constructors(_t); - if (!decls || idx_c >= decls->size()) { + ptr_vector const & decls = dt_util.get_datatype_constructors(_t); + if (idx_c >= decls.size()) { SET_ERROR_CODE(Z3_INVALID_ARG); return 0; } - func_decl* decl = (*decls)[idx_c]; + func_decl* decl = (decls)[idx_c]; if (decl->get_arity() <= idx_a) { SET_ERROR_CODE(Z3_INVALID_ARG); RETURN_Z3(0); } - ptr_vector const * accs = dt_util.get_constructor_accessors(decl); - SASSERT(accs && accs->size() == decl->get_arity()); - if (!accs || accs->size() <= idx_a) { + 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); RETURN_Z3(0); } - decl = (*accs)[idx_a]; + decl = (accs)[idx_a]; mk_c(c)->save_ast_trail(decl); RETURN_Z3(of_func_decl(decl)); Z3_CATCH_RETURN(0); @@ -574,16 +558,13 @@ extern "C" { SET_ERROR_CODE(Z3_INVALID_ARG); return 0; } - ptr_vector const * decls = dt_util.get_datatype_constructors(tuple); - if (!decls || decls->size() != 1) { + 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]); - if (!accs) { - return 0; - } - return accs->size(); + ptr_vector const & accs = dt_util.get_constructor_accessors(decls[0]); + return accs.size(); Z3_CATCH_RETURN(0); } @@ -597,21 +578,17 @@ extern "C" { SET_ERROR_CODE(Z3_INVALID_ARG); RETURN_Z3(0); } - ptr_vector const * decls = dt_util.get_datatype_constructors(tuple); - if (!decls || decls->size() != 1) { + 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]); - if (!accs) { - SET_ERROR_CODE(Z3_INVALID_ARG); - RETURN_Z3(0); - } - if (accs->size() <= i) { + ptr_vector const & accs = dt_util.get_constructor_accessors((decls)[0]); + if (accs.size() <= i) { SET_ERROR_CODE(Z3_IOB); RETURN_Z3(0); } - func_decl* acc = (*accs)[i]; + func_decl* acc = (accs)[i]; mk_c(c)->save_ast_trail(acc); RETURN_Z3(of_func_decl(acc)); Z3_CATCH_RETURN(0); diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp index 9ebfdfbef..9211c5899 100644 --- a/src/ast/ast_smt_pp.cpp +++ b/src/ast/ast_smt_pp.cpp @@ -907,7 +907,6 @@ public: void pp_dt(ast_mark& mark, sort* s) { SASSERT(s->is_sort_of(m_dt_fid, DATATYPE_SORT)); datatype_util util(m_manager); - ptr_vector const* decls; ptr_vector rec_sorts; rec_sorts.push_back(s); @@ -916,10 +915,10 @@ public: // collect siblings and sorts that have not already been printed. for (unsigned h = 0; h < rec_sorts.size(); ++h) { s = rec_sorts[h]; - 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]; + for (unsigned i = 0; i < decls.size(); ++i) { + func_decl* f = decls[i]; for (unsigned j = 0; j < f->get_arity(); ++j) { sort* s2 = f->get_domain(j); if (!mark.is_marked(s2)) { @@ -955,11 +954,11 @@ public: m_out << "("; m_out << m_renaming.get_symbol(s->get_name()); m_out << " "; - 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); + for (unsigned i = 0; i < decls.size(); ++i) { + func_decl* f = decls[i]; + ptr_vector const& accs = util.get_constructor_accessors(f); if (m_is_smt2 || accs.size() > 0) { m_out << "("; } @@ -976,7 +975,7 @@ public: } if (m_is_smt2 || accs.size() > 0) { m_out << ")"; - if (i + 1 < decls->size()) { + if (i + 1 < decls.size()) { m_out << " "; } } diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 446992105..e2aa54236 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -20,6 +20,7 @@ Revision History: #include "util/warning.h" #include "ast/ast_smt2_pp.h" +#ifndef DATATYPE_V2 /** \brief Auxiliary class used to declare inductive datatypes. @@ -802,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); @@ -819,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; } /** @@ -854,12 +855,12 @@ 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(); + unsigned sz = constructors.size(); ++m_start; for (unsigned j = 0; j < sz; ++j) { - func_decl * c = (*constructors)[(j + m_start) % sz]; + func_decl * c = constructors[(j + m_start) % sz]; unsigned num_args = c->get_arity(); unsigned i = 0; for (; i < num_args; i++) { @@ -872,7 +873,7 @@ func_decl * datatype_util::get_non_rec_constructor_core(sort * ty, ptr_vectorget_name() << "\n";); unsigned num_args = c->get_arity(); unsigned i = 0; @@ -915,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); @@ -938,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) { @@ -988,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; @@ -1048,14 +1049,14 @@ 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); - for (unsigned i = 0; i < cnstrs->size(); ++i) { - func_decl* cns = (*cnstrs)[i]; + 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); - for (unsigned j = 0; j < accs->size(); ++j) { - func_decl* acc = (*accs)[j]; + 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(); strm << "(" << acc->get_name() << ": " << s1->get_name() << ") "; if (is_datatype(s1) && are_siblings(s1, s0) && !mark.is_marked(s1)) { @@ -1090,3 +1091,5 @@ bool datatype_util::is_constructor_of(unsigned num_params, parameter const* para params[1] == f->get_parameter(1); } + +#endif diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h index dcd352471..b9c2602ef 100644 --- a/src/ast/datatype_decl_plugin.h +++ b/src/ast/datatype_decl_plugin.h @@ -16,9 +16,15 @@ Author: Revision History: --*/ +// define DATATYPE_V2 +#ifdef DATATYPE_V2 +#include "ast/datatype_decl_plugin2.h" +#else + #ifndef DATATYPE_DECL_PLUGIN_H_ #define DATATYPE_DECL_PLUGIN_H_ + #include "ast/ast.h" #include "util/tptr.h" #include "util/buffer.h" @@ -210,7 +216,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(); @@ -230,7 +236,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; } @@ -245,3 +251,4 @@ public: #endif /* DATATYPE_DECL_PLUGIN_H_ */ +#endif /* DATATYPE_V2 */ diff --git a/src/ast/datatype_decl_plugin2.cpp b/src/ast/datatype_decl_plugin2.cpp index 8233da7d9..2fc62af31 100644 --- a/src/ast/datatype_decl_plugin2.cpp +++ b/src/ast/datatype_decl_plugin2.cpp @@ -22,6 +22,7 @@ Revision History: #include "ast/ast_smt2_pp.h" +#ifdef DATATYPE_V2 namespace datatype { void accessor::fix_range(sort_ref_vector const& dts) { @@ -49,6 +50,10 @@ namespace datatype { def const& accessor::get_def() const { return m_constructor->get_def(); } util& accessor::u() const { return m_constructor->u(); } + constructor::~constructor() { + for (accessor* a : m_accessors) dealloc(a); + m_accessors.reset(); + } util& constructor::u() const { return m_def->u(); } func_decl_ref constructor::instantiate(sort_ref_vector const& ps) const { @@ -164,7 +169,7 @@ namespace datatype { sort* r = to_sort(parameters[i].get_ast()); S.insert(d->params()[i], r->get_num_elements()); } - sort_size ts = d->sort_size()->fold(S); + sort_size ts = d->sort_size()->eval(S); s->set_num_elements(ts); } return s; @@ -278,7 +283,9 @@ namespace datatype { def& plugin::add(symbol const& name, unsigned n, sort * const * params) { ast_manager& m = *m_manager; - def* d = alloc(def, m, u(), name, m_class_id, n, params); + def* d = 0; + if (m_defs.find(name, d)) 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; @@ -895,3 +902,4 @@ namespace datatype { } } } +#endif diff --git a/src/ast/datatype_decl_plugin2.h b/src/ast/datatype_decl_plugin2.h index c540b7c1c..c8aa042f1 100644 --- a/src/ast/datatype_decl_plugin2.h +++ b/src/ast/datatype_decl_plugin2.h @@ -24,17 +24,12 @@ Revision History: #include "util/symbol_table.h" #include "util/obj_hashtable.h" -namespace datatype { - - class util; - class def; - class accessor; - class constructor; +#ifdef DATATYPE_V2 enum sort_kind { DATATYPE_SORT }; - + enum op_kind { OP_DT_CONSTRUCTOR, OP_DT_RECOGNISER, @@ -43,6 +38,14 @@ namespace datatype { LAST_DT_OP }; +namespace datatype { + + class util; + class def; + class accessor; + class constructor; + + class accessor { symbol m_name; sort* m_range; @@ -109,7 +112,7 @@ namespace datatype { static size* mk_power(size* a1, size* a2); virtual size* subst(obj_map& S) = 0; - virtual sort_size fold(obj_map const& S) = 0; + virtual sort_size eval(obj_map const& S) = 0; }; struct offset : public size { @@ -117,16 +120,16 @@ namespace datatype { offset(sort_size const& s): m_offset(s) {} virtual ~offset() {} virtual size* subst(obj_map& S) { return this; } - virtual sort_size fold(obj_map const& S) { return m_offset; } + virtual sort_size eval(obj_map const& S) { return m_offset; } }; struct plus : public size { size* m_arg1, *m_arg2; plus(size* a1, size* a2): m_arg1(a1), m_arg2(a2) { a1->inc_ref(); a2->inc_ref();} virtual ~plus() { m_arg1->dec_ref(); m_arg2->dec_ref(); } virtual size* subst(obj_map& S) { return mk_plus(m_arg1->subst(S), m_arg2->subst(S)); } - virtual sort_size fold(obj_map const& S) { - sort_size s1 = m_arg1->fold(S); - sort_size s2 = m_arg2->fold(S); + virtual sort_size eval(obj_map const& S) { + sort_size s1 = m_arg1->eval(S); + sort_size s2 = m_arg2->eval(S); if (s1.is_infinite()) return s1; if (s2.is_infinite()) return s2; if (s1.is_very_big()) return s1; @@ -140,9 +143,9 @@ namespace datatype { times(size* a1, size* a2): m_arg1(a1), m_arg2(a2) { a1->inc_ref(); a2->inc_ref(); } virtual ~times() { m_arg1->dec_ref(); m_arg2->dec_ref(); } virtual size* subst(obj_map& S) { return mk_times(m_arg1->subst(S), m_arg2->subst(S)); } - virtual sort_size fold(obj_map const& S) { - sort_size s1 = m_arg1->fold(S); - sort_size s2 = m_arg2->fold(S); + virtual sort_size eval(obj_map const& S) { + sort_size s1 = m_arg1->eval(S); + sort_size s2 = m_arg2->eval(S); if (s1.is_infinite()) return s1; if (s2.is_infinite()) return s2; if (s1.is_very_big()) return s1; @@ -156,9 +159,9 @@ namespace datatype { power(size* a1, size* a2): m_arg1(a1), m_arg2(a2) { a1->inc_ref(); a2->inc_ref(); } virtual ~power() { m_arg1->dec_ref(); m_arg2->dec_ref(); } virtual size* subst(obj_map& S) { return mk_power(m_arg1->subst(S), m_arg2->subst(S)); } - virtual sort_size fold(obj_map const& S) { - sort_size s1 = m_arg1->fold(S); - sort_size s2 = m_arg2->fold(S); + virtual sort_size eval(obj_map const& S) { + sort_size s1 = m_arg1->eval(S); + sort_size s2 = m_arg2->eval(S); // s1^s2 if (s1.is_infinite()) return s1; if (s2.is_infinite()) return s2; @@ -176,7 +179,7 @@ namespace datatype { sparam(sort_ref& p): m_param(p) {} virtual ~sparam() {} virtual size* subst(obj_map& S) { return S[m_param]; } - virtual sort_size fold(obj_map const& S) { return S[m_param]; } + virtual sort_size eval(obj_map const& S) { return S[m_param]; } }; }; @@ -201,6 +204,8 @@ namespace datatype { {} ~def() { if (m_sort_size) m_sort_size->dec_ref(); + for (constructor* c : m_constructors) dealloc(c); + m_constructors.reset(); } void add(constructor* c) { m_constructors.push_back(c); @@ -361,5 +366,36 @@ namespace datatype { }; +#ifdef DATATYPE_V2 +typedef datatype::accessor accessor_decl; +typedef datatype::constructor constructor_decl; +typedef datatype::def datatype_decl; +typedef datatype::decl::plugin datatype_decl_plugin; +typedef datatype::util datatype_util; + +class type_ref { + void * m_data; +public: + type_ref():m_data(TAG(void *, static_cast(0), 1)) {} + type_ref(int idx):m_data(BOXINT(void *, idx)) {} + type_ref(sort * s):m_data(TAG(void *, s, 1)) {} + + bool is_idx() const { return GET_TAG(m_data) == 0; } + bool is_sort() const { return GET_TAG(m_data) == 1; } + sort * get_sort() const { return UNTAG(sort *, m_data); } + int get_idx() const { return UNBOXINT(m_data); } +}; + +inline accessor_decl * mk_accessor_decl(symbol const & n, type_ref const & t) { + if (t.is_idx()) { + return alloc(accessor_decl, n, t.get_idx()); + } + else { + return alloc(accessor_decl, n, t.get_sort()); + } +} +#endif + #endif /* DATATYPE_DECL_PLUGIN_H_ */ +#endif DATATYPE_V2 diff --git a/src/ast/decl_collector.cpp b/src/ast/decl_collector.cpp index e000f43df..bf509aba5 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 d38c9e476..8746fab86 100644 --- a/src/ast/rewriter/datatype_rewriter.cpp +++ b/src/ast/rewriter/datatype_rewriter.cpp @@ -47,11 +47,11 @@ 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); - SASSERT(acc && acc->size() == a->get_num_args()); - unsigned num = acc->size(); + 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) { - if (f == (*acc)[i]) { + if (f == acc[i]) { // found it. result = a->get_arg(i); return BR_DONE; @@ -70,13 +70,13 @@ 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); - SASSERT(acc && acc->size() == a->get_num_args()); - unsigned num = acc->size(); + 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; for (unsigned i = 0; i < num; ++i) { - if (f == (*acc)[i]) { + if (f == acc[i]) { new_args.push_back(args[1]); } else { diff --git a/src/ast/rewriter/enum2bv_rewriter.cpp b/src/ast/rewriter/enum2bv_rewriter.cpp index eb6b195f0..b2ecbcc24 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 8b1a89f3f..109fe1718 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1954,19 +1954,19 @@ 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(); + 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->get(j); + func_decl * c = constructors[j]; m_owner.insert(c); TRACE("new_dt_eh", tout << "new constructor: " << c->get_name() << "\n";); 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(); + 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->get(k); + func_decl * a = accessors[k]; m_owner.insert(a); TRACE("new_dt_eh", tout << "new accessor: " << a->get_name() << "\n";); } diff --git a/src/muz/base/dl_rule.h b/src/muz/base/dl_rule.h index ea0e64e4f..51d673ba5 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 21317a07c..75487bbfb 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 6d2f88019..b9dbe83ca 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) { @@ -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 3055985f4..1bca8e925 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 a277c9ed6..14d8899c5 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/qe/qe_datatype_plugin.cpp b/src/qe/qe_datatype_plugin.cpp index 4178c3af3..eff230ffe 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)[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)[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)[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)[vl.get_unsigned()]; } subst_constructor(x, c, fml, def); } diff --git a/src/qe/qe_datatypes.cpp b/src/qe/qe_datatypes.cpp index db1e6ec85..f16bdda59 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 257331161..10af3be25 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 d738f2cbd..653ef034a 100644 --- a/src/smt/proto_model/datatype_factory.cpp +++ b/src/smt/proto_model/datatype_factory.cpp @@ -88,8 +88,8 @@ 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); - for (func_decl * constructor : *constructors) { + 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; bool recursive = false; @@ -151,8 +151,8 @@ 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); - for (func_decl * constructor : *constructors) { + 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; unsigned num = constructor->get_arity(); @@ -189,8 +189,8 @@ 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); - for (func_decl * constructor : *constructors) { + 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; unsigned num = constructor->get_arity(); diff --git a/src/smt/smt_value_sort.cpp b/src/smt/smt_value_sort.cpp index 56768b91a..3eeb3461d 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 beb1acf63..33b4b194d 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -97,12 +97,9 @@ 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); - SASSERT(c->get_arity() == accessors->size()); - ptr_vector::const_iterator it = accessors->begin(); - ptr_vector::const_iterator end = accessors->end(); - for (; it != end; ++it) { - func_decl * d = *it; + 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); expr * acc = m.mk_app(d, n->get_owner()); args.push_back(acc); @@ -123,15 +120,14 @@ 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); - SASSERT(n->get_num_args() == accessors->size()); - ptr_vector::const_iterator it = accessors->begin(); - ptr_vector::const_iterator end = accessors->end(); - for (unsigned i = 0; it != end; ++it, ++i) { - func_decl * acc = *it; + 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) { app * acc_app = m.mk_app(acc, n->get_owner()); enode * arg = n->get_arg(i); assert_eq_axiom(arg, acc_app, null_literal); + ++i; } } @@ -172,15 +168,12 @@ 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_iterator it = accessors->begin(); - ptr_vector::const_iterator end = accessors->end(); + 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)); - for (; it != end; ++it) { + for (func_decl* acc1 : accessors) { enode* arg; - func_decl * acc1 = *it; if (acc1 == acc) { arg = n->get_arg(1); } @@ -215,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)->get(0); + func_decl * c = m_util.get_datatype_constructors(s)[0]; assert_is_constructor_axiom(n, c, null_literal); } else { @@ -716,8 +709,8 @@ namespace smt { enode * r = d->m_recognizers[unassigned_idx]; literal consequent; if (!r) { - ptr_vector const * constructors = m_util.get_datatype_constructors(dt); - func_decl * rec = m_util.get_constructor_recognizer(constructors->get(unassigned_idx)); + 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); consequent = literal(ctx.get_bool_var(rec_app)); @@ -781,9 +774,9 @@ 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->get(idx)); + r = m_util.get_constructor_recognizer(constructors[idx]); break; } else if (!ctx.is_relevant(curr)) { diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp index 73adabb6f..a13cd54d8 100644 --- a/src/tactic/core/elim_uncnstr_tactic.cpp +++ b/src/tactic/core/elim_uncnstr_tactic.cpp @@ -174,11 +174,8 @@ 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_iterator it = constructors->begin(); - ptr_vector::const_iterator end = constructors->end(); - for (; it != end; ++it) { - func_decl * constructor = *it; + 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; for (unsigned i = 0; i < num; i++) { @@ -707,10 +704,10 @@ 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->get(i) == f) + for (unsigned i = 0; i < accs.size(); i++) { + if (accs[i] == f) new_args.push_back(u); else new_args.push_back(m().get_some_value(c->get_domain(i))); @@ -726,9 +723,9 @@ 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->get(i), u)); + add_def(args[i], m().mk_app(accs[i], u)); } return u; } diff --git a/src/tactic/portfolio/enum2bv_solver.cpp b/src/tactic/portfolio/enum2bv_solver.cpp index 36a178c41..db7cebd6e 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); diff --git a/src/test/get_consequences.cpp b/src/test/get_consequences.cpp index 9337dcee3..e8868c661 100644 --- a/src/test/get_consequences.cpp +++ b/src/test/get_consequences.cpp @@ -71,7 +71,7 @@ void test2() { sort* rgb = new_sorts[0].get(); expr_ref x = mk_const(m, "x", rgb), y = mk_const(m, "y", rgb), z = mk_const(m, "z", rgb); - ptr_vector const& enums = *dtutil.get_datatype_constructors(rgb); + ptr_vector const& enums = dtutil.get_datatype_constructors(rgb); expr_ref r = expr_ref(m.mk_const(enums[0]), m); expr_ref g = expr_ref(m.mk_const(enums[1]), m); expr_ref b = expr_ref(m.mk_const(enums[2]), m);