public final class RuleAppIndex
extends java.lang.Object
Constructor and Description |
---|
RuleAppIndex(TacletAppIndex p_tacletAppIndex,
BuiltInRuleAppIndex p_builtInRuleAppIndex,
Services services) |
RuleAppIndex(TacletIndex p_tacletIndex,
BuiltInRuleAppIndex p_builtInRuleAppIndex,
Services services) |
Modifier and Type | Method and Description |
---|---|
void |
addNewRuleListener(NewRuleListener l)
adds a change listener to the index
|
void |
addNoPosTacletApp(java.lang.Iterable<NoPosTacletApp> tacletApps)
adds a new Taclet with instantiation information to the Taclet Index
of this TacletAppIndex.
|
void |
addNoPosTacletApp(NoPosTacletApp tacletApp)
adds a new Taclet with instantiation information to the Taclet Index
of this TacletAppIndex.
|
void |
autoModeStarted()
Currently the rule app index can either operate in interactive mode (and
contain applications of all existing taclets) or in automatic mode (and
only contain a restricted set of taclets that can possibly be applied
automated).
|
void |
autoModeStopped() |
BuiltInRuleAppIndex |
builtInRuleAppIndex()
returns the built-in rule application index for this
ruleAppIndex.
|
void |
clearAndDetachCache()
Empties all caches
|
void |
clearIndexes()
Empties all caches
|
RuleAppIndex |
copy()
returns a new RuleAppIndex with a copied TacletIndex.
|
void |
fillCache()
Ensures that all caches are fully up-to-date
|
ImmutableList<IBuiltInRuleApp> |
getBuiltInRules(Goal g,
PosInOccurrence pos)
returns a list of built-in rule applications applicable
for the given goal, user defined constraint and position
|
ImmutableList<NoPosTacletApp> |
getFindTaclet(TacletFilter filter,
PosInOccurrence pos,
TermServices services)
collects all FindTacletInstantiations for the given
heuristics and position
|
ImmutableList<NoPosTacletApp> |
getNoFindTaclet(TacletFilter filter,
Services services)
collects all NoFindTacletInstantiations for the given
heuristics
|
ImmutableList<NoPosTacletApp> |
getRewriteTaclet(TacletFilter filter,
PosInOccurrence pos,
TermServices services)
collects all RewriteTacletInstantiations for the given
heuristics in a subterm of the constraintformula described by a
PosInOccurrence
|
ImmutableList<TacletApp> |
getTacletAppAt(TacletFilter filter,
PosInOccurrence pos,
Services services)
returns the set of rule applications for
the given heuristics
at the given position of the given sequent.
|
ImmutableList<TacletApp> |
getTacletAppAtAndBelow(TacletFilter filter,
PosInOccurrence pos,
Services services)
returns the rule applications at the given PosInOccurrence and at all
Positions below this.
|
void |
removeNewRuleListener(NewRuleListener l)
removes a change listener to the index
|
void |
removeNoPosTacletApp(NoPosTacletApp tacletApp)
remove a Taclet with instantiation information from the Taclet
Index of this TacletAppIndex.
|
void |
reportAutomatedRuleApps(NewRuleListener l,
Services services)
Report all rule applications that are supposed to be applied
automatically, and that are currently stored by the index
|
void |
scanBuiltInRules(Goal p_goal)
Report builtin rules to all registered NewRuleListener instances.
|
void |
sequentChanged(Goal g,
SequentChangeInfo sci)
called if a formula has been replaced
|
void |
setup(Goal p_goal) |
TacletIndex |
tacletIndex()
returns the Taclet index for this ruleAppIndex.
|
java.lang.String |
toString() |
public RuleAppIndex(TacletAppIndex p_tacletAppIndex, BuiltInRuleAppIndex p_builtInRuleAppIndex, Services services)
public RuleAppIndex(TacletIndex p_tacletIndex, BuiltInRuleAppIndex p_builtInRuleAppIndex, Services services)
public void setup(Goal p_goal)
public void autoModeStarted()
public void autoModeStopped()
public TacletIndex tacletIndex()
public BuiltInRuleAppIndex builtInRuleAppIndex()
public void addNewRuleListener(NewRuleListener l)
l
- the AppIndexListener to addpublic void removeNewRuleListener(NewRuleListener l)
l
- the AppIndexListener to removepublic ImmutableList<TacletApp> getTacletAppAt(TacletFilter filter, PosInOccurrence pos, Services services)
filter
- the TacletFiler filtering the taclets of interestpos
- the PosInOccurrence to focusservices
- the Services object encapsulating information
about the java datastructures like (static)types etc.public ImmutableList<TacletApp> getTacletAppAtAndBelow(TacletFilter filter, PosInOccurrence pos, Services services)
filter
- the TacletFiler filtering the taclets of interestpos
- the position where to start fromservices
- the Services object encapsulating information
about the java datastructures like (static)types etc.public ImmutableList<NoPosTacletApp> getFindTaclet(TacletFilter filter, PosInOccurrence pos, TermServices services)
filter
- the TacletFiler filtering the taclets of interestpos
- the PosInOccurrence to focusservices
- the Services object encapsulating information
about the java datastructures like (static)types etc.public ImmutableList<NoPosTacletApp> getNoFindTaclet(TacletFilter filter, Services services)
filter
- the TacletFiler filtering the taclets of interestservices
- the Services object encapsulating information
about the java datastructures like (static)types etc.public ImmutableList<NoPosTacletApp> getRewriteTaclet(TacletFilter filter, PosInOccurrence pos, TermServices services)
filter
- the TacletFiler filtering the taclets of interestpos
- the PosInOccurrence to focusservices
- the Services object encapsulating information
about the java datastructures like (static)types etc.public ImmutableList<IBuiltInRuleApp> getBuiltInRules(Goal g, PosInOccurrence pos)
public void addNoPosTacletApp(java.lang.Iterable<NoPosTacletApp> tacletApps)
tacletApp
- the NoPosTacletApp describing a partial instantiated Taclet to addpublic void addNoPosTacletApp(NoPosTacletApp tacletApp)
tacletApp
- the NoPosTacletApp describing a partial instantiated Taclet to addpublic void removeNoPosTacletApp(NoPosTacletApp tacletApp)
tacletApp
- the NoPosTacletApp to removepublic void sequentChanged(Goal g, SequentChangeInfo sci)
g
- the Goal which sequent has been changedsci
- SequentChangeInfo describing the change of the sequentpublic void clearAndDetachCache()
public void clearIndexes()
public void fillCache()
public void reportAutomatedRuleApps(NewRuleListener l, Services services)
l
- the NewRuleListenerservices
- the Servicespublic void scanBuiltInRules(Goal p_goal)
p_goal
- the Goal which to scanpublic RuleAppIndex copy()
public java.lang.String toString()
toString
in class java.lang.Object
Copyright © 2003-2019 The KeY-Project.