fix: add dedicated lim_svector<sort*> m_type_vars to decl_collector and emit declare-type-var in display_decls

- decl_collector.h: add m_type_vars lim_svector, get_type_vars() getter, update reset()
- decl_collector.cpp: push poly_family_id sorts to m_type_vars instead of m_sorts;
  push_scope/pop_scope m_type_vars in push()/pop()
- ast_pp_util.h: add stacked_value<unsigned> m_type_vars counter
- ast_pp_util.cpp: emit (declare-type-var <name>) before other sort declarations
  in display_decls(); reset/push/pop the new m_type_vars counter

src/ast/ast_pp_util.cpp

@@ -36,9 +36,14 @@ void ast_pp_util::collect(expr_ref_vector const& es) {
 }
 
 void ast_pp_util::display_decls(std::ostream& out) {
+    unsigned n = coll.get_type_vars().size();
+    for (unsigned i = m_type_vars; i < n; ++i)
+        out << "(declare-type-var " << coll.get_type_vars()[i]->get_name() << ")\n";
+    m_type_vars = n;
+
     ast_smt_pp pp(m);
     coll.order_deps(m_sorts);
-    unsigned n = coll.get_num_sorts();
+    n = coll.get_num_sorts();
     ast_mark seen;
     for (unsigned i = m_sorts; i < n; ++i) 
         pp.display_sort_decl(out, coll.get_sorts()[i], seen);
@@ -68,6 +73,7 @@ void ast_pp_util::reset() {
     coll.reset();
     m_removed.reset();
     m_sorts.clear(0u);
+    m_type_vars.clear(0u);
     m_decls.clear(0u);
     m_rec_decls.clear(0u); 
     m_is_defined.reset();
@@ -140,6 +146,7 @@ void ast_pp_util::push() {
     m_rec_decls.push();
     m_decls.push();
     m_sorts.push();
+    m_type_vars.push();
     m_defined_lim.push_back(m_defined.size());
 }
 
@@ -148,6 +155,7 @@ void ast_pp_util::pop(unsigned n) {
     m_rec_decls.pop(n);
     m_decls.pop(n);
     m_sorts.pop(n);
+    m_type_vars.pop(n);
     unsigned old_sz = m_defined_lim[m_defined_lim.size() - n];
     for (unsigned i = m_defined.size(); i-- > old_sz; ) 
         m_is_defined.mark(m_defined.get(i), false);

src/ast/ast_pp_util.h

@@ -30,6 +30,7 @@ class ast_pp_util {
     stacked_value<unsigned> m_rec_decls;
     stacked_value<unsigned> m_decls;
     stacked_value<unsigned> m_sorts;
+    stacked_value<unsigned> m_type_vars;
     expr_mark               m_is_defined;
     expr_ref_vector         m_defined;
     unsigned_vector         m_defined_lim;
@@ -38,7 +39,7 @@ class ast_pp_util {
 
     decl_collector      coll;
     
-    ast_pp_util(ast_manager& m): m(m), m_env(m), m_rec_decls(0), m_decls(0), m_sorts(0), m_defined(m), coll(m) {}
+    ast_pp_util(ast_manager& m): m(m), m_env(m), m_rec_decls(0), m_decls(0), m_sorts(0), m_type_vars(0), m_defined(m), coll(m) {}
 
     void reset();
 

src/ast/decl_collector.cpp

@@ -24,8 +24,10 @@ Revision History:
 void decl_collector::visit_sort(sort * n) {
     SASSERT(!m_visited.is_marked(n));
     family_id fid = n->get_family_id();
-    if (m.is_uninterp(n) || fid == poly_family_id)
+    if (m.is_uninterp(n))
         m_sorts.push_back(n);
+    else if (fid == poly_family_id)
+        m_type_vars.push_back(n);
     else if (fid == m_dt_fid) {
         m_sorts.push_back(n);
         for (func_decl * cnstr : *m_dt_util.get_datatype_constructors(n)) {
@@ -188,6 +190,7 @@ void decl_collector::collect_deps(sort* s, sort_set& set) {
 void decl_collector::push() {
     m_trail_lim.push_back(m_trail.size());
     m_sorts.push_scope();
+    m_type_vars.push_scope();
     m_decls.push_scope();
     m_rec_decls.push_scope();
 }
@@ -200,6 +203,7 @@ void decl_collector::pop(unsigned n) {
     m_trail.shrink(sz);
     m_trail_lim.shrink(m_trail_lim.size() - n);
     m_sorts.pop_scope(n);
+    m_type_vars.pop_scope(n);
     m_decls.pop_scope(n);
     m_rec_decls.pop_scope(n);
 }

src/ast/decl_collector.h

@@ -26,8 +26,9 @@ Revision History:
 #include "ast/array_decl_plugin.h"
 
 class decl_collector {
-    ast_manager &         m;
+    ast_manager &           m;
     lim_svector<sort*>      m_sorts;
+    lim_svector<sort*>      m_type_vars;
     lim_svector<func_decl*> m_decls;
     lim_svector<func_decl*> m_rec_decls;
     ast_mark              m_visited;
@@ -53,7 +54,7 @@ public:
 
     bool should_declare(func_decl* f) const;
 
-    void reset() { m_sorts.reset(); m_decls.reset(); m_visited.reset(); m_trail.reset(); }
+    void reset() { m_sorts.reset(); m_type_vars.reset(); m_decls.reset(); m_visited.reset(); m_trail.reset(); }
     void visit_func(func_decl* n);
     void visit(ast * n);
     void visit(unsigned n, expr* const* es);
@@ -68,6 +69,7 @@ public:
     unsigned get_num_decls() const { return m_decls.size(); }
     
     lim_svector<sort*> const& get_sorts() const { return m_sorts; }
+    lim_svector<sort*> const& get_type_vars() const { return m_type_vars; }
     lim_svector<func_decl*> const& get_func_decls() const { return m_decls; }
     lim_svector<func_decl*> const& get_rec_decls() const { return m_rec_decls; }
 };