public class ServiceCaches
extends java.lang.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 java.util.Map<Sort,java.util.Map<Sort,java.lang.Boolean>> |
disjointnessCache
Cache used by TypeComparisonCondition
|
private java.util.Map<Node,PosInOccurrence> |
exhaustiveMacroCache
Cache used by the exhaustive macro
|
private LRUCache<Term,Term> |
formattedTermCache
Cache used by HandleArith for caching formatted terms
|
private java.util.Map<Term,ClausesGraph> |
graphCache
Map from
Term (allTerm) to ClausesGraph |
private IfFormulaInstantiationCache |
ifFormulaInstantiationCache
Cache used IfFormulaInstSeq
|
private IfInstantiationCachePool |
ifInstantiationCache
Cache used by the ifinstantiator
|
private LRUCache<PosInOccurrence,RuleAppCost> |
ifThenElseMalusCache |
private LRUCache<Operator,java.lang.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 java.util.Map<Term,Term> |
termCache
Cache used by the TermFactory to avoid unnecessary creation of terms
|
private java.util.Map<PrefixTermTacletAppIndexCacheImpl.CacheKey,TermTacletAppIndex> |
termTacletAppIndexCache
The cache used by
TermTacletAppIndexCacheSet instances. |
private java.util.Map<Term,TriggersSet> |
triggerSetCache
a
HashMap from Term to
TriggersSet uses to cache all created TriggersSets |
Constructor and Description |
---|
ServiceCaches() |
public static final int MAX_TERM_TACLET_APP_INDEX_ENTRIES
getTermTacletAppIndexCache()
.private final java.util.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 java.util.Map<Term,TriggersSet> triggerSetCache
HashMap
from Term
to
TriggersSet
uses to cache all created TriggersSetsprivate final java.util.Map<Term,ClausesGraph> graphCache
Term
(allTerm) to ClausesGraph
private final java.util.Map<Term,Term> termCache
private final java.util.Map<Sort,java.util.Map<Sort,java.lang.Boolean>> disjointnessCache
private final LRUCache<Term,Term> formattedTermCache
private final LRUCache<Term,Term> provedByArithFstCache
private final java.util.Map<Node,PosInOccurrence> exhaustiveMacroCache
private final IfInstantiationCachePool ifInstantiationCache
private final IfFormulaInstantiationCache ifFormulaInstantiationCache
public final java.util.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<Operator,java.lang.Integer> getIntroductionTimeCache()
public final LRUCache<Term,Polynomial> getPolynomialCache()
public final java.util.Map<Term,TriggersSet> getTriggerSetCache()
public final java.util.Map<Term,ClausesGraph> getGraphCache()
public final java.util.Map<Sort,java.util.Map<Sort,java.lang.Boolean>> getDisjointnessCache()
public final java.util.Map<Node,PosInOccurrence> getExhaustiveMacroCache()
public final IfInstantiationCachePool getIfInstantiationCache()
public final IfFormulaInstantiationCache getIfFormulaInstantiationCache()