From 867f45496dddfe3e798c329a31c24149d650940f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 2 Aug 2026 12:14:51 -0700
Subject: [PATCH] separate out guard_set_cache

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/guard_set.h | 74 ++++++++++++++++++++----------------
 1 file changed, 41 insertions(+), 33 deletions(-)

diff --git a/src/ast/rewriter/guard_set.h b/src/ast/rewriter/guard_set.h
index 3b68cd6af9..5488218db0 100644
--- a/src/ast/rewriter/guard_set.h
+++ b/src/ast/rewriter/guard_set.h
@@ -30,46 +30,54 @@ Author:
 #include "ast/seq_decl_plugin.h"
 #include "ast/rewriter/seq_range_collapse.h"
 
-// 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:
-    guard_set_cache(ast_manager& m): m(m), m_trail(m) {}
-    ~guard_set_cache() { reset(); }
-    void reset();
-    void maybe_reset(unsigned cap) {
-        if (m_cache.size() > cap)
-            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);
-};
 
 class guard_set {
+public:
+    // 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 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(ast_manager &m) : m(m), m_trail(m) {}
+        ~cache() {
+            reset();
+        }
+        void reset();
+        void maybe_reset(unsigned cap) {
+            if (m_cache.size() > cap)
+                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:
     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
-    guard_set_cache*     m_rp_cache = nullptr;
+    cache*               m_rp_cache = nullptr;
     seq::range_predicate m_rp;             // char representation
     expr_ref             m_guard;          // generic representation (conjunction over v0)
 
@@ -88,7 +96,7 @@ class guard_set {
 
 public:
     guard_set(ast_manager& _m, seq_util& _u, sort* elem_sort, expr* v0,
-              guard_set_cache* cache = nullptr);
+              cache* cache = nullptr);
 
     bool ok() const { return m_ok; }