diff --git a/src/ast/rewriter/seq_derive.cpp b/src/ast/rewriter/seq_derive.cpp index 3a196ddf82..1876f4ddfb 100644 --- a/src/ast/rewriter/seq_derive.cpp +++ b/src/ast/rewriter/seq_derive.cpp @@ -38,7 +38,8 @@ namespace seq { m_autil(m), m_br(m), m_re(re), - m_trail(m), + m_trail(m), + m_cofactor_cache(m), m_ele(m), m_path_expr(m) { m_br.set_flat_and_or(false); @@ -1570,20 +1571,18 @@ namespace seq { get_cofactors_rec(r, result); } - #if 0 - expr_ref_pair_vector const &derive::get_cached_cofactors(transition_mode mode, expr *ele, expr *r) { + expr_ref_pair_vector const &derive::get_cached_cofactors(transition_mode mode, expr *r) { expr_ref_pair_vector *v = nullptr; if (m_cofactor_cache.find(r, v)) return *v; v = alloc(expr_ref_pair_vector, m); - if (mode == transition_mode::light_antimirov) + if (mode == transition_mode::light_antimirov_tm) light_ant_derivative_cofactors(r, *v); else - brz_derivative_cofactors(r, *v); + derivative_cofactors(r, *v); m_cofactor_cache.insert(r, v); // takes ownership of v and pins the key r return *v; } - #endif void derive::derivative_cofactors(expr* r, expr_ref_pair_vector& result) { // Compute the symbolic derivative wrt the canonical variable diff --git a/src/ast/rewriter/seq_derive.h b/src/ast/rewriter/seq_derive.h index 2ce4755e16..46ec0157fe 100644 --- a/src/ast/rewriter/seq_derive.h +++ b/src/ast/rewriter/seq_derive.h @@ -37,6 +37,7 @@ class seq_rewriter; namespace seq { enum class derivative_kind { antimirov_t, brzozowski_t }; + enum class transition_mode { brzozowski_tm, light_antimirov_tm }; /** * Symbolic derivative engine for regular expressions. * @@ -94,7 +95,7 @@ namespace seq { obj_pair_map m_atop_cache, m_btop_cache; // post-simplify cache expr_ref_vector m_trail; // pin cached results - // cofactor_cache m_cofactor_cache; + cofactor_cache m_cofactor_cache; // Op cache for ITE-hoisting operations (union, inter, concat, complement) // Path-aware caches: key is (a, b, path_expr) for binary ops, (a, path_expr) for complement @@ -272,8 +273,11 @@ namespace seq { */ void get_cofactors(expr* ele, expr* r, expr_ref_pair_vector& result); + expr_ref_pair_vector const &get_cached_cofactors(transition_mode mode, expr *r); - // expr_ref_pair_vector const &get_cached_cofactors(transition_mode mode, expr *ele, expr *r); + void maybe_reset_cached_cofactors(unsigned cap) { + m_cofactor_cache.maybe_reset(cap); + } /** * Compute the symbolic derivative of r and enumerate its reachable diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp index 85c2c9d8c4..c2fb368698 100644 --- a/src/ast/rewriter/seq_monadic.cpp +++ b/src/ast/rewriter/seq_monadic.cpp @@ -98,17 +98,7 @@ lbool seq_monadic::nullable(expr* r) { expr_ref_pair_vector const& seq_monadic::derivative_cofactors(expr* r) { ++m_stats.m_cofactor_calls; - expr_ref_pair_vector* v = nullptr; - if (m_cofactors.find(r, v)) - return *v; - ++m_stats.m_states; - v = alloc(expr_ref_pair_vector, m); - 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); - m_cofactors.insert(r, v); // takes ownership of v and pins the key r - return *v; + return m_rw.get_derive().get_cached_cofactors(m_config.m_mode, r); } bool seq_monadic::live_states(expr* R, expr_ref_vector& out) { @@ -578,8 +568,8 @@ lbool seq_monadic::decide(membership_vec const& memberships) { return l_true; // empty conjunction is vacuously true reset_search(); // clear the caches before dropping the m_pin.reset(); // pins that keep their keys alive - m_cofactors.maybe_reset(1u << 16); // cofactors persist across calls (own their pins) m_rp_cache.maybe_reset(1u << 16); + m_rw.get_derive().maybe_reset_cached_cofactors(1u << 16); m_budget = 200000; m_giveup = false; if (!prepare(memberships)) diff --git a/src/ast/rewriter/seq_monadic.h b/src/ast/rewriter/seq_monadic.h index 46ae1e0b7c..136555f0a3 100644 --- a/src/ast/rewriter/seq_monadic.h +++ b/src/ast/rewriter/seq_monadic.h @@ -78,42 +78,13 @@ Author: #include class seq_monadic { -public: - enum class transition_mode { - brzozowski, - light_antimirov - }; - -private: - // Self-contained memo for derivative_cofactors: maps a regex to its (owned) cofactor - // vector and keeps a trail of pinned keys so they stay live for the cache's lifetime. - // The memoized cofactors depend only on the regex (and the fixed transition mode), so - // the cache is valid across solve()/decide()/check() calls; callers reset it only when - // it grows past a size cap (maybe_reset). - class cofactor_cache { - obj_map m_cache; - expr_ref_vector m_pin; // trail of pinned keys - public: - cofactor_cache(ast_manager& m) : m_pin(m) {} - ~cofactor_cache() { reset(); } - bool find(expr* r, expr_ref_pair_vector*& v) const { return m_cache.find(r, v); } - void insert(expr* r, expr_ref_pair_vector* v) { m_pin.push_back(r); m_cache.insert(r, v); } - unsigned size() const { return m_cache.size(); } - void reset() { - for (auto const& [k, v] : m_cache) - dealloc(v); - m_cache.reset(); - m_pin.reset(); - } - void maybe_reset(unsigned cap) { if (m_cache.size() > cap) reset(); } - }; struct config { - transition_mode m_mode; + seq::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) {} + config(seq::transition_mode mode) : m_mode(mode) {} }; enum class bail_reason { unsupported, state_cap, dnf_cap, budget, resource, nullability, guard, num_reasons }; @@ -141,7 +112,6 @@ private: 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 obj_pair_map m_der_cache; // memoizes der_elem per (regex, element) obj_map m_nullable_cache; // memoizes nullability (0 false / 1 true / 2 unknown); @@ -273,16 +243,16 @@ private: public: seq_monadic(seq_rewriter& rw, trail_stack& undo_trail, - transition_mode mode = transition_mode::light_antimirov) : + seq::transition_mode mode = seq::transition_mode::light_antimirov_tm) : m(rw.m()), m_rw(rw), m_thrw(rw.m()), m_undo_trail(undo_trail), - m_pin(rw.m()), m_config(mode), m_cofactors(rw.m()), m_rp_cache(rw.m()), + m_pin(rw.m()), m_config(mode), m_rp_cache(rw.m()), m_regexes(rw.m()) {} ~seq_monadic() { reset_live_cache(); } void collect_statistics(::statistics &st) const; - transition_mode mode() const { return m_config.m_mode; } + seq::transition_mode mode() const { return m_config.m_mode; } // Enable/disable model generation (default: enabled). When enabled, a successful // solve()/check() extracts a feasible model retrievable via get_model(). diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 5bad5ae3dc..1d4cb51eec 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -81,16 +81,6 @@ public: void dec_ref(sym_expr* s) { if (s) s->dec_ref(); } }; -#if 0 - -class expr_solver { -public: - virtual ~expr_solver() = default; - virtual lbool check_sat(expr* e) = 0; -}; -#endif - - /** \brief Cheap rewrite rules for seq constraints */ @@ -464,6 +454,10 @@ public: m_derive.get_cofactors(ele, r, result); } + seq::derive &get_derive() { + return m_derive; + } + /* Compute the symbolic derivative of r and enumerate its reachable leaves in fully ITE-hoisted normal form: a list of (path_condition, target)