public class DelayedCut
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
private int |
cutMode |
static int |
DECISION_PREDICATE_IN_ANTECEDENT |
static int |
DECISION_PREDICATE_IN_SUCCEDENT |
private Term |
decisionPredicate |
private RuleApp |
firstAppliedRuleApp |
private ImmutableList<NodeGoalPair> |
goalsAfterUncovering |
private NoPosTacletApp |
hideApp |
private Node |
node |
private Proof |
proof |
private Goal |
remainingGoal |
private ImmutableList<Node> |
subtrees |
Constructor and Description |
---|
DelayedCut(Proof proof,
Node node,
Term formula,
ImmutableList<Node> subtrees,
int sideOfDecisionPredicate,
RuleApp firstAppliedRuleApp) |
Modifier and Type | Method and Description |
---|---|
int |
getCutMode() |
RuleApp |
getFirstAppliedRuleApp() |
Term |
getFormula() |
ImmutableList<NodeGoalPair> |
getGoalsAfterUncovering() |
NoPosTacletApp |
getHideApp() |
Node |
getNode() |
Proof |
getProof() |
Goal |
getRemainingGoal() |
Services |
getServices() |
ImmutableList<Node> |
getSubtrees() |
boolean |
isDecisionPredicateInAntecendet() |
(package private) void |
setGoalsAfterUncovering(ImmutableList<NodeGoalPair> goalsAfterUncovering) |
(package private) void |
setHideApp(NoPosTacletApp hideApp) |
(package private) void |
setRemainingGoal(Goal remainingGoal) |
public static final int DECISION_PREDICATE_IN_ANTECEDENT
public static final int DECISION_PREDICATE_IN_SUCCEDENT
private final Proof proof
private final Node node
private final ImmutableList<Node> subtrees
private final int cutMode
private final Term decisionPredicate
private final RuleApp firstAppliedRuleApp
private NoPosTacletApp hideApp
private ImmutableList<NodeGoalPair> goalsAfterUncovering
private Goal remainingGoal
public Term getFormula()
public RuleApp getFirstAppliedRuleApp()
public Services getServices()
public Node getNode()
public Proof getProof()
void setHideApp(NoPosTacletApp hideApp)
void setGoalsAfterUncovering(ImmutableList<NodeGoalPair> goalsAfterUncovering)
void setRemainingGoal(Goal remainingGoal)
public Goal getRemainingGoal()
public ImmutableList<NodeGoalPair> getGoalsAfterUncovering()
public NoPosTacletApp getHideApp()
public ImmutableList<Node> getSubtrees()
public int getCutMode()
public boolean isDecisionPredicateInAntecendet()