public final class Goal
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
private ImmutableList<RuleApp> |
appliedRuleApps
list of all applied rule applications at this branch
|
private boolean |
automatic
a goal has been excluded from automatic rule application iff automatic == false
|
private Strategy |
goalStrategy
the strategy object that determines automated application of rules
|
private Goal |
linkedGoal
Marks this goal as linked (->
MergeRule ) |
private java.util.List<GoalListener> |
listeners
goal listeners
|
private NamespaceSet |
localNamespaces
The namespaces local to this goal.
|
private Node |
node |
private RuleAppIndex |
ruleAppIndex
all possible rule applications at this node are managed with this index
|
private AutomatedRuleApplicationManager |
ruleAppManager
This is the object which keeps book about all applicable rules.
|
private Properties |
strategyInfos
If an application of a rule added some information for the strategy,
then this information is stored in this map.
|
private FormulaTagManager |
tagManager
this object manages the tags for all formulas of the sequent
|
Modifier | Constructor and Description |
---|---|
|
Goal(Node node,
RuleAppIndex ruleAppIndex)
creates a new goal referencing the given node
|
private |
Goal(Node node,
RuleAppIndex ruleAppIndex,
ImmutableList<RuleApp> appliedRuleApps,
AutomatedRuleApplicationManager ruleAppManager,
Properties strategyInfos,
NamespaceSet localNamespace) |
private |
Goal(Node node,
RuleAppIndex ruleAppIndex,
ImmutableList<RuleApp> appliedRuleApps,
FormulaTagManager tagManager,
AutomatedRuleApplicationManager ruleAppManager,
Properties strategyInfos,
NamespaceSet localNamespace) |
Modifier and Type | Method and Description |
---|---|
private void |
adaptNamespacesNewGoals(ImmutableList<Goal> goalList) |
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.
|
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
|
(package private) void |
pruneToParent() |
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
|
private void |
resetLocalSymbols() |
private void |
resetTagManager() |
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.
|
private void |
setNode(Node p_node)
set the node the goal is related to
|
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
|
private Node node
private RuleAppIndex ruleAppIndex
private ImmutableList<RuleApp> appliedRuleApps
private FormulaTagManager tagManager
private Strategy goalStrategy
private AutomatedRuleApplicationManager ruleAppManager
private java.util.List<GoalListener> listeners
private boolean automatic
private final Properties strategyInfos
private NamespaceSet localNamespaces
private Goal(Node node, RuleAppIndex ruleAppIndex, ImmutableList<RuleApp> appliedRuleApps, FormulaTagManager tagManager, AutomatedRuleApplicationManager ruleAppManager, Properties strategyInfos, NamespaceSet localNamespace)
private Goal(Node node, RuleAppIndex ruleAppIndex, ImmutableList<RuleApp> appliedRuleApps, AutomatedRuleApplicationManager ruleAppManager, Properties strategyInfos, NamespaceSet localNamespace)
public Goal(Node node, RuleAppIndex ruleAppIndex)
namespaceSet
- 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)
private void setNode(Node p_node)
p_node
- the Node in the proof tree to which this goal
refers topublic 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)
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)
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)
private void resetTagManager()
public void setBranchLabel(java.lang.String s)
void pruneToParent()
private void resetLocalSymbols()
public ImmutableList<Goal> apply(RuleApp ruleApp)
private void adaptNamespacesNewGoals(ImmutableList<Goal> goalList)
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 static boolean hasApplicableRules(Goal goal)
Goal
has applicable rules.goal
- The Goal
to check.true
has applicable rules, false
no rules are applicable.public void makeLocalNamespacesFrom(NamespaceSet ns)
ns
- a non-null set of namesspaces which applies to this goal.