From 3ad6df3258a458f4bdb57a6bbb582976c1977306 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Apr 2026 08:29:41 -0700 Subject: [PATCH] build fixes Signed-off-by: Nikolaj Bjorner --- src/smt/seq/seq_nielsen.cpp | 73 +++++++------------------------------ src/smt/seq/seq_nielsen.h | 17 --------- 2 files changed, 13 insertions(+), 77 deletions(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 7b34f3077..017f1ba09 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -392,9 +392,7 @@ namespace seq { m_sg(sg), m_solver(solver), m_parikh(alloc(seq_parikh, sg)), - m_seq_regex(alloc(seq::seq_regex, sg)), - m_len_vars(sg.get_manager()), - m_gpower_vars(sg.get_manager()) { + m_seq_regex(alloc(seq::seq_regex, sg)) { } nielsen_graph::~nielsen_graph() { @@ -487,12 +485,6 @@ namespace seq { m_fresh_cnt = 0; m_root_constraints_asserted = false; m_mod_cnt.reset(); - m_len_var_cache.clear(); - m_len_vars.reset(); - m_char_var_cache.clear(); - m_gpower_n_var_cache.clear(); - m_gpower_m_var_cache.clear(); - m_gpower_vars.reset(); m_dep_mgr.reset(); m_solver.reset(); } @@ -516,6 +508,7 @@ namespace seq { } ast_manager& m = sg.get_manager(); seq_util& seq = sg.get_seq_util(); + arith_util a(m); for (euf::snode* t : tokens) { if (t->is_var()) { nielsen_subst s(t, sg.mk_empty_seq(t->get_sort()), dep); @@ -2479,7 +2472,7 @@ namespace seq { if (!exp_m || !exp_n) continue; rational diff; - SASSERT(!get_const_power_diff(exp_n, exp_m, arith, diff)); // handled by simplification + SASSERT(!get_const_power_diff(exp_n, exp_m, a, diff)); // handled by simplification // Branch 1 (explored first): n < m (add constraint c ≥ p + 1) { @@ -3657,67 +3650,27 @@ namespace seq { // ----------------------------------------------------------------------- expr_ref nielsen_graph::get_or_create_len_var(euf::snode* var, unsigned mod_count) { - SASSERT(var && var->is_var()); - SASSERT(mod_count > 0); - - auto key = std::make_pair(var->id(), mod_count); - auto it = m_len_var_cache.find(key); - if (it != m_len_var_cache.end()) - return expr_ref(it->second, m); - - // Create a fresh integer variable: len__ - std::string name = "len!" + std::to_string(var->id()) + "!" + std::to_string(mod_count); - expr_ref fresh(m.mk_fresh_const(name.c_str(), a.mk_int()), m); - m_len_vars.push_back(fresh); - m_len_var_cache.insert({key, fresh.get()}); - return fresh; + th_rewriter rw(m); + return skolem(m, rw).mk("len!", var->get_expr(), a.mk_int(mod_count), a.mk_int()); } euf::snode* nielsen_graph::get_or_create_char_var(euf::snode* var, unsigned mod_count) { - SASSERT(var && var->is_var()); - - auto key = std::make_pair(var->id(), mod_count); - auto it = m_char_var_cache.find(key); - if (it != m_char_var_cache.end()) - return it->second; - - std::string name = "c!" + std::to_string(var->id()) + "!" + std::to_string(mod_count); - sort* char_sort = m_seq.mk_char_sort(); - expr_ref fresh_const(m.mk_fresh_const(name.c_str(), char_sort), m); - expr_ref unit(m_seq.str.mk_unit(fresh_const), m); - euf::snode* fresh = m_sg.mk(unit); - m_char_var_cache.insert({key, fresh}); - return fresh; + th_rewriter rw(m); + sort *char_sort = m_seq.mk_char_sort(); + auto char_var = skolem(m, rw).mk("char!", var->get_expr(), a.mk_int(mod_count), char_sort); + return m_sg.mk(char_var); } expr_ref nielsen_graph::get_or_create_gpower_n_var(euf::snode* var, unsigned mod_count) { SASSERT(var && var->is_var()); - - auto key = std::make_pair(var->id(), mod_count); - auto it = m_gpower_n_var_cache.find(key); - if (it != m_gpower_n_var_cache.end()) - return expr_ref(it->second, m); - - std::string name = "gpn!" + std::to_string(var->id()) + "!" + std::to_string(mod_count); - expr_ref fresh(m.mk_fresh_const(name.c_str(), a.mk_int()), m); - m_gpower_vars.push_back(fresh); - m_gpower_n_var_cache.insert({key, fresh.get()}); - return fresh; + th_rewriter rw(m); + return skolem(m, rw).mk("gpn!", var->get_expr(), a.mk_int(mod_count), a.mk_int()); } expr_ref nielsen_graph::get_or_create_gpower_m_var(euf::snode* var, unsigned mod_count) { SASSERT(var && var->is_var()); - - auto key = std::make_pair(var->id(), mod_count); - auto it = m_gpower_m_var_cache.find(key); - if (it != m_gpower_m_var_cache.end()) - return expr_ref(it->second, m); - - std::string name = "gpm!" + std::to_string(var->id()) + "!" + std::to_string(mod_count); - expr_ref fresh(m.mk_fresh_const(name.c_str(), a.mk_int()), m); - m_gpower_vars.push_back(fresh); - m_gpower_m_var_cache.insert({key, fresh.get()}); - return fresh; + th_rewriter rw(m); + return skolem(m, rw).mk("gpm!", var->get_expr(), a.mk_int(mod_count), a.mk_int()); } void nielsen_graph::add_subst_length_constraints(nielsen_edge* e) { diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index a752936e2..bbceaad4a 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -769,23 +769,6 @@ namespace seq { // |x| = 1 + |x| that results from reusing the same length symbol. u_map m_mod_cnt; - // Cache: (var snode id, modification count) → fresh integer variable. - // Variables at mod_count 0 use str.len(var_expr) (standard form). - // Variables at mod_count > 0 get a fresh Z3 integer constant. - std::map, expr*> m_len_var_cache; - - // Pins the fresh length variable expressions so they aren't garbage collected. - expr_ref_vector m_len_vars; - - // Cache: (var snode id, modification count) → fresh character variable - std::map, euf::snode*> m_char_var_cache; - - // Cache: (var snode id, modification count) → fresh integer variable - std::map, expr*> m_gpower_n_var_cache; - std::map, expr*> m_gpower_m_var_cache; - - // Pins the fresh gpower variable expressions so they aren't garbage collected. - expr_ref_vector m_gpower_vars; // Arena for dep_tracker nodes. Declared mutable so that const methods // (e.g., explain_conflict) can call mk_join / linearize.