public class DelayedCutProcessor
extends java.lang.Object
implements java.lang.Runnable
This class is responsible for processing the delayed cut. The information
about the cut is stored in DelayedCut
. For each cut a new object
of this class must be created. The cutting process consists of three steps:
DECISION_PREDICATE_IN_ANTECEDENT
: The pruned subtree is attached
to the goal having F in its antecedent.DECISION_PREDICATE_IN_SUCCEDENT
: The pruned subtree is attached
to the goal having F in its succedent.
REMARK: Before you change this class, see the comment at the method
apply
.
Modifier and Type | Field and Description |
---|---|
private static java.lang.String |
CUT_TACLET |
private static int |
DEC_PRED_INDEX |
private Term |
descisionPredicate |
private static java.lang.String |
HIDE_LEFT_TACLET |
private static java.lang.String |
HIDE_RIGHT_TACLET
The names of the taclets used by the process.
|
private java.util.LinkedList<DelayedCutListener> |
listeners |
private int |
mode |
private Node |
node |
private Proof |
proof |
private boolean |
used |
Constructor and Description |
---|
DelayedCutProcessor(Proof proof,
Node node,
Term descisionPredicate,
int mode) |
Modifier and Type | Method and Description |
---|---|
void |
add(DelayedCutListener listener) |
private int |
add(java.util.LinkedList<NodeGoalPair> pairs,
java.util.LinkedList<NodeGoalPair> openLeaves,
java.util.Iterator<Node> iterator,
java.util.LinkedList<Goal> goals)
Used for rebuilding the tree: Joins the node of the old sub trees and the
corresponding goals in the new tree to one object.
|
private java.util.LinkedList<Goal> |
apply(Goal goal,
RuleApp app,
TermServices services)
CAUTION: The order of the goals is crucial for the success of the delayed
cut.
|
private java.util.LinkedList<Goal> |
apply(Node oldNode,
Goal goal,
RuleApp app,
TermServices services) |
private ImmutableList<Goal> |
apply(java.lang.String tacletName,
Goal goal,
PosInOccurrence pio) |
private void |
check(Goal goal,
RuleApp app,
PosInOccurrence newPos,
Services services) |
private RuleApp |
createNewRuleApp(NodeGoalPair pair,
Services services)
Based on an old rule application a new rule application is built.
|
DelayedCut |
cut() |
private ImmutableList<Goal> |
cut(DelayedCut cut) |
private Goal |
find(Proof proof,
Node node) |
static java.util.List<ApplicationCheck> |
getApplicationChecks() |
private int |
getGoalForHiding(ImmutableList<Goal> goals,
DelayedCut cut)
After applying the cut rule two goal result.
|
private java.lang.String |
getHideTacletName(DelayedCut cut) |
private SequentFormula |
getSequentFormula(Goal goal,
boolean decPredInAnte) |
private ImmutableList<Goal> |
hide(DelayedCut cut,
Goal goal)
Hides the formula that has been added by the hide process.
|
private java.util.List<NodeGoalPair> |
rebuildSubTrees(DelayedCut cut,
Goal goal)
Rebuilds the subtree pruned by the process, that is the rules are
replayed.
|
void |
remove(DelayedCutListener listener) |
void |
run() |
private PosInOccurrence |
translate(NodeGoalPair pair,
TermServices services) |
private void |
uncoverDecisionPredicate(DelayedCut cut,
java.util.List<NodeGoalPair> openLeaves)
This function uncovers the decision predicate that is hidden after
applying the cut rule.
|
private static final java.lang.String HIDE_RIGHT_TACLET
private static final java.lang.String HIDE_LEFT_TACLET
private static final java.lang.String CUT_TACLET
private static final int DEC_PRED_INDEX
private final java.util.LinkedList<DelayedCutListener> listeners
private final Proof proof
private final Node node
private final Term descisionPredicate
private final int mode
private boolean used
public void add(DelayedCutListener listener)
public void remove(DelayedCutListener listener)
public static java.util.List<ApplicationCheck> getApplicationChecks()
public DelayedCut cut()
private ImmutableList<Goal> cut(DelayedCut cut)
private ImmutableList<Goal> apply(java.lang.String tacletName, Goal goal, PosInOccurrence pio)
private ImmutableList<Goal> hide(DelayedCut cut, Goal goal)
private int getGoalForHiding(ImmutableList<Goal> goals, DelayedCut cut)
private java.lang.String getHideTacletName(DelayedCut cut)
private SequentFormula getSequentFormula(Goal goal, boolean decPredInAnte)
private java.util.List<NodeGoalPair> rebuildSubTrees(DelayedCut cut, Goal goal)
private java.util.LinkedList<Goal> apply(Goal goal, RuleApp app, TermServices services)
goal
- app
- private java.util.LinkedList<Goal> apply(Node oldNode, Goal goal, RuleApp app, TermServices services)
private RuleApp createNewRuleApp(NodeGoalPair pair, Services services)
private void check(Goal goal, RuleApp app, PosInOccurrence newPos, Services services)
private PosInOccurrence translate(NodeGoalPair pair, TermServices services)
private int add(java.util.LinkedList<NodeGoalPair> pairs, java.util.LinkedList<NodeGoalPair> openLeaves, java.util.Iterator<Node> iterator, java.util.LinkedList<Goal> goals)
pairs
and openLeaves
are manipulated.private void uncoverDecisionPredicate(DelayedCut cut, java.util.List<NodeGoalPair> openLeaves)
public void run()
run
in interface java.lang.Runnable