From 0c251e2930b07a94d3188286f232f7b07dc26b5f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 2 Aug 2026 14:19:44 -0700 Subject: [PATCH] collect configurations one place --- src/ast/rewriter/seq_monadic.cpp | 6 +++--- src/ast/rewriter/seq_monadic.h | 21 +++++++++++++++------ 2 files changed, 18 insertions(+), 9 deletions(-) diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp index 70808c7365..5dfc599b0d 100644 --- a/src/ast/rewriter/seq_monadic.cpp +++ b/src/ast/rewriter/seq_monadic.cpp @@ -67,7 +67,7 @@ expr_ref_pair_vector const& seq_monadic::derivative_cofactors(expr* r) { if (m_cofactors.find(r, v)) return *v; v = alloc(expr_ref_pair_vector, m); - if (m_mode == transition_mode::light_antimirov) + if (m_config.m_mode == transition_mode::light_antimirov) m_rw.light_ant_derivative_cofactors(r, *v); else m_rw.brz_derivative_cofactors(r, *v); @@ -399,11 +399,11 @@ lbool seq_monadic::decide_dnf(vector const& dnf) { lbool ne = product_nonempty(groups[gi], m_config.m_model ? &w : nullptr); if (ne == l_false) { has_empty = true; break; } // this variable has no value if (ne == l_undef) { has_undef = true; continue; } - if (m_gen_model) { m_pin.push_back(w); local.insert(group_var[gi], w.get()); } + if (m_config.m_model) { m_pin.push_back(w); local.insert(group_var[gi], w.get()); } } if (has_empty) continue; if (has_undef) { any_undef = true; continue; } - if (m_gen_model) + if (m_config.m_model) for (auto const& [k, v] : local) m_model.insert(k, v); return l_true; // all variables satisfiable => sat diff --git a/src/ast/rewriter/seq_monadic.h b/src/ast/rewriter/seq_monadic.h index 44afad23fb..9fa37c4cfa 100644 --- a/src/ast/rewriter/seq_monadic.h +++ b/src/ast/rewriter/seq_monadic.h @@ -95,18 +95,25 @@ private: }; struct config { + transition_mode m_mode; + bool m_model = true; // whether solve()/check() extract a feasible model + bool m_min_core = true; // whether check() minimizes the unsat core (else: all deps) + + config(transition_mode mode) : m_mode(mode) {} + }; + ast_manager& m; seq_rewriter& m_rw; th_rewriter m_thrw; // normalizes constant-element derivatives (folds // ground guards so dead states become re.empty) trail_stack& m_undo_trail; - transition_mode m_mode; sort* m_seq_sort = nullptr; // sequence sort of the regex under analysis sort* m_elem_sort = nullptr; // element sort of that sequence sort expr_ref_vector m_pin; // pins derivative states / witnesses referenced later unsigned m_budget = 0; // global work budget (decompose disjuncts + product pops) bool m_giveup = false; // set when the budget is exhausted - bool m_min_core = true; // whether check() minimizes the unsat core (else: all deps) + config m_config; + statistics m_stats; obj_map m_model; // last extracted model (var -> witness); see get_model() cofactor_cache m_cofactors; // memoizes derivative_cofactors per regex (see class above) guard_set::cache m_rp_cache; // cofactor guard -> range predicate @@ -193,15 +200,17 @@ public: seq_monadic(seq_rewriter& rw, trail_stack& undo_trail, transition_mode mode = transition_mode::light_antimirov) : m(rw.m()), m_rw(rw), m_thrw(rw.m()), m_undo_trail(undo_trail), - m_mode(mode), m_pin(rw.m()), m_cofactors(rw.m()), m_rp_cache(rw.m()) {} + m_pin(rw.m()), m_config(mode), m_cofactors(rw.m()), m_rp_cache(rw.m()) {} ~seq_monadic() = default; - transition_mode mode() const { return m_mode; } + transition_mode mode() const { return m_config.m_mode; } + + void collect_statistics(::statistics& st) const; // Enable/disable model generation (default: enabled). When enabled, a successful // solve()/check() extracts a feasible model retrievable via get_model(). - void set_gen_model(bool b) { m_gen_model = b; } + void set_gen_model(bool b) { m_config.m_model = b; } // The model extracted by the last successful solve()/check(): var -> witness, // where each witness is a concrete sequence term (over the element sort) giving one @@ -216,7 +225,7 @@ public: // Enable/disable unsat-core minimization (default: enabled). When disabled, core() // returns the dependencies of all asserted memberships (no deletion-based shrinking). - void set_min_core(bool b) { m_min_core = b; } + void set_min_core(bool b) { m_config.m_min_core = b; } void set_is_var(std::function const &is_var) { m_is_var = is_var;