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
.
Constructor and Description |
---|
DelayedCutProcessor(Proof proof,
Node node,
Term descisionPredicate,
int mode) |
Modifier and Type | Method and Description |
---|---|
void |
add(DelayedCutListener listener) |
DelayedCut |
cut() |
static java.util.List<ApplicationCheck> |
getApplicationChecks() |
void |
remove(DelayedCutListener listener) |
void |
run() |
public void add(DelayedCutListener listener)
public void remove(DelayedCutListener listener)
public static java.util.List<ApplicationCheck> getApplicationChecks()
public DelayedCut cut()
public void run()
run
in interface java.lang.Runnable
Copyright © 2003-2019 The KeY-Project.