guard_set: wrap rp_cache into guard_set_cache class (#10362)

Addresses code review feedback on PR #10361: the raw `obj_map` typedef +
static `dealloc_cache` helper is replaced by a proper `guard_set_cache`
class that owns its memory and adds a recycling optimization.

## Changes

- **New `guard_set_cache` class** (`guard_set.h` / `.cpp`):
- `m_cache` — `obj_map<expr, seq::range_predicate*>` (null value =
unsupported guard, avoids retranslation)
- `m_fresh` — pre-allocated `range_predicate*` recycled across failed
translations; when `guard_to_range_predicate` rejects a guard, the heap
object is retained in `m_fresh` instead of deallocated, so the next miss
reuses it without an alloc/dealloc round-trip
- Public API: `reset()`, `find(expr*, seq::range_predicate*&) → bool`,
`fresh(unsigned max_char) → seq::range_predicate*`, `insert(expr*,
seq::range_predicate*)`

- **`guard_set`**: removed `rp_cache` typedef and `dealloc_cache`
static; constructor parameter updated to `guard_set_cache*`; `conjoin`
updated to use `fresh()` + `insert()` for the recycling path

- **`seq_monadic`**: field type `guard_set::rp_cache` →
`guard_set_cache`; reset call updated to `m_rp_cache.reset()`

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nikolaj@cs.stanford.edu>

src/ast/rewriter/guard_set.cpp

@@ -20,7 +20,7 @@ Author:
 #include "ast/bv_decl_plugin.h"
 
 guard_set::guard_set(ast_manager& _m, seq_util& _u, sort* elem_sort, expr* v0,
-                     rp_cache* cache)
+                     guard_set_cache* cache)
     : m(_m), u(_u), m_sort(elem_sort), m_v0(v0),
       m_is_char(_u.is_char(elem_sort)), m_rp_cache(cache),
       m_rp(_u.max_char()), m_guard(_m) {
@@ -28,10 +28,23 @@ guard_set::guard_set(ast_manager& _m, seq_util& _u, sort* elem_sort, expr* v0,
     else           m_guard = m.mk_true();
 }
 
-void guard_set::dealloc_cache(rp_cache& c) {
-    for (auto const& [k, v] : c)
-        dealloc(v);
-    c.reset();
+void guard_set_cache::reset() {
+    for (auto const& [k, v] : m_cache) dealloc(v);
+    m_cache.reset();
+    dealloc(m_fresh);
+    m_trail.reset();
+    m_fresh = nullptr;
+}
+
+seq::range_predicate* guard_set_cache::fresh(unsigned max_char) {
+    if (!m_fresh) m_fresh = alloc(seq::range_predicate, max_char);
+    return m_fresh;
+}
+
+void guard_set_cache::insert(expr* g, seq::range_predicate* p) {
+    if (p) m_fresh = nullptr;  // ownership transferred to map
+    m_trail.push_back(g);
+    m_cache.insert(g, p);
 }
 
 void guard_set::collect_consts(expr* g, ptr_vector<expr>& out) const {
@@ -138,7 +151,8 @@ lbool guard_set::generic_eval(expr_ref* witness) const {
 }
 
 void guard_set::conjoin(expr* g) {
-    if (!m_ok) return;
+    if (!m_ok) 
+        return;
     if (!m_is_char) {
         m_guard = m.mk_and(m_guard, g);
         return;
@@ -149,20 +163,20 @@ void guard_set::conjoin(expr* g) {
         // branch, so translate each one once.
         seq::range_predicate* s = nullptr;
         if (!m_rp_cache->find(g, s)) {
-            s = alloc(seq::range_predicate, u.max_char());
-            if (!seq::guard_to_range_predicate(u, m_v0, g, *s)) {
-                dealloc(s);
-                s = nullptr;
-            }
-            m_rp_cache->insert(g, s);
+            s = m_rp_cache->fresh(u.max_char());
+            if (!seq::guard_to_range_predicate(u, m_v0, g, *s)) 
+                s = nullptr; // recycles s into m_fresh
+            m_rp_cache->insert(g, s);   
         }
         if (!s) { m_ok = false; return; }
         m_rp = m_rp & *s;
         return;
     }
     seq::range_predicate s(u.max_char());
-    if (!seq::guard_to_range_predicate(u, m_v0, g, s)) { m_ok = false; return; }
-    m_rp = m_rp & s;
+    if (seq::guard_to_range_predicate(u, m_v0, g, s)) 
+        m_rp = m_rp & s;
+    else 
+        m_ok = false;     
 }
 
 lbool guard_set::eval(expr_ref* witness) const {

src/ast/rewriter/guard_set.h

@@ -30,22 +30,42 @@ Author:
 #include "ast/seq_decl_plugin.h"
 #include "ast/rewriter/seq_range_collapse.h"
 
-class guard_set {
+// Cache mapping guard expressions to their range predicates.
+// A null value in the map records that the guard is unsupported (avoiding retranslation).
+// m_fresh recycles the last allocated range_predicate so failed translations do not
+// incur an alloc/dealloc cycle on every miss.
+//
+// Lifetime contract: expr* keys are assumed to outlive the cache (their lifetime is
+// managed by the caller -- e.g. by the cofactor_cache that owns the guard expressions).
+class guard_set_cache {
+    ast_manager& m;
+    expr_ref_vector m_trail;
+    obj_map<expr, seq::range_predicate*> m_cache;
+    seq::range_predicate*                m_fresh = nullptr;
 public:
-    // Cache of guard expression -> its range predicate (null value: unsupported guard).
-    // Only meaningful for the character sort, and only valid while every guard_set sharing
-    // it uses the same element variable v0 (v0 is hash-consed per element sort).
-    typedef obj_map<expr, seq::range_predicate*> rp_cache;
-    static void dealloc_cache(rp_cache& c);
+    guard_set_cache(ast_manager& m): m(m), m_trail(m) {}
+    ~guard_set_cache() { reset(); }
+    void reset();
+    // Returns true if g is in the cache; val is set to the cached entry
+    // (val may be null = unsupported guard).
+    bool find(expr* g, seq::range_predicate*& val) const { return m_cache.find(g, val); }
+    // Returns a range_predicate* ready for guard_to_range_predicate to write into.
+    // Reuses the previously recycled object when available; otherwise allocates one.
+    seq::range_predicate* fresh(unsigned max_char);
+    // Records g -> p.  If p is non-null (translation succeeded), ownership is transferred
+    // to the cache and m_fresh is cleared.  If p is null (unsupported), the object
+    // previously returned by fresh() is retained in m_fresh for the next translation.
+    void insert(expr* g, seq::range_predicate* p);
+};
 
-private:
+class guard_set {
     ast_manager&         m;
     seq_util&            u;
     sort*                m_sort;
     expr*                m_v0;
     bool                 m_is_char;
     bool                 m_ok = true;      // false: an unsupported guard was conjoined
-    rp_cache*            m_rp_cache = nullptr;
+    guard_set_cache*     m_rp_cache = nullptr;
     seq::range_predicate m_rp;             // char representation
     expr_ref             m_guard;          // generic representation (conjunction over v0)
 
@@ -64,7 +84,7 @@ private:
 
 public:
     guard_set(ast_manager& _m, seq_util& _u, sort* elem_sort, expr* v0,
-              rp_cache* cache = nullptr);
+              guard_set_cache* cache = nullptr);
 
     bool ok() const { return m_ok; }
 

src/ast/rewriter/seq_monadic.cpp

@@ -80,7 +80,7 @@ void seq_monadic::reset_cofactor_cache() {
     for (auto const& [k, v] : m_cofactor_cache)
         dealloc(v);
     m_cofactor_cache.reset();
-    guard_set::dealloc_cache(m_rp_cache);   // the guards live in the cofactor vectors
+    m_rp_cache.reset();                      // the guards live in the cofactor vectors
 }
 
 bool seq_monadic::live_states(expr* R, expr_ref_vector& out) {

src/ast/rewriter/seq_monadic.h

@@ -86,9 +86,9 @@ private:
     bool            m_min_core = true;      // whether check() minimizes the unsat core (else: all deps)
     obj_map<expr, expr*> m_model;           // last extracted model (var -> witness); see get_model()
     obj_map<expr, expr_ref_pair_vector*> m_cofactor_cache;  // memoizes derivative_cofactors per regex
-    guard_set::rp_cache m_rp_cache;         // cofactor guard -> range predicate; the guards
-                                            // are owned by m_cofactor_cache, so both are
-                                            // reset together
+    guard_set_cache m_rp_cache;         // cofactor guard -> range predicate; the guards
+                                        // are owned by m_cofactor_cache, so both are
+                                        // reset together
     using membership_vec = vector<std::tuple<expr_ref, expr_ref, void*>>;
     membership_vec m_memberships;           // asserted (term in regex, dep) for check()
     ptr_vector<void> m_core;                // dependencies of an unsat subset, filled by check() on l_false
@@ -175,7 +175,7 @@ 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_mode(mode), m_pin(rw.m()), m_rp_cache(m) {}
 
     ~seq_monadic() { reset_cofactor_cache(); }