public final class Goal
extends java.lang.Object
Constructor and Description |
---|
Goal(Node node,
RuleAppIndex ruleAppIndex)
creates a new goal referencing the given node
|
Modifier and Type | Method and Description |
---|---|
void |
addAppliedRuleApp(RuleApp app)
puts a RuleApp to the list of the applied rule apps at this goal
and stores it in the node of the goal
|
void |
addFormula(SequentFormula cf,
boolean inAntec,
boolean first)
adds a formula to the antecedent or succedent of a
sequent.
|
void |
addFormula(SequentFormula cf,
PosInOccurrence p)
adds a formula to the sequent before the given position
and informs the rule application index about this change
|
void |
addGoalListener(GoalListener l)
adds the listener l to the list of goal listeners.
|
void |
addNoPosTacletApp(NoPosTacletApp app)
puts the NoPosTacletApp to the set of TacletApps at the node
of the goal and to the current RuleAppIndex.
|
void |
addProgramVariable(ProgramVariable pv) |
<T> void |
addStrategyInfo(Properties.Property<T> property,
T info,
StrategyInfoUndoMethod undoMethod) |
void |
addTaclet(Taclet rule,
SVInstantiations insts,
boolean isAxiom)
creates a new TacletApp and puts it to the set of TacletApps at the node
of the goal and to the current RuleAppIndex.
|
ImmutableList<RuleApp> |
appliedRuleApps()
returns set of rules applied at this branch
|
ImmutableList<Goal> |
apply(RuleApp ruleApp) |
void |
changeFormula(SequentFormula cf,
PosInOccurrence p)
replaces a formula at the given position
and informs the rule application index about this change
|
void |
clearAndDetachRuleAppIndex()
Rebuild all rule caches
|
Goal |
clone(Node node)
clones the goal (with copy of tacletindex and ruleAppIndex).
|
Goal |
copy()
like the clone method but returns right type
|
protected void |
fireAautomaticStateChanged(boolean oldAutomatic,
boolean newAutomatic) |
protected void |
fireGoalReplaced(Goal goal,
Node parent,
ImmutableList<Goal> newGoals) |
protected void |
fireSequentChanged(SequentChangeInfo sci)
informs all goal listeners about a change of the sequent
to reduce unnecessary object creation the necessary information is passed
to the listener as parameters and not through an event object.
|
java.util.List<RuleApp> |
getAllBuiltInRuleApps() |
java.util.List<TacletApp> |
getAllTacletApps(Services services) |
FormulaTagManager |
getFormulaTagManager()
this object manages the tags for all formulas of the sequent
|
Strategy |
getGoalStrategy() |
Goal |
getLinkedGoal()
Returns the goal that this goal is linked to.
|
NamespaceSet |
getLocalNamespaces()
returns the namespaces for this goal.
|
AutomatedRuleApplicationManager |
getRuleAppManager() |
<T> T |
getStrategyInfo(Properties.Property<T> property) |
long |
getTime() |
static boolean |
hasApplicableRules(Goal goal)
Checks if the
Goal has applicable rules. |
TacletIndex |
indexOfTaclets()
returns the Taclet index for this goal.
|
boolean |
isAutomatic()
Checks if is an automatic goal.
|
boolean |
isLinked()
Checks if is this node is linked to another
node (for example due to a
MergeRule ). |
void |
makeLocalNamespacesFrom(NamespaceSet ns)
Update the local namespaces from a namespace set.
|
Node |
node()
returns the referenced node
|
Proof |
proof()
returns the proof the goal belongs to
|
void |
removeFormula(PosInOccurrence p)
removes a formula at the given position from the sequent
and informs the rule appliccation index about this change
|
void |
removeGoalListener(GoalListener l)
removes the listener l from the list of goal listeners.
|
void |
removeLastAppliedRuleApp()
PRECONDITION: appliedRuleApps.size () > 0
|
RuleAppIndex |
ruleAppIndex()
returns the index of possible rule applications at this node
|
Sequent |
sequent()
returns the sequent of the node
|
void |
setBranchLabel(java.lang.String s) |
void |
setEnabled(boolean t)
Sets the automatic status of this goal.
|
void |
setGoalStrategy(Strategy p_goalStrategy) |
void |
setLinkedGoal(Goal linkedGoal)
Sets the node that this goal is linked to; also sets this for
all parents.
|
void |
setRuleAppManager(AutomatedRuleApplicationManager manager) |
void |
setSequent(SequentChangeInfo sci)
sets the sequent of the node
|
ImmutableList<Goal> |
split(int n)
creates n new nodes as children of the
referenced node and new
n goals that have references to these new nodes.
|
java.lang.String |
toString() |
void |
undoStrategyInfoAdd(StrategyInfoUndoMethod undoMethod) |
void |
updateRuleAppIndex()
Rebuild all rule caches
|
public Goal(Node node, RuleAppIndex ruleAppIndex)
namespaceSet
- public static boolean hasApplicableRules(Goal goal)
Goal
has applicable rules.goal
- The Goal
to check.true
has applicable rules, false
no rules are applicable.public FormulaTagManager getFormulaTagManager()
public Strategy getGoalStrategy()
public void setGoalStrategy(Strategy p_goalStrategy)
public AutomatedRuleApplicationManager getRuleAppManager()
public void setRuleAppManager(AutomatedRuleApplicationManager manager)
public Node node()
public NamespaceSet getLocalNamespaces()
public void addGoalListener(GoalListener l)
l
- the GoalListener to be addedpublic void removeGoalListener(GoalListener l)
l
- the GoalListener to be removedprotected void fireSequentChanged(SequentChangeInfo sci)
protected void fireGoalReplaced(Goal goal, Node parent, ImmutableList<Goal> newGoals)
protected void fireAautomaticStateChanged(boolean oldAutomatic, boolean newAutomatic)
public RuleAppIndex ruleAppIndex()
public TacletIndex indexOfTaclets()
public ImmutableList<RuleApp> appliedRuleApps()
public long getTime()
public Proof proof()
public Sequent sequent()
public boolean isAutomatic()
public void setEnabled(boolean t)
t
- the new status: true for automatic, false for interactivepublic boolean isLinked()
MergeRule
).public Goal getLinkedGoal()
public void setLinkedGoal(Goal linkedGoal)
TODO: Check whether it is problematic when multiple child nodes of a node are linked; in this case, the linkedNode field would be overwritten.
linkedGoal
- The goal that this goal is linked to.public void setSequent(SequentChangeInfo sci)
sci
- SequentChangeInfo containing the sequent to be set and
desribing the applied changes to the sequent of the parent nodepublic void addFormula(SequentFormula cf, PosInOccurrence p)
cf
- the SequentFormula to be addedp
- PosInOccurrence encodes the positionpublic void addFormula(SequentFormula cf, boolean inAntec, boolean first)
cf
- the SequentFormula to be addedinAntec
- boolean true(false) if SequentFormula has to be
added to antecedent (succedent)first
- boolean true if at the front, if false then cf is
added at the backpublic void changeFormula(SequentFormula cf, PosInOccurrence p)
cf
- the SequentFormula replacing the old onep
- the PosInOccurrence encoding the positionpublic void removeFormula(PosInOccurrence p)
p
- PosInOccurrence encodes the positionpublic void addNoPosTacletApp(NoPosTacletApp app)
app
- the TacletApppublic void addTaclet(Taclet rule, SVInstantiations insts, boolean isAxiom)
rule
- the Taclet of the TacletApp to createinsts
- the given instantiations of the TacletApp to be createdpublic void updateRuleAppIndex()
public void clearAndDetachRuleAppIndex()
public void addProgramVariable(ProgramVariable pv)
public Goal clone(Node node)
The local symbols are reused. This is taken care of later.
node
- the new Node to which the goal is attachedpublic Goal copy() throws java.lang.CloneNotSupportedException
java.lang.CloneNotSupportedException
public void addAppliedRuleApp(RuleApp app)
app
- the applied rule apppublic void removeLastAppliedRuleApp()
public ImmutableList<Goal> split(int n)
public void setBranchLabel(java.lang.String s)
public ImmutableList<Goal> apply(RuleApp ruleApp)
public java.lang.String toString()
toString
in class java.lang.Object
public <T> T getStrategyInfo(Properties.Property<T> property)
public <T> void addStrategyInfo(Properties.Property<T> property, T info, StrategyInfoUndoMethod undoMethod)
public void undoStrategyInfoAdd(StrategyInfoUndoMethod undoMethod)
public void makeLocalNamespacesFrom(NamespaceSet ns)
The parameter is copied and stored locally.
ns
- a non-null set of namesspaces which applies to this goal.public java.util.List<RuleApp> getAllBuiltInRuleApps()
Copyright © 2003-2019 The KeY-Project.