From 1e07ca76afb8bbb634e8168476afeea32f38cf18 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 13 Jul 2026 03:27:16 +0000 Subject: [PATCH] fix: add dedicated lim_svector 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 m_type_vars counter - ast_pp_util.cpp: emit (declare-type-var ) before other sort declarations in display_decls(); reset/push/pop the new m_type_vars counter --- src/ast/ast_pp_util.cpp | 10 +++++++++- src/ast/ast_pp_util.h | 3 ++- src/ast/decl_collector.cpp | 6 +++++- src/ast/decl_collector.h | 6 ++++-- 4 files changed, 20 insertions(+), 5 deletions(-) diff --git a/src/ast/ast_pp_util.cpp b/src/ast/ast_pp_util.cpp index 2b7e72a919..d02956557d 100644 --- a/src/ast/ast_pp_util.cpp +++ b/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); diff --git a/src/ast/ast_pp_util.h b/src/ast/ast_pp_util.h index 9dbfec6afb..d1b91c1cf0 100644 --- a/src/ast/ast_pp_util.h +++ b/src/ast/ast_pp_util.h @@ -30,6 +30,7 @@ class ast_pp_util { stacked_value m_rec_decls; stacked_value m_decls; stacked_value m_sorts; + stacked_value 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(); diff --git a/src/ast/decl_collector.cpp b/src/ast/decl_collector.cpp index c08c1cf751..44cfc3c88f 100644 --- a/src/ast/decl_collector.cpp +++ b/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); } diff --git a/src/ast/decl_collector.h b/src/ast/decl_collector.h index a7f79d008a..e1dd5dc1be 100644 --- a/src/ast/decl_collector.h +++ b/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 m_sorts; + lim_svector m_type_vars; lim_svector m_decls; lim_svector 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 const& get_sorts() const { return m_sorts; } + lim_svector const& get_type_vars() const { return m_type_vars; } lim_svector const& get_func_decls() const { return m_decls; } lim_svector const& get_rec_decls() const { return m_rec_decls; } };