public class FocussedRuleApplicationManager extends java.lang.Object implements DelegationBasedAutomatedRuleApplicationManager
Modifier and Type | Field and Description |
---|---|
private AutomatedRuleApplicationManager |
delegate |
private FormulaTag |
focussedFormula |
private PosInOccurrence |
focussedSubterm |
private Goal |
goal |
private boolean |
onlyModifyFocussedFormula |
QueueRuleApplicationManager |
rootManager |
Modifier | Constructor and Description |
---|---|
private |
FocussedRuleApplicationManager(AutomatedRuleApplicationManager delegate,
Goal goal,
FormulaTag focussedFormula,
PosInOccurrence focussedSubterm,
boolean onlyModifyFocussedFormula) |
|
FocussedRuleApplicationManager(AutomatedRuleApplicationManager delegate,
Goal goal,
PosInOccurrence focussedSubterm) |
Modifier and Type | Method and Description |
---|---|
void |
clearCache()
Clear existing caches of applicable rules
|
java.lang.Object |
clone() |
AutomatedRuleApplicationManager |
copy() |
AutomatedRuleApplicationManager |
getDelegate() |
private PosInOccurrence |
getPIOForFocussedSubterm() |
private boolean |
isBelow(PosInOccurrence over,
PosInOccurrence under) |
protected boolean |
isRuleApplicationForFocussedFormula(RuleApp rule,
PosInOccurrence pos) |
private boolean |
isSameFormula(PosInOccurrence pio1,
PosInOccurrence pio2) |
RuleApp |
next() |
RuleApp |
peekNext() |
void |
ruleAdded(RuleApp rule,
PosInOccurrence pos)
Called when a new RuleApp is added
|
void |
rulesAdded(ImmutableList<? extends RuleApp> rules,
PosInOccurrence pos)
Called when a collection of new RuleApps is added
|
void |
setGoal(Goal p_goal)
Set the goal
this is the rule app manager for |
private final AutomatedRuleApplicationManager delegate
public final QueueRuleApplicationManager rootManager
private final FormulaTag focussedFormula
private final PosInOccurrence focussedSubterm
private Goal goal
private boolean onlyModifyFocussedFormula
private FocussedRuleApplicationManager(AutomatedRuleApplicationManager delegate, Goal goal, FormulaTag focussedFormula, PosInOccurrence focussedSubterm, boolean onlyModifyFocussedFormula)
public FocussedRuleApplicationManager(AutomatedRuleApplicationManager delegate, Goal goal, PosInOccurrence focussedSubterm)
public void clearCache()
AutomatedRuleApplicationManager
clearCache
in interface AutomatedRuleApplicationManager
public AutomatedRuleApplicationManager copy()
copy
in interface AutomatedRuleApplicationManager
public java.lang.Object clone()
clone
in class java.lang.Object
public RuleApp peekNext()
peekNext
in interface AutomatedRuleApplicationManager
public RuleApp next()
next
in interface AutomatedRuleApplicationManager
public void setGoal(Goal p_goal)
AutomatedRuleApplicationManager
this
is the rule app manager forsetGoal
in interface AutomatedRuleApplicationManager
public void ruleAdded(RuleApp rule, PosInOccurrence pos)
NewRuleListener
ruleAdded
in interface NewRuleListener
protected boolean isRuleApplicationForFocussedFormula(RuleApp rule, PosInOccurrence pos)
public void rulesAdded(ImmutableList<? extends RuleApp> rules, PosInOccurrence pos)
NewRuleListener
rulesAdded
in interface NewRuleListener
private boolean isSameFormula(PosInOccurrence pio1, PosInOccurrence pio2)
private PosInOccurrence getPIOForFocussedSubterm()
private boolean isBelow(PosInOccurrence over, PosInOccurrence under)
public AutomatedRuleApplicationManager getDelegate()
getDelegate
in interface DelegationBasedAutomatedRuleApplicationManager