de.uka.ilkd.key.proof.delayedcut

Class DelayedCut

java.lang.Object

de.uka.ilkd.key.proof.delayedcut.DelayedCut

public class DelayedCut
extends java.lang.Object

This class wraps the information about the delayed cut. It only wraps data but not functional information.

Author:

Benjamin Niedermann

Field Summary

Fields

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 Summary

Constructors

Constructor and Description
DelayedCut(Proof proof, Node node, Term formula, ImmutableList<Node> subtrees, int sideOfDecisionPredicate, RuleApp firstAppliedRuleApp)

Method Summary

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)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

DECISION_PREDICATE_IN_ANTECEDENT

public static final int DECISION_PREDICATE_IN_ANTECEDENT

See Also:

Constant Field Values

DECISION_PREDICATE_IN_SUCCEDENT

public static final int DECISION_PREDICATE_IN_SUCCEDENT

See Also:

Constant Field Values

proof

private final Proof proof

node

private final Node node

subtrees

private final ImmutableList<Node> subtrees

cutMode

private final int cutMode

decisionPredicate

private final Term decisionPredicate

firstAppliedRuleApp

private final RuleApp firstAppliedRuleApp

hideApp

private NoPosTacletApp hideApp

goalsAfterUncovering

private ImmutableList<NodeGoalPair> goalsAfterUncovering

remainingGoal

private Goal remainingGoal

Constructor Detail

DelayedCut

public DelayedCut(Proof proof,
                  Node node,
                  Term formula,
                  ImmutableList<Node> subtrees,
                  int sideOfDecisionPredicate,
                  RuleApp firstAppliedRuleApp)

Method Detail

getFormula

public Term getFormula()

getFirstAppliedRuleApp

public RuleApp getFirstAppliedRuleApp()

getServices

public Services getServices()

getNode

public Node getNode()

getProof

public Proof getProof()

setHideApp

void setHideApp(NoPosTacletApp hideApp)

setGoalsAfterUncovering

void setGoalsAfterUncovering(ImmutableList<NodeGoalPair> goalsAfterUncovering)

setRemainingGoal

void setRemainingGoal(Goal remainingGoal)

getRemainingGoal

public Goal getRemainingGoal()

getGoalsAfterUncovering

public ImmutableList<NodeGoalPair> getGoalsAfterUncovering()

getHideApp

public NoPosTacletApp getHideApp()

getSubtrees

public ImmutableList<Node> getSubtrees()

getCutMode

public int getCutMode()

isDecisionPredicateInAntecendet

public boolean isDecisionPredicateInAntecendet()