adding declarations for regression tests

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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);

src/ast/datatype_decl_plugin2.h

@@ -334,7 +334,6 @@ namespace datatype {
         void compute_datatype_size_functions(svector<symbol> 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<sort>& 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<def>& defs);
+        def const& get_def(sort* s) const;
     };
 
 };

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);
+    return m.instantiate_datatype(this, m_name, n, s);
-    if (r)
-        return r;
-    buffer<parameter> 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
 }
 
@@ -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
+    sort * r = m.instantiate_datatype(this, m_name, n, s);
-    SASSERT(n == m_num_params);
-    sort * r = find(s);
-    if (r)
-        return r;
-    buffer<parameter> 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());
+    if (r && n > 0 && util.is_declared(r)) {
-    cache(m, s, r);
+        ast_mark mark;
-    m.save_info(r, this, n, s);
+        datatype::def const& d = util.get_def(r);
-    if (m_num_params > 0 && util.is_declared(r)) {
+        mark.mark(r, true);
-        bool has_typevar = false;
+        sort_ref_vector params(m.m(), n, s);
-        // crude check ..
+        for (datatype::constructor* c : d) {
-        for (unsigned i = 0; !has_typevar && i < n; ++i) {
+            for (datatype::accessor* a : *c) {
-            has_typevar = s[i]->get_name().is_numerical();
+                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<sort> 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;
+                        }
+                    }
+                }
             }
-        if (!has_typevar) {
-            m.notify_new_dt(r, this);
         }
     }
     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<parameter> 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);    
 }
 

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); }

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