| java.lang.Object
 de.uka.ilkd.key.proof.RuleAppIndex
| RuleAppIndex | | public class RuleAppIndex (Code) | | manages the possible application of rules (RuleApps)
|
| Method Summary | |
| public void | addNewRuleListener(NewRuleListener l)
| | public void | addNoPosTacletApp(NoPosTacletApp tacletApp)
adds a new Taclet with instantiation information to the Taclet Index
of this TacletAppIndex. | | public 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). | | public void | autoModeStopped()
| | public BuiltInRuleAppIndex | builtInRuleAppIndex()
returns the built-in rule application index for this
ruleAppIndex. | | public void | clearAndDetachCache()
| | public void | clearIndexes()
| | public RuleAppIndex | copy()
returns a new RuleAppIndex with a copied TacletIndex. | | public void | fillCache()
| | public ListOfRuleApp | getBuiltInRule(Goal goal, PosInOccurrence pos, Constraint userConstraint)
| | public ListOfNoPosTacletApp | getFindTaclet(TacletFilter filter, PosInOccurrence pos, Services services, Constraint userConstraint)
| | public ListOfNoPosTacletApp | getNoFindTaclet(TacletFilter filter, Services services, Constraint userConstraint)
| | public ListOfNoPosTacletApp | getRewriteTaclet(TacletFilter filter, PosInOccurrence pos, Services services, Constraint userConstraint)
| | public ListOfTacletApp | getTacletAppAt(TacletFilter filter, PosInOccurrence pos, Services services, Constraint userConstraint)
returns the set of rule applications for
the given heuristics
at the given position of the given sequent. | | public ListOfTacletApp | getTacletAppAtAndBelow(TacletFilter filter, PosInOccurrence pos, Services services, Constraint userConstraint)
returns the rule applications at the given PosInOccurrence and at all
Positions below this. | | public void | removeNewRuleListener(NewRuleListener l)
| | public void | removeNoPosTacletApp(NoPosTacletApp tacletApp)
remove a Taclet with instantiation information from the Taclet
Index of this TacletAppIndex. | | public void | reportAutomatedRuleApps(NewRuleListener l, Services services, Constraint userConstraint)
| | public void | scanBuiltInRules(Goal p_goal, Constraint p_userConstraint)
Report builtin rules to all registered NewRuleListener instances. | | public void | sequentChanged(Goal goal, SequentChangeInfo sci)
| | public void | setup(Goal p_goal)
| | public TacletIndex | tacletIndex()
returns the Taclet index for this ruleAppIndex. | | public String | toString()
|
| addNewRuleListener | | public void addNewRuleListener(NewRuleListener l)(Code) | | adds a change listener to the index
Parameters:
l - the AppIndexListener to add |
| addNoPosTacletApp | | public void addNoPosTacletApp(NoPosTacletApp tacletApp)(Code) | | adds a new Taclet with instantiation information to the Taclet Index
of this TacletAppIndex.
Parameters:
tacletApp - the NoPosTacletApp describing a partial instantiated Taclet to add |
| autoModeStarted | | public void autoModeStarted()(Code) | | 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). This distinction could be replaced with a more general way to
control the contents of the rule app index
|
| autoModeStopped | | public void autoModeStopped()(Code) | | |
| builtInRuleAppIndex | | public BuiltInRuleAppIndex builtInRuleAppIndex()(Code) | | returns the built-in rule application index for this
ruleAppIndex.
|
| clearAndDetachCache | | public void clearAndDetachCache()(Code) | | Empties all caches
|
| clearIndexes | | public void clearIndexes()(Code) | | Empties all caches
|
| copy | | public RuleAppIndex copy()(Code) | | returns a new RuleAppIndex with a copied TacletIndex.
Attention: the listener lists are not copied
|
| fillCache | | public void fillCache()(Code) | | Ensures that all caches are fully up-to-date
|
| getBuiltInRule | | public ListOfRuleApp getBuiltInRule(Goal goal, PosInOccurrence pos, Constraint userConstraint)(Code) | | returns a list of built-in rule applications applicable
for the given goal, user defined constraint and position
|
| getFindTaclet | | public ListOfNoPosTacletApp getFindTaclet(TacletFilter filter, PosInOccurrence pos, Services services, Constraint userConstraint)(Code) | | collects all FindTacletInstantiations for the given
heuristics and position
Parameters:
filter - the TacletFiler filtering the taclets of interest
Parameters:
pos - the PosInOccurrence to focus
Parameters:
services - the Services object encapsulating informationabout the java datastructures like (static)types etc.
Parameters:
userConstraint - the Constraint with user defined instantiationsof meta variables list of all possible instantiations |
| getNoFindTaclet | | public ListOfNoPosTacletApp getNoFindTaclet(TacletFilter filter, Services services, Constraint userConstraint)(Code) | | collects all NoFindTacletInstantiations for the given
heuristics
Parameters:
filter - the TacletFiler filtering the taclets of interest
Parameters:
services - the Services object encapsulating informationabout the java datastructures like (static)types etc.
Parameters:
userConstraint - the Constraint with user defined instantiationsof meta variables list of all possible instantiations |
| getRewriteTaclet | | public ListOfNoPosTacletApp getRewriteTaclet(TacletFilter filter, PosInOccurrence pos, Services services, Constraint userConstraint)(Code) | | collects all RewriteTacletInstantiations for the given
heuristics in a subterm of the constraintformula described by a
PosInOccurrence
Parameters:
filter - the TacletFiler filtering the taclets of interest
Parameters:
pos - the PosInOccurrence to focus
Parameters:
services - the Services object encapsulating informationabout the java datastructures like (static)types etc.
Parameters:
userConstraint - the Constraint with user defined instantiationsof meta variables list of all possible instantiations |
| getTacletAppAt | | public ListOfTacletApp getTacletAppAt(TacletFilter filter, PosInOccurrence pos, Services services, Constraint userConstraint)(Code) | | returns the set of rule applications for
the given heuristics
at the given position of the given sequent.
Parameters:
filter - the TacletFiler filtering the taclets of interest
Parameters:
pos - the PosInOccurrence to focus
Parameters:
services - the Services object encapsulating informationabout the java datastructures like (static)types etc.
Parameters:
userConstraint - the Constraint with user defined instantiationsof meta variables |
| getTacletAppAtAndBelow | | public ListOfTacletApp getTacletAppAtAndBelow(TacletFilter filter, PosInOccurrence pos, Services services, Constraint userConstraint)(Code) | | returns the rule applications at the given PosInOccurrence and at all
Positions below this. The method calls getTacletAppAt for all the
Positions below.
Parameters:
filter - the TacletFiler filtering the taclets of interest
Parameters:
pos - the position where to start from
Parameters:
services - the Services object encapsulating informationabout the java datastructures like (static)types etc.
Parameters:
userConstraint - the Constraint with user defined instantiationsof meta variables the possible rule applications |
| removeNewRuleListener | | public void removeNewRuleListener(NewRuleListener l)(Code) | | removes a change listener to the index
Parameters:
l - the AppIndexListener to remove |
| removeNoPosTacletApp | | public void removeNoPosTacletApp(NoPosTacletApp tacletApp)(Code) | | remove a Taclet with instantiation information from the Taclet
Index of this TacletAppIndex.
Parameters:
tacletApp - the NoPosTacletApp to remove |
| reportAutomatedRuleApps | | public void reportAutomatedRuleApps(NewRuleListener l, Services services, Constraint userConstraint)(Code) | | Report all rule applications that are supposed to be applied
automatically, and that are currently stored by the index
Parameters:
l - the NewRuleListener
Parameters:
services - the Services
Parameters:
userConstraint - the Constraint capturing user defined instantiationsof meta variables |
| scanBuiltInRules | | public void scanBuiltInRules(Goal p_goal, Constraint p_userConstraint)(Code) | | Report builtin rules to all registered NewRuleListener instances.
Parameters:
p_goal - the Goal which to scan
Parameters:
p_userConstraint - the Constraint capturing user defined instantiationsof meta variables |
| sequentChanged | | public void sequentChanged(Goal goal, SequentChangeInfo sci)(Code) | | called if a formula has been replaced
Parameters:
goal - the Goal which sequent has been changed
Parameters:
sci - SequentChangeInfo describing the change of the sequent |
| tacletIndex | | public TacletIndex tacletIndex()(Code) | | returns the Taclet index for this ruleAppIndex.
|
|
|