move derivative cofactors cache into seq_derive

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

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<expr, expr, expr*> 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

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))

src/ast/rewriter/seq_monadic.h

@@ -78,42 +78,13 @@ Author:
 #include <unordered_map>
 
 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<expr, expr_ref_pair_vector*>  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<expr, expr*> 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<expr, expr, expr*> m_der_cache;  // memoizes der_elem per (regex, element)
     obj_map<expr, char> 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().

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)