From 1346a168a1346405a313c2a9eceb2560576f8e02 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Apr 2022 07:00:53 +0200 Subject: [PATCH] #5952 --- src/cmd_context/cmd_context.cpp | 1 + src/cmd_context/cmd_context.h | 1 + src/cmd_context/pdecl.cpp | 59 +++++++++++++++++++++++---------- src/cmd_context/pdecl.h | 17 ++++++---- 4 files changed, 54 insertions(+), 24 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 89efc439f..580cc2de4 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1636,6 +1636,7 @@ void cmd_context::pop(unsigned n) { restore_aux_pdecls(s.m_aux_pdecls_lim); restore_assertions(s.m_assertions_lim); restore_psort_inst(s.m_psort_inst_stack_lim); + m_dt_eh.get()->reset(); m_mcs.shrink(m_mcs.size() - n); m_scopes.shrink(new_lvl); if (!m_global_decls) diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 4f9d80a8d..60a6e930b 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -267,6 +267,7 @@ protected: cmd_context & m_owner; datatype_util m_dt_util; public: + void reset() { m_dt_util.reset(); } dt_eh(cmd_context & owner); ~dt_eh() override; void operator()(sort * dt, pdecl* pd) override; diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp index 7a93382e9..2bf21de3a 100644 --- a/src/cmd_context/pdecl.cpp +++ b/src/cmd_context/pdecl.cpp @@ -156,8 +156,8 @@ public: return false; return m_sort == static_cast(other)->m_sort; } - void display(std::ostream & out) const override { - out << m_sort->get_name(); + std::ostream& display(std::ostream & out) const override { + return out << m_sort->get_name(); } }; @@ -180,8 +180,8 @@ public: get_num_params() == other->get_num_params() && m_idx == static_cast(other)->m_idx; } - void display(std::ostream & out) const override { - out << "s_" << m_idx; + std::ostream& display(std::ostream & out) const override { + return out << "s_" << m_idx; } unsigned idx() const { return m_idx; } }; @@ -254,7 +254,7 @@ public: } return true; } - void display(std::ostream & out) const override { + std::ostream& display(std::ostream & out) const override { if (m_args.empty()) { out << m_decl->get_name(); } @@ -267,6 +267,7 @@ public: } out << ")"; } + return out; } }; @@ -342,12 +343,12 @@ void display_sort_args(std::ostream & out, unsigned num_params) { out << ") "; } -void psort_user_decl::display(std::ostream & out) const { +std::ostream& psort_user_decl::display(std::ostream & out) const { out << "(declare-sort " << m_name; display_sort_args(out, m_num_params); if (m_def) m_def->display(out); - out << ")"; + return out << ")"; } // ------------------- @@ -364,8 +365,8 @@ sort * psort_dt_decl::instantiate(pdecl_manager & m, unsigned n, sort * const * return m.instantiate_datatype(this, m_name, n, s); } -void psort_dt_decl::display(std::ostream & out) const { - out << "(datatype-sort " << m_name << ")"; +std::ostream& psort_dt_decl::display(std::ostream & out) const { + return out << "(datatype-sort " << m_name << ")"; } // ------------------- @@ -410,8 +411,8 @@ sort * psort_builtin_decl::instantiate(pdecl_manager & m, unsigned n, unsigned c } } -void psort_builtin_decl::display(std::ostream & out) const { - out << "(declare-builtin-sort " << m_name << ")"; +std::ostream& psort_builtin_decl::display(std::ostream & out) const { + return out << "(declare-builtin-sort " << m_name << ")"; } void ptype::display(std::ostream & out, pdatatype_decl const * const * dts) const { @@ -615,7 +616,7 @@ sort * pdatatype_decl::instantiate(pdecl_manager & m, unsigned n, sort * const * } -void pdatatype_decl::display(std::ostream & out) const { +std::ostream& pdatatype_decl::display(std::ostream & out) const { out << "(declare-datatype " << m_name; display_sort_args(out, m_num_params); bool first = true; @@ -631,7 +632,7 @@ void pdatatype_decl::display(std::ostream & out) const { } first = false; } - out << ")"; + return out << ")"; } bool pdatatype_decl::commit(pdecl_manager& m) { @@ -645,9 +646,11 @@ bool pdatatype_decl::commit(pdecl_manager& m) { 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.data(), sorts); + m.notify_mk_datatype(m_name); if (is_ok && m_num_params == 0) { m.notify_new_dt(sorts.get(0), this); } + return is_ok; } @@ -722,6 +725,7 @@ void pdecl_manager::notify_datatype(sort *r, psort_decl* p, unsigned n, sort* co void pdecl_manager::push() { m_notified_lim.push_back(m_notified_trail.size()); + m_datatypes_lim.push_back(m_datatypes_trail.size()); } void pdecl_manager::pop(unsigned n) { @@ -732,6 +736,16 @@ void pdecl_manager::pop(unsigned n) { } m_notified_trail.shrink(new_sz); m_notified_lim.shrink(m_notified_lim.size() - n); + + new_sz = m_datatypes_lim[m_datatypes_lim.size() - n]; + if (new_sz != m_datatypes_trail.size()) { + datatype_util util(m()); + for (unsigned i = m_datatypes_trail.size(); i-- > new_sz; ) + util.plugin().remove(m_datatypes_trail[i]); + } + m_datatypes_trail.shrink(new_sz); + m_datatypes_lim.shrink(m_datatypes_lim.size() - n); + } bool pdatatypes_decl::instantiate(pdecl_manager & m, sort * const * s) { @@ -751,16 +765,24 @@ bool pdatatypes_decl::commit(pdecl_manager& m) { sort_ref_vector sorts(m.m()); bool is_ok = m.get_dt_plugin()->mk_datatypes(m_datatypes.size(), dts.m_buffer.data(), 0, nullptr, sorts); if (is_ok) { + for (pdatatype_decl* d : m_datatypes) { + m.notify_mk_datatype(d->get_name()); + } for (unsigned i = 0; i < m_datatypes.size(); ++i) { pdatatype_decl* d = m_datatypes[i]; - if (d->get_num_params() == 0) { + if (d->get_num_params() == 0) m.notify_new_dt(sorts.get(i), this); - } } } + return is_ok; } +void pdecl_manager::notify_mk_datatype(symbol const& name) { + m_datatypes_trail.push_back(name); +} + + struct pdecl_manager::sort_info { psort_decl * m_decl; @@ -985,16 +1007,19 @@ void pdecl_manager::del_decl_core(pdecl * p) { } void pdecl_manager::del_decl(pdecl * p) { - TRACE("pdecl_manager", tout << "del psort "; p->display(tout); tout << "\n";); + TRACE("pdecl_manager", tout << "del psort "; p->display(tout); tout << "\n";); if (p->is_psort()) { psort * _p = static_cast(p); if (_p->is_sort_wrapper()) { - m_sort2psort.erase(static_cast(_p)->get_sort()); + sort* s = static_cast(_p)->get_sort(); + m_sort2psort.erase(s); } else { m_table.erase(_p); } + } + del_decl_core(p); } diff --git a/src/cmd_context/pdecl.h b/src/cmd_context/pdecl.h index 3a1db06c1..4f9c56825 100644 --- a/src/cmd_context/pdecl.h +++ b/src/cmd_context/pdecl.h @@ -45,7 +45,7 @@ public: unsigned get_id() const { return m_id; } unsigned get_ref_count() const { return m_ref_count; } unsigned hash() const { return m_id; } - virtual void display(std::ostream & out) const {} + virtual std::ostream& display(std::ostream & out) const { return out;} virtual void reset_cache(pdecl_manager& m) {} }; @@ -123,7 +123,7 @@ protected: ~psort_user_decl() override {} public: sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override; - void display(std::ostream & out) const override; + std::ostream& display(std::ostream & out) const override; }; class psort_builtin_decl : public psort_decl { @@ -137,7 +137,7 @@ protected: public: sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override; sort * instantiate(pdecl_manager & m, unsigned n, unsigned const * s) override; - void display(std::ostream & out) const override; + std::ostream& display(std::ostream & out) const override; }; class psort_dt_decl : public psort_decl { @@ -148,7 +148,7 @@ protected: ~psort_dt_decl() override {} public: sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override; - void display(std::ostream & out) const override; + std::ostream& display(std::ostream & out) const override; }; @@ -198,7 +198,7 @@ class paccessor_decl : public pdecl { ptype const & get_type() const { return m_type; } ~paccessor_decl() override {} public: - void display(std::ostream & out) const override { pdecl::display(out); } + std::ostream& display(std::ostream & out) const override { pdecl::display(out); return out; } void display(std::ostream & out, pdatatype_decl const * const * dts) const; }; @@ -219,7 +219,7 @@ class pconstructor_decl : public pdecl { constructor_decl * instantiate_decl(pdecl_manager & m, unsigned n, sort * const * s); ~pconstructor_decl() override {} public: - void display(std::ostream & out) const override { pdecl::display(out); } + std::ostream& display(std::ostream & out) const override { pdecl::display(out); return out; } void display(std::ostream & out, pdatatype_decl const * const * dts) const; }; @@ -237,7 +237,7 @@ class pdatatype_decl : public psort_decl { ~pdatatype_decl() override {} public: sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override; - void display(std::ostream & out) const override; + std::ostream& display(std::ostream & out) const override; bool has_missing_refs(symbol & missing) const; bool has_duplicate_accessors(symbol & repeated) const; bool commit(pdecl_manager& m); @@ -289,6 +289,8 @@ class pdecl_manager { obj_hashtable m_notified; ptr_vector m_notified_trail; unsigned_vector m_notified_lim; + svector m_datatypes_trail; + unsigned_vector m_datatypes_lim; void init_list(); void del_decl_core(pdecl * p); @@ -319,6 +321,7 @@ public: sort * instantiate_datatype(psort_decl* p, symbol const& name, unsigned n, sort * const* s); sort * instantiate(psort * s, unsigned num, sort * const * args); void notify_datatype(sort *r, psort_decl* p, unsigned n, sort* const* s); + void notify_mk_datatype(symbol const& name); void push(); void pop(unsigned n);