#5952

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)

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;

src/cmd_context/pdecl.cpp

@@ -156,8 +156,8 @@ public:
             return false;
         return m_sort == static_cast<psort_sort const *>(other)->m_sort;
     }
-    void display(std::ostream & out) const override {
+    std::ostream& display(std::ostream & out) const override {
-        out << m_sort->get_name();
+        return out << m_sort->get_name();
     }
 };
 
@@ -180,8 +180,8 @@ public:
             get_num_params() == other->get_num_params() && 
             m_idx == static_cast<psort_var const *>(other)->m_idx;
     }
-    void display(std::ostream & out) const override {
+    std::ostream& display(std::ostream & out) const override {
-        out << "s_" << m_idx;
+        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 {
+std::ostream& psort_dt_decl::display(std::ostream & out) const {
-    out << "(datatype-sort " << m_name << ")";
+    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 {
+std::ostream& psort_builtin_decl::display(std::ostream & out) const {
-    out << "(declare-builtin-sort " << m_name << ")";
+    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;
 
@@ -989,12 +1011,15 @@ void pdecl_manager::del_decl(pdecl * p) {
     if (p->is_psort()) {
         psort * _p = static_cast<psort*>(p);
         if (_p->is_sort_wrapper()) {
-            m_sort2psort.erase(static_cast<psort_sort*>(_p)->get_sort());
+            sort* s = static_cast<psort_sort*>(_p)->get_sort();
+            m_sort2psort.erase(s);
         }
         else {
             m_table.erase(_p);
         }
+
     }
+
     del_decl_core(p);
 }
 

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<sort>          m_notified;
     ptr_vector<sort>             m_notified_trail;
     unsigned_vector              m_notified_lim;
+    svector<symbol>              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);