public class DelayedCut
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
static int |
DECISION_PREDICATE_IN_ANTECEDENT |
static int |
DECISION_PREDICATE_IN_SUCCEDENT |
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() |
public static final int DECISION_PREDICATE_IN_ANTECEDENT
public static final int DECISION_PREDICATE_IN_SUCCEDENT
public Term getFormula()
public RuleApp getFirstAppliedRuleApp()
public Services getServices()
public Node getNode()
public Proof getProof()
public Goal getRemainingGoal()
public ImmutableList<NodeGoalPair> getGoalsAfterUncovering()
public NoPosTacletApp getHideApp()
public ImmutableList<Node> getSubtrees()
public int getCutMode()
public boolean isDecisionPredicateInAntecendet()
Copyright © 2003-2019 The KeY-Project.