mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-08 15:02:09 +00:00
Code Activity

separate out guard_set_cache

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-08-02 12:14:51 -07:00
parent 6b91929df9
commit 867f45496d
1 changed files with 41 additions and 33 deletions
Download patch file Download diff file Expand all files Collapse all files

74
src/ast/rewriter/guard_set.h
View file

@ -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; }