fix: declare type variables before use in solver display output (#10103)

`decl_collector::visit_sort` did not collect sorts with `poly_family_id`
(type variables created via `mk_type_var` / `declare-type-var`), so
`solver::display` and `ast_pp_util::display_decls` never emitted type
variable declarations before referencing them — producing invalid
SMT-LIB2 output.

## Changes

- **`src/ast/decl_collector.h`**: added a dedicated `lim_svector<sort*>
m_type_vars` field (separate from `m_sorts`) with a `get_type_vars()`
getter; `reset()` clears it; `push()`/`pop()` maintain its scope.

- **`src/ast/decl_collector.cpp` — `visit_sort`**: sorts with
`poly_family_id` are now pushed to `m_type_vars` instead of `m_sorts`,
keeping type variables distinct from uninterpreted sorts:

```cpp
if (m.is_uninterp(n))
    m_sorts.push_back(n);
else if (fid == poly_family_id)
    m_type_vars.push_back(n);
```

- **`src/ast/ast_pp_util.h`**: added a `stacked_value<unsigned>
m_type_vars` cursor to track which type variables have already been
printed.

- **`src/ast/ast_pp_util.cpp` — `display_decls`**: emits
`(declare-type-var <name>)` for each collected type variable before
other sort declarations; `reset()`/`push()`/`pop()` maintain the new
cursor.

**Example** — given `(declare-type-var A)(declare-fun f (A) A)`, the
dump now correctly produces:

```smt2
(declare-type-var A)
(declare-fun f (A) A)
(assert ...)
```

The output round-trips cleanly through the Z3 parser.

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>

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

@@ -26,6 +26,8 @@ void decl_collector::visit_sort(sort * n) {
     family_id fid = n->get_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; }
 };