From 7f127cdd5dfc2a21433e64e19a5e91ab344648c4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 6 Sep 2017 09:48:10 -0700 Subject: [PATCH] adding declarations for regression tests Signed-off-by: Nikolaj Bjorner --- src/ast/datatype_decl_plugin2.cpp | 1 + src/ast/datatype_decl_plugin2.h | 2 +- src/cmd_context/pdecl.cpp | 99 +++++++++++++++++-------------- src/cmd_context/pdecl.h | 3 + src/parsers/smt2/smt2parser.cpp | 1 + 5 files changed, 62 insertions(+), 44 deletions(-) diff --git a/src/ast/datatype_decl_plugin2.cpp b/src/ast/datatype_decl_plugin2.cpp index b53a2743f..43164a436 100644 --- a/src/ast/datatype_decl_plugin2.cpp +++ b/src/ast/datatype_decl_plugin2.cpp @@ -346,6 +346,7 @@ namespace datatype { begin_def_block(); for (unsigned i = 0; i < num_datatypes; ++i) { def* d = 0; + TRACE("datatype", tout << "declaring " << datatypes[i]->name() << "\n";); if (m_defs.find(datatypes[i]->name(), d)) { TRACE("datatype", tout << "delete previous version for " << datatypes[i]->name() << "\n";); dealloc(d); diff --git a/src/ast/datatype_decl_plugin2.h b/src/ast/datatype_decl_plugin2.h index d9a069de3..a88c7100e 100644 --- a/src/ast/datatype_decl_plugin2.h +++ b/src/ast/datatype_decl_plugin2.h @@ -334,7 +334,6 @@ namespace datatype { void compute_datatype_size_functions(svector const& names); param_size::size* get_sort_size(sort_ref_vector const& params, sort* s); bool is_well_founded(unsigned num_types, sort* const* sorts); - def const& get_def(sort* s) const; def& get_def(symbol const& s) { return m_plugin->get_def(s); } void get_subsorts(sort* s, ptr_vector& sorts) const; @@ -380,6 +379,7 @@ namespace datatype { unsigned get_recognizer_constructor_idx(func_decl * f) const; decl::plugin* get_plugin() { return m_plugin; } void get_defs(sort* s, ptr_vector& defs); + def const& get_def(sort* s) const; }; }; diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp index 2293072a2..95a6030f3 100644 --- a/src/cmd_context/pdecl.cpp +++ b/src/cmd_context/pdecl.cpp @@ -360,28 +360,7 @@ sort * psort_dt_decl::instantiate(pdecl_manager & m, unsigned n, sort * const * 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; + return m.instantiate_datatype(this, m_name, n, s); #endif } @@ -603,32 +582,39 @@ struct datatype_decl_buffer { }; #ifdef DATATYPE_V2 + sort * pdatatype_decl::instantiate(pdecl_manager & m, unsigned n, sort * const * s) { - // TBD: copied - 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])); + sort * r = m.instantiate_datatype(this, m_name, n, s); 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); + if (r && n > 0 && util.is_declared(r)) { + ast_mark mark; + datatype::def const& d = util.get_def(r); + mark.mark(r, true); + sort_ref_vector params(m.m(), n, s); + for (datatype::constructor* c : d) { + for (datatype::accessor* a : *c) { + sort* rng = a->range(); + if (util.is_datatype(rng) && !mark.is_marked(rng) && m_parent) { + mark.mark(rng, true); + // TBD: search over more than just parents + for (pdatatype_decl* p : *m_parent) { + if (p->get_name() == rng->get_name()) { + ptr_vector ps; + func_decl_ref acc = a->instantiate(params); + for (unsigned j = 0; j < util.get_datatype_num_parameter_sorts(rng); ++j) { + ps.push_back(util.get_datatype_parameter_sort(acc->get_range(), j)); + } + m.instantiate_datatype(p, p->get_name(), ps.size(), ps.c_ptr()); + break; + } + } + } + } } } return r; } + #else sort * pdatatype_decl::instantiate(pdecl_manager & m, unsigned n, sort * const * s) { SASSERT(m_num_params == n); @@ -729,6 +715,33 @@ bool pdatatypes_decl::fix_missing_refs(symbol & missing) { } #ifdef DATATYPE_V2 +sort* pdecl_manager::instantiate_datatype(psort_decl* p, symbol const& name, unsigned n, sort * const* s) { + TRACE("datatype", tout << name << " "; for (unsigned i = 0; i < n; ++i) tout << s[i]->get_name() << " "; tout << "\n";); + pdecl_manager& m = *this; + sort * r = p->find(s); + if (r) + return r; + buffer ps; + ps.push_back(parameter(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()); + p->cache(m, s, r); + m.save_info(r, p, n, s); + if (n > 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, p); + } + } + return r; +} + bool pdatatypes_decl::instantiate(pdecl_manager & m, sort * const * s) { UNREACHABLE(); return false; @@ -887,6 +900,7 @@ void pdecl_manager::init_list() { mk_pconstructor_decl(1, symbol("insert"), symbol("is-insert"), 2, as) }; m_list = mk_pdatatype_decl(1, symbol("List"), 2, cs); inc_ref(m_list); + m_list->commit(*this); } pdecl_manager::pdecl_manager(ast_manager & m): @@ -966,7 +980,6 @@ psort_decl * pdecl_manager::mk_psort_user_decl(unsigned num_params, symbol const } 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); } diff --git a/src/cmd_context/pdecl.h b/src/cmd_context/pdecl.h index 414415255..bef723380 100644 --- a/src/cmd_context/pdecl.h +++ b/src/cmd_context/pdecl.h @@ -261,6 +261,8 @@ class pdatatypes_decl : public pdecl { virtual ~pdatatypes_decl() {} public: pdatatype_decl const * const * children() const { return m_datatypes.c_ptr(); } + pdatatype_decl * const * begin() const { return m_datatypes.begin(); } + pdatatype_decl * const * end() const { return m_datatypes.end(); } #ifdef DATATYPE_V2 // commit declaration bool commit(pdecl_manager& m); @@ -316,6 +318,7 @@ public: pdatatypes_decl * mk_pdatatypes_decl(unsigned num_params, unsigned num, pdatatype_decl * const * dts); pdatatype_decl * mk_plist_decl() { if (!m_list) init_list(); return m_list; } bool fix_missing_refs(pdatatypes_decl * s, symbol & missing) { return s->fix_missing_refs(missing); } + sort * instantiate_datatype(psort_decl* p, symbol const& name, unsigned n, sort * const* s); sort * instantiate(psort * s, unsigned num, sort * const * args); void lazy_dec_ref(pdecl * p) { p->dec_ref(); if (p->get_ref_count() == 0) m_to_delete.push_back(p); } diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 7bfc8bd99..ab2eecb36 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -897,6 +897,7 @@ namespace smt2 { m_ctx.insert_aux_pdecl(dts.get()); #else dts->commit(pm()); + m_ctx.insert_aux_pdecl(dts.get()); #endif } #ifndef DATATYPE_V2