working on moving cached cofactors

src/ast/rewriter/seq_derive.cpp

@@ -1570,6 +1570,21 @@ 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 *v = nullptr;
+        if (m_cofactor_cache.find(r, v))
+            return *v;
+        v = alloc(expr_ref_pair_vector, m);
+        if (mode == transition_mode::light_antimirov)
+            light_ant_derivative_cofactors(r, *v);
+        else
+            brz_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
         // (:var 0); operator() sets m_ele to that variable.  We use the

src/ast/rewriter/seq_derive.h

@@ -54,6 +54,35 @@ namespace seq {
      * - Depth-bounded to prevent stack overflow
      */
     class derive {
+        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();
+            }
+        };
         ast_manager&    m;
         seq_util        m_util;
         arith_util      m_autil;
@@ -64,6 +93,8 @@ namespace seq {
         obj_pair_map<expr, expr, expr*> m_acache, m_bcache;
         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;
 
         // 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
@@ -241,6 +272,9 @@ 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 *ele, expr *r);
+
         /**
          * Compute the symbolic derivative of r and enumerate its reachable
          * leaves in fully ITE-hoisted normal form.

src/ast/rewriter/seq_monadic.cpp

@@ -22,11 +22,6 @@ Abstract:
 
 TODOs:
 - create a validation harness: expose certificates for correctness that can be checked.
-- consider using expr_ref as alternative to pinned expressions
-- revisit parse_term and "the_var" condition. A sequence of units should be allowed 
-  even though a good solver will apply derivatives directly.
-- optimize for cases where the same term is member of multiple regex constraints.
-  - coallesce the membership constraints into a single regex membership constraint of the intersection of regexes.
 - take into account shape of terms to prune the search space (e.g., if the term is xax, then retain the effect of 
   intersecting with .*a.*).
 - connect to semi-linear pruning, such as xx in (ab)*a is unsat due to parity 
@@ -352,9 +347,9 @@ lbool seq_monadic::product_nonempty(svector<component> const& comps, expr_ref* w
     return l_false;
 }
 
-bool seq_monadic::parse_term(expr* t, vector<atom>& atoms, expr*& the_var) {
+bool seq_monadic::parse_term(expr* t, vector<atom>& atoms) {
     if (u().str.is_concat(t))
-        return all_of(*to_app(t), [&](expr* arg) { return parse_term(arg, atoms, the_var); });
+        return all_of(*to_app(t), [&](expr* arg) { return parse_term(arg, atoms); });
     if (u().str.is_empty(t))
         return true;                              // epsilon: contributes nothing
     zstring s;
@@ -372,7 +367,6 @@ bool seq_monadic::parse_term(expr* t, vector<atom>& atoms, expr*& the_var) {
     }
     // uninterpreted constant of sequence sort => a sequence variable
     if (is_var(t)) {
-        the_var = t;                              // mark that at least one variable occurs
         atoms.push_back(atom(m, true, t, nullptr));
         return true;
     }
@@ -416,15 +410,10 @@ bool seq_monadic::prepare(membership_vec const& memberships) {
             return false;
         }
         vector<atom> atoms;
-        expr* the_var = nullptr;
-        if (!parse_term(term, atoms, the_var)) {
+        if (!parse_term(term, atoms)) {
             m_stats.inc_bail(bail_reason::unsupported);
             return false;
         }
-        if (!the_var) {
-            m_stats.inc_bail(bail_reason::unsupported);
-            return false;                         // no variable: ground membership, not our case
-        }
         m_regexes.push_back(regex);
         m_atoms.push_back(atoms);
         m_pin.push_back(regex);

src/ast/rewriter/seq_monadic.h

@@ -225,7 +225,7 @@ private:
     lbool product_nonempty(svector<component> const& comps, expr_ref* witness_word = nullptr);
 
     // Flatten a str.++ term into atoms; false on an unsupported shape (non-constant unit).
-    bool parse_term(expr* term, vector<atom>& atoms, expr*& the_var);
+    bool parse_term(expr* term, vector<atom>& atoms);
 
     // Drop all search state accumulated by the previous decide()/solve().
     void reset_search();