public class DelayedCutProcessor extends Object implements 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 String |
CUT_TACLET |
private static int |
DEC_PRED_INDEX |
private Term |
descisionPredicate |
private static String |
HIDE_LEFT_TACLET |
private static String |
HIDE_RIGHT_TACLET
The names of the taclets used by the process.
|
private 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(LinkedList<NodeGoalPair> pairs,
LinkedList<NodeGoalPair> openLeaves,
Iterator<Node> iterator,
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 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 LinkedList<Goal> |
apply(Node oldNode,
Goal goal,
RuleApp app,
TermServices services) |
private ImmutableList<Goal> |
apply(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 List<ApplicationCheck> |
getApplicationChecks() |
private int |
getGoalForHiding(ImmutableList<Goal> goals,
DelayedCut cut)
After applying the cut rule two goal result.
|
private 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 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,
List<NodeGoalPair> openLeaves)
This function uncovers the decision predicate that is hidden after
applying the cut rule.
|
private static final String HIDE_RIGHT_TACLET
private static final String HIDE_LEFT_TACLET
private static final String CUT_TACLET
private static final int DEC_PRED_INDEX
private final 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 List<ApplicationCheck> getApplicationChecks()
public DelayedCut cut()
private ImmutableList<Goal> cut(DelayedCut cut)
private ImmutableList<Goal> apply(String tacletName, Goal goal, PosInOccurrence pio)
private ImmutableList<Goal> hide(DelayedCut cut, Goal goal)
private int getGoalForHiding(ImmutableList<Goal> goals, DelayedCut cut)
private String getHideTacletName(DelayedCut cut)
private SequentFormula getSequentFormula(Goal goal, boolean decPredInAnte)
private List<NodeGoalPair> rebuildSubTrees(DelayedCut cut, Goal goal)
private LinkedList<Goal> apply(Goal goal, RuleApp app, TermServices services)
goal
- app
- private 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(LinkedList<NodeGoalPair> pairs, LinkedList<NodeGoalPair> openLeaves, Iterator<Node> iterator, LinkedList<Goal> goals)
pairs
and openLeaves
are manipulated.private void uncoverDecisionPredicate(DelayedCut cut, List<NodeGoalPair> openLeaves)