public class ServiceCaches extends Object
Instances of this class provides all caches used by an individual Proof
or more precise by its Services
.
This is a redesign of the old static caches which were implemented via final static
Map
s like
private static final Map<CacheKey, TermTacletAppIndex> termTacletAppIndexCache = new LRUCache<CacheKey, TermTacletAppIndex> ( MAX_TERM_TACLET_APP_INDEX_ENTRIES );
.
The old idea that memory is reused and shared between multiple Proof
s
by static variables is wrong, because in practice it wastes memory.
The problem is that cached data structures
can become large, especially in case of getTermTacletAppIndexCache()
.
The static cache is filled with these large data structures and
not freed even if all Proof
s are disposed (Proof.isDisposed()
).
This can fill quickly (about 30 done Proof
s) the whole memory.
A new Proof
which does not profit from the cached data structure
has then no free memory to live in which makes the whole system unusable slow.
The goal of this new design is to avoid all static cache variables and
to collect them instead as instance variables in this class.
Each Proof
has its own Services
which provides a ServiceCaches
instance to use via
Services.getCaches()
. The advantages are:
Proof
s not relevant for the current Proof
.Proof
is disposed via Proof.dispose()
.Proof
s at the same time are faster because they can fill the cache up to the fixed limit. Also the user interface profits from it when a user switches between proofs.Proof
s exist at the same time it seems to be no problem that multiple caches exist.Proof
s use the same cache can be realized just by using the same ServiceCaches
instance. This can be useful for instance in side proofs.Modifier and Type | Field and Description |
---|---|
private LRUCache<Term,AbstractBetaFeature.TermInfo> |
betaCandidates |
private Map<Sort,Map<Sort,Boolean>> |
disjointnessCache
Cache used by TypeComparisonCondition
|
private Map<Node,PosInOccurrence> |
exhaustiveMacroCache
Cache used by the exhaustive macro
|
private LRUCache<Term,Term> |
formattedTermCache
Cache used by HandleArith for caching formatted terms
|
private Map<Term,ClausesGraph> |
graphCache
Map from
Term (allTerm) to ClausesGraph |
private LRUCache<PosInOccurrence,RuleAppCost> |
ifThenElseMalusCache |
private LRUCache<Operator,Integer> |
introductionTimeCache |
static int |
MAX_TERM_TACLET_APP_INDEX_ENTRIES
The maximal number of index entries in
getTermTacletAppIndexCache() . |
private LRUCache<Term,Monomial> |
monomialCache |
private LRUCache<Term,Polynomial> |
polynomialCache |
private LRUCache<Term,Term> |
provedByArithFstCache
Caches used bu HandleArith to cache proof results
|
private LRUCache<Pair<Term,Term>,Term> |
provedByArithSndCache |
private Map<Term,Term> |
termCache
Cache used by the TermFactory to avoid unnecessary creation of terms
|
private Map<PrefixTermTacletAppIndexCacheImpl.CacheKey,TermTacletAppIndex> |
termTacletAppIndexCache
The cache used by
TermTacletAppIndexCacheSet instances. |
private Map<Term,TriggersSet> |
triggerSetCache
a
HashMap from Term to
TriggersSet uses to cache all created TriggersSets |
Constructor and Description |
---|
ServiceCaches() |
Modifier and Type | Method and Description |
---|---|
LRUCache<Term,AbstractBetaFeature.TermInfo> |
getBetaCandidates() |
Map<Sort,Map<Sort,Boolean>> |
getDisjointnessCache() |
Map<Node,PosInOccurrence> |
getExhaustiveMacroCache() |
LRUCache<Term,Term> |
getFormattedTermCache() |
Map<Term,ClausesGraph> |
getGraphCache() |
LRUCache<PosInOccurrence,RuleAppCost> |
getIfThenElseMalusCache() |
LRUCache<Operator,Integer> |
getIntroductionTimeCache() |
LRUCache<Term,Monomial> |
getMonomialCache() |
LRUCache<Term,Polynomial> |
getPolynomialCache() |
LRUCache<Term,Term> |
getProvedByArithFstCache() |
LRUCache<Pair<Term,Term>,Term> |
getProvedByArithSndCache() |
Map<Term,Term> |
getTermFactoryCache() |
Map<PrefixTermTacletAppIndexCacheImpl.CacheKey,TermTacletAppIndex> |
getTermTacletAppIndexCache()
Returns the cache used by
TermTacletAppIndexCacheSet instances. |
Map<Term,TriggersSet> |
getTriggerSetCache() |
public static final int MAX_TERM_TACLET_APP_INDEX_ENTRIES
getTermTacletAppIndexCache()
.private final Map<PrefixTermTacletAppIndexCacheImpl.CacheKey,TermTacletAppIndex> termTacletAppIndexCache
TermTacletAppIndexCacheSet
instances.private final LRUCache<Term,AbstractBetaFeature.TermInfo> betaCandidates
private final LRUCache<PosInOccurrence,RuleAppCost> ifThenElseMalusCache
private final LRUCache<Term,Polynomial> polynomialCache
private final Map<Term,TriggersSet> triggerSetCache
HashMap
from Term
to
TriggersSet
uses to cache all created TriggersSetsprivate final Map<Term,ClausesGraph> graphCache
Term
(allTerm) to ClausesGraph
private final Map<Term,Term> termCache
private final Map<Sort,Map<Sort,Boolean>> disjointnessCache
private final LRUCache<Term,Term> formattedTermCache
private LRUCache<Term,Term> provedByArithFstCache
private Map<Node,PosInOccurrence> exhaustiveMacroCache
public Map<PrefixTermTacletAppIndexCacheImpl.CacheKey,TermTacletAppIndex> getTermTacletAppIndexCache()
TermTacletAppIndexCacheSet
instances.TermTacletAppIndexCacheSet
instances.public final LRUCache<Term,AbstractBetaFeature.TermInfo> getBetaCandidates()
public final LRUCache<PosInOccurrence,RuleAppCost> getIfThenElseMalusCache()
public final LRUCache<Term,Polynomial> getPolynomialCache()
public final Map<Term,TriggersSet> getTriggerSetCache()
public final Map<Term,ClausesGraph> getGraphCache()
public final Map<Node,PosInOccurrence> getExhaustiveMacroCache()