| Method Summary |
|
| public void | addAppliedRuleApp(RuleApp app)
|
| public void | addClosureConstraint(Constraint c)
|
| public void | addFormula(ConstrainedFormula cf, PosInOccurrence p)
|
| public void | addFormula(ListOfConstrainedFormula insertions, PosInOccurrence p)
|
| public void | addFormula(ListOfConstrainedFormula insertions, boolean inAntec, boolean first)
adds a list of formulas to the antecedent or succedent of a
sequent. |
| public void | addFormula(ConstrainedFormula cf, boolean inAntec, boolean first)
adds a formula to the antecedent or succedent of a
sequent. |
| public void | addGoalListener(GoalListener l)
adds the listener l to the list of goal listeners.
Attention: A listener added to this goal will be taken over when
splitting into subgoals. |
| public void | addNoPosTacletApp(NoPosTacletApp app)
puts the NoPosTacletApp to the set of TacletApps at the node
of the goal and to the current RuleAppIndex. |
| public void | addProgramVariable(ProgramVariable pv)
|
| public void | addProgramVariables(Namespace ns)
|
| public void | addRestrictedMetavariable(Metavariable mv)
|
| public static void | addRuleAppListener(RuleAppListener p)
|
| public void | addTaclet(Taclet rule, SVInstantiations insts, Constraint constraint)
creates a new TacletApp and puts it to the set of TacletApps at the node
of the goal and to the current RuleAppIndex. |
| public ListOfRuleApp | appliedRuleApps()
|
| public ListOfGoal | apply(RuleApp p_ruleApp)
|
| public static void | applyUpdateSimplifier(ListOfGoal goalList)
|
| public void | applyUpdateSimplifier()
|
| public void | applyUpdateSimplifier(boolean antec)
|
| public void | changeFormula(ConstrainedFormula cf, PosInOccurrence p)
|
| public void | changeFormula(ListOfConstrainedFormula replacements, PosInOccurrence p)
|
| public void | clearAndDetachRuleAppIndex()
|
| public Object | clone()
|
| public Goal | copy()
|
| public Namespace | createGlobalProgVarNamespace()
|
| protected void | fireGoalReplaced(Goal goal, Node parent, ListOfGoal newGoals)
|
| protected void | fireRuleApplied(ProofEvent p_e)
|
| 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. |
| public Constraint | getClosureConstraint()
|
| public FormulaTagManager | getFormulaTagManager()
|
| public SetOfProgramVariable | getGlobalProgVars()
|
| public Strategy | getGoalStrategy()
|
| public AutomatedRuleApplicationManager | getRuleAppManager()
|
| public long | getTime()
|
| public Namespace | getVariableNamespace(Namespace exNS)
adds the global program variables to a new created variable namespace
that contains all the elements of the given namespace. |
| public TacletIndex | indexOfTaclets()
returns the Taclet index for this goal. |
| public Node | node()
|
| public Proof | proof()
|
| public void | removeAppliedRuleApp()
|
| public void | removeFormula(PosInOccurrence p)
|
| public void | removeGoalListener(GoalListener l)
removes the listener l from the list of goal listeners.
Attention: The listener is just removed from 'this' goal not from the
other goals. |
| public static void | removeRuleAppListener(RuleAppListener p)
|
| public RuleAppIndex | ruleAppIndex()
|
| public Sequent | sequent()
|
| public ListOfGoal | setBack(ListOfGoal goalList)
sets back the proof step that led to this goal. |
| public void | setBranchLabel(String s)
|
| public void | setGlobalProgVars(SetOfProgramVariable s)
|
| public void | setGoalStrategy(Strategy p_goalStrategy)
|
| public void | setRuleAppManager(AutomatedRuleApplicationManager manager)
|
| public void | setSequent(SequentChangeInfo sci)
|
| public UpdateSimplifier | simplifier()
|
| public ListOfGoal | split(int n)
creates n new nodes as children of the
referenced node and new
n goals that have references to these new nodes. |
| public String | toString()
|
| public void | updateRuleAppIndex()
|
