001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.proof;
012:
013: import java.util.ArrayList;
014: import java.util.Collections;
015: import java.util.Iterator;
016: import java.util.List;
017:
018: import de.uka.ilkd.key.gui.RuleAppListener;
019: import de.uka.ilkd.key.logic.*;
020: import de.uka.ilkd.key.logic.op.IteratorOfProgramVariable;
021: import de.uka.ilkd.key.logic.op.Metavariable;
022: import de.uka.ilkd.key.logic.op.ProgramVariable;
023: import de.uka.ilkd.key.logic.op.SetOfProgramVariable;
024: import de.uka.ilkd.key.proof.incclosure.BranchRestricter;
025: import de.uka.ilkd.key.proof.incclosure.IteratorOfSink;
026: import de.uka.ilkd.key.proof.proofevent.NodeChangeJournal;
027: import de.uka.ilkd.key.proof.proofevent.RuleAppInfo;
028: import de.uka.ilkd.key.rule.*;
029: import de.uka.ilkd.key.rule.inst.SVInstantiations;
030: import de.uka.ilkd.key.strategy.AutomatedRuleApplicationManager;
031: import de.uka.ilkd.key.strategy.QueueRuleApplicationManager;
032: import de.uka.ilkd.key.strategy.Strategy;
033:
034: /**
035: * A proof is represented as a tree of nodes containing sequents. The initial
036: * proof consists of just one node -- the root -- that has to be
037: * proved. Therefore it is divided up into several sub goals and so on. A
038: * single goal is not divided into sub goals any longer if the contained
039: * sequent becomes an axiom. A proof is closed if all leaves are closed. As
040: * the calculus works only on the leaves of a tree, the goals are the
041: * additional information needed for the proof is only stored at the leaves
042: * (saves memory) and not in the inner nodes. This class represents now a goal
043: * of the proof, this means a leave whose sequent is not closed. It keeps
044: * track of all applied rule applications on the branch and of the
045: * corresponding rule application index. Furthermore it offers methods for
046: * setting back several proof steps. The sequent has to be changed using the
047: * methods of Goal.
048: */
049: public class Goal {
050:
051: private Node node;
052:
053: /** all possible rule applications at this node are managed with this index */
054: private RuleAppIndex ruleAppIndex;
055:
056: /** list of all applied rule applications at this branch */
057: private ListOfRuleApp appliedRuleApps = SLListOfRuleApp.EMPTY_LIST;
058:
059: /** this object manages the tags for all formulas of the sequent */
060: private FormulaTagManager tagManager;
061:
062: /** the strategy object that determines automated application of rules */
063: private Strategy goalStrategy = null;
064:
065: /** */
066: private AutomatedRuleApplicationManager ruleAppManager;
067:
068: /** goal listeners */
069: private List listeners = new ArrayList();
070:
071: /** list of rule app listeners */
072: private static List ruleAppListenerList = Collections
073: .synchronizedList(new ArrayList(10));
074:
075: /** creates a new goal referencing the given node */
076: private Goal(Node node, RuleAppIndex ruleAppIndex,
077: ListOfRuleApp appliedRuleApps,
078: FormulaTagManager tagManager,
079: AutomatedRuleApplicationManager ruleAppManager) {
080: this .node = node;
081: this .ruleAppIndex = ruleAppIndex;
082: this .appliedRuleApps = appliedRuleApps;
083: this .tagManager = tagManager;
084: this .goalStrategy = null;
085: this .ruleAppIndex.setup(this );
086: setRuleAppManager(ruleAppManager);
087: }
088:
089: /**
090: * creates a new goal referencing the given node
091: */
092: public Goal(Node node, RuleAppIndex ruleAppIndex) {
093: this (node, ruleAppIndex, SLListOfRuleApp.EMPTY_LIST, null,
094: new QueueRuleApplicationManager());
095: tagManager = new FormulaTagManager(this );
096: }
097:
098: /** returns the simplifier that has to be used */
099: public UpdateSimplifier simplifier() {
100: return proof().simplifier();
101: }
102:
103: /** this object manages the tags for all formulas of the sequent */
104: public FormulaTagManager getFormulaTagManager() {
105: return tagManager;
106: }
107:
108: /**
109: * @return the strategy that determines automated rule applications for this
110: * goal
111: */
112: public Strategy getGoalStrategy() {
113: if (goalStrategy == null)
114: goalStrategy = proof().getActiveStrategy();
115: return goalStrategy;
116: }
117:
118: public void setGoalStrategy(Strategy p_goalStrategy) {
119: goalStrategy = p_goalStrategy;
120: ruleAppManager.clearCache();
121: }
122:
123: public AutomatedRuleApplicationManager getRuleAppManager() {
124: return ruleAppManager;
125: }
126:
127: public void setRuleAppManager(
128: AutomatedRuleApplicationManager manager) {
129: if (ruleAppManager != null) {
130: ruleAppIndex().removeNewRuleListener(ruleAppManager);
131: ruleAppManager.setGoal(null);
132: }
133:
134: ruleAppManager = manager;
135:
136: if (ruleAppManager != null) {
137: ruleAppIndex().addNewRuleListener(ruleAppManager);
138: ruleAppManager.setGoal(this );
139: }
140: }
141:
142: /**
143: * returns the referenced node
144: */
145: public Node node() {
146: return node;
147: }
148:
149: public SetOfProgramVariable getGlobalProgVars() {
150: return node().getGlobalProgVars();
151: }
152:
153: public Namespace createGlobalProgVarNamespace() {
154: final Namespace ns = new Namespace();
155: final IteratorOfProgramVariable it = getGlobalProgVars()
156: .iterator();
157: while (it.hasNext()) {
158: ns.add(it.next());
159: }
160: return ns;
161: }
162:
163: /**
164: * adds the listener l to the list of goal listeners.
165: * Attention: A listener added to this goal will be taken over when
166: * splitting into subgoals.
167: * @param l the GoalListener to be added
168: */
169: public void addGoalListener(GoalListener l) {
170: listeners.add(l);
171: }
172:
173: /**
174: * removes the listener l from the list of goal listeners.
175: * Attention: The listener is just removed from 'this' goal not from the
176: * other goals. (All goals can be accessed via proof openGoals())
177: * @param l the GoalListener to be removed
178: */
179: public void removeGoalListener(GoalListener l) {
180: listeners.remove(l);
181: }
182:
183: /**
184: * informs all goal listeners about a change of the sequent
185: * to reduce unnecessary object creation the necessary information is passed
186: * to the listener as parameters and not through an event object.
187: */
188: protected void fireSequentChanged(SequentChangeInfo sci) {
189: getFormulaTagManager().sequentChanged(this , sci);
190: ruleAppIndex().sequentChanged(this , sci);
191: for (int i = 0, sz = listeners.size(); i < sz; i++) {
192: ((GoalListener) listeners.get(i)).sequentChanged(this , sci);
193: }
194: }
195:
196: protected void fireGoalReplaced(Goal goal, Node parent,
197: ListOfGoal newGoals) {
198: for (int i = 0, sz = listeners.size(); i < sz; i++) {
199: ((GoalListener) listeners.get(i)).goalReplaced(goal,
200: parent, newGoals);
201: }
202: }
203:
204: /**
205: * adds the global program variables to a new created variable namespace
206: * that contains all the elements of the given namespace.
207: */
208: public Namespace getVariableNamespace(Namespace exNS) {
209: Namespace newNS = exNS;
210: final IteratorOfProgramVariable it = getGlobalProgVars()
211: .iterator();
212: if (it.hasNext()) {
213: newNS = newNS.extended(it.next());
214: }
215: while (it.hasNext()) {
216: newNS.add(it.next());
217: }
218: return newNS;
219: }
220:
221: public void setGlobalProgVars(SetOfProgramVariable s) {
222: node.setGlobalProgVars(s);
223: }
224:
225: /**
226: * set the node the goal is related to
227: * @param p_node the Node in the proof tree to which this goal
228: * refers to
229: */
230: private void setNode(Node p_node) {
231: if (node().sequent() != p_node.sequent()) {
232: node = p_node;
233: resetTagManager();
234: } else
235: node = p_node;
236: ruleAppIndex.setup(this );
237: }
238:
239: /**
240: * returns the index of possible rule applications at this node
241: */
242: public RuleAppIndex ruleAppIndex() {
243: return ruleAppIndex;
244: }
245:
246: /**
247: * returns the Taclet index for this goal. This is just a shortcut to the
248: * Taclet index of the RuleAppIndex
249: * @return the Taclet index assigned to this goal
250: */
251: public TacletIndex indexOfTaclets() {
252: return ruleAppIndex.tacletIndex();
253: }
254:
255: /** adds a formula to the sequent before the given position
256: * and informs the rule appliccation index about this change
257: * @param cf the ConstrainedFormula to be added
258: * @param p PosInOccurrence encodes the position
259: */
260: public void addFormula(ConstrainedFormula cf, PosInOccurrence p) {
261: setSequent(sequent().addFormula(cf, p));
262: }
263:
264: /** adds a list of formulas to the sequent before the given position
265: * and informs the rule appliccation index about this change
266: * @param insertions the ListOfConstrainedFormula to be added
267: * @param p PosInOccurrence encodes the position
268: */
269: public void addFormula(ListOfConstrainedFormula insertions,
270: PosInOccurrence p) {
271: if (!insertions.isEmpty()) {
272: setSequent(sequent().addFormula(insertions, p));
273: }
274: }
275:
276: /** adds a list of formulas to the antecedent or succedent of a
277: * sequent. Either at its front or back.
278: * and informs the rule appliccation index about this change
279: * @param insertions the ListOfConstrainedFormula to be added
280: * @param inAntec boolean true(false) if ConstrainedFormula has to be
281: * added to antecedent (succedent)
282: * @param first boolean true if at the front, if false then cf is
283: * added at the back
284: */
285: public void addFormula(ListOfConstrainedFormula insertions,
286: boolean inAntec, boolean first) {
287: if (!insertions.isEmpty()) {
288: setSequent(sequent().addFormula(insertions, inAntec, first));
289: }
290: }
291:
292: /** adds a formula to the antecedent or succedent of a
293: * sequent. Either at its front or back
294: * and informs the rule appliccation index about this change
295: * @param cf the ConstrainedFormula to be added
296: * @param inAntec boolean true(false) if ConstrainedFormula has to be
297: * added to antecedent (succedent)
298: * @param first boolean true if at the front, if false then cf is
299: * added at the back
300: */
301: public void addFormula(ConstrainedFormula cf, boolean inAntec,
302: boolean first) {
303: setSequent(sequent().addFormula(cf, inAntec, first));
304: }
305:
306: /** returns set of rules applied at this branch
307: * @return ListOfRuleApp applied rule applications
308: */
309: public ListOfRuleApp appliedRuleApps() {
310: return appliedRuleApps;
311: }
312:
313: /**
314: * @return the current time of this goal (which is just the number of
315: * applied rules)
316: */
317: public long getTime() {
318: return appliedRuleApps().size();
319: }
320:
321: /** returns the proof the goal belongs to
322: * @return the Proof the goal belongs to
323: */
324: public Proof proof() {
325: return node().proof();
326: }
327:
328: /** returns the sequent of the node
329: * @return the Sequent to be proved
330: */
331: public Sequent sequent() {
332: return node().sequent();
333: }
334:
335: /**
336: * sets the sequent of the node
337: * @param sci SequentChangeInfo containing the sequent to be set and
338: * desribing the applied changes to the sequent of the parent node
339: */
340: public void setSequent(SequentChangeInfo sci) {
341: node().setSequent(sci.sequent());
342: //VK reminder: now update the index
343: fireSequentChanged(sci);
344: }
345:
346: /**
347: * replaces a formula at the given position
348: * and informs the rule application index about this change
349: * @param cf the ConstrainedFormula replacing the old one
350: * @param p the PosInOccurrence encoding the position
351: */
352: public void changeFormula(ConstrainedFormula cf, PosInOccurrence p) {
353: setSequent(sequent().changeFormula(cf, p));
354: }
355:
356: /**
357: * replaces a formula at the given position
358: * and informs the rule appliccation index about this change
359: * @param cf the ConstrainedFormula replacing the old one
360: * @param p PosInOccurrence encodes the position
361: */
362: public void changeFormula(ListOfConstrainedFormula replacements,
363: PosInOccurrence p) {
364: setSequent(sequent().changeFormula(replacements, p));
365: }
366:
367: /** removes a formula at the given position from the sequent
368: * and informs the rule appliccation index about this change
369: * @param p PosInOccurrence encodes the position
370: */
371: public void removeFormula(PosInOccurrence p) {
372: setSequent(sequent().removeFormula(p));
373: }
374:
375: /**
376: * puts the NoPosTacletApp to the set of TacletApps at the node
377: * of the goal and to the current RuleAppIndex.
378: * @param app the TacletApp
379: */
380: public void addNoPosTacletApp(NoPosTacletApp app) {
381: node().addNoPosTacletApp(app);
382: ruleAppIndex.addNoPosTacletApp(app);
383: }
384:
385: /**
386: * creates a new TacletApp and puts it to the set of TacletApps at the node
387: * of the goal and to the current RuleAppIndex.
388: * @param rule the Taclet of the TacletApp to create
389: * @param insts the given instantiations of the TacletApp to be created
390: * @param constraint the constraint under which the taclet can be applied
391: */
392: public void addTaclet(Taclet rule, SVInstantiations insts,
393: Constraint constraint) {
394: NoPosTacletApp tacletApp = NoPosTacletApp
395: .createFixedNoPosTacletApp(rule, insts, constraint);
396: if (tacletApp != null) {
397: addNoPosTacletApp(tacletApp);
398: if (proof().env() != null) { // do not break everything
399: // because of ProofMgt
400: proof().env().registerRuleIntroducedAtNode(tacletApp,
401: node.parent());
402: }
403: }
404: }
405:
406: /**
407: * Rebuild all rule caches
408: */
409: public void updateRuleAppIndex() {
410: getRuleAppManager().clearCache();
411: ruleAppIndex.clearIndexes();
412: }
413:
414: /**
415: * Rebuild all rule caches
416: */
417: public void clearAndDetachRuleAppIndex() {
418: getRuleAppManager().clearCache();
419: ruleAppIndex.clearAndDetachCache();
420: }
421:
422: public void addProgramVariable(ProgramVariable pv) {
423: node.setGlobalProgVars(getGlobalProgVars().add(pv));
424: }
425:
426: public void addProgramVariables(Namespace ns) {
427: final IteratorOfNamed it = ns.elements().iterator();
428: while (it.hasNext()) {
429: addProgramVariable((ProgramVariable) it.next());
430: }
431: }
432:
433: /**
434: * clones the goal (with copy of tacletindex and ruleAppIndex)
435: * @return Object the clone
436: */
437: public Object clone() {
438: Goal clone = new Goal(node, ruleAppIndex.copy(),
439: appliedRuleApps, getFormulaTagManager().copy(),
440: ruleAppManager.copy());
441: clone.listeners = (List) ((ArrayList) listeners).clone();
442: return clone;
443: }
444:
445: /** like the clone method but returns right type
446: * @return Goal clone of this Goal
447: */
448: public Goal copy() {
449: return (Goal) clone();
450: }
451:
452: /**
453: * puts a RuleApp to the list of the applied rule apps at this goal
454: * and stores it in the node of the goal
455: * @param app the applied rule app
456: */
457: public void addAppliedRuleApp(RuleApp app) {
458: // Last app first makes inserting and searching faster
459: appliedRuleApps = appliedRuleApps.prepend(app);
460: node().setAppliedRuleApp(app);
461: }
462:
463: /**
464: * PRECONDITION: appliedRuleApps.size () > 0
465: */
466: public void removeAppliedRuleApp() {
467: appliedRuleApps = appliedRuleApps.tail();
468: node().setAppliedRuleApp(null);
469: }
470:
471: /** creates n new nodes as children of the
472: * referenced node and new
473: * n goals that have references to these new nodes.
474: * @return the list of new created goals.
475: */
476: public ListOfGoal split(int n) {
477: ListOfGoal goalList = SLListOfGoal.EMPTY_LIST;
478: Node parent = node(); // has to be stored because the node
479: // of this goal will be replaced
480: if (n > 0) {
481: IteratorOfSink itSinks = parent.reserveSinks(n);
482: BranchRestricter br;
483: Node newNode = null;
484: Goal newGoal = null;
485:
486: for (int i = 0; i < n; i++) {
487: if (i == 0) { // first new goal is this one
488: newGoal = this ;
489: } else { // otherwise it is a copy
490: newGoal = copy();
491: }
492: // create new node and add to tree
493: if (n > 1) {
494: br = new BranchRestricter(itSinks.next());
495: newNode = new Node(parent.proof(),
496: parent.sequent(), null, parent, br);
497: br.setNode(newNode);
498: } else
499: newNode = new Node(parent.proof(),
500: parent.sequent(), null, parent, itSinks
501: .next());
502:
503: // newNode.addNoPosTacletApps(parent.getNoPosTacletApps());
504: newNode.setGlobalProgVars(parent.getGlobalProgVars());
505: parent.add(newNode);
506:
507: // make new Goal and add to list
508: newGoal.setNode(newNode);
509:
510: goalList = goalList.prepend(newGoal);
511: }
512: }
513:
514: fireGoalReplaced(this , parent, goalList);
515:
516: return goalList;
517: }
518:
519: /**
520: * sets back the proof step that led to this goal. This goal is set to
521: * the parent node of the node corresponding to this goal. Goals given in
522: * the goal list parameter are removed from that list, if their
523: * corresponding nodes are leaves of the parent node of this goal.
524: * @param goalList the ListOfGoal with the goals to be removed
525: * @return the new list of goals where goals mapped to the leaves of
526: * the parent to this goal are removed from compared to the given list.
527: */
528: public ListOfGoal setBack(ListOfGoal goalList) {
529: final Node parent = node.parent();
530: final IteratorOfNode leavesIt = parent.leavesIterator();
531: while (leavesIt.hasNext()) {
532: Node n = leavesIt.next();
533:
534: final IteratorOfGoal goalIt = goalList.iterator();
535: while (goalIt.hasNext()) {
536: final Goal g = goalIt.next();
537:
538: if (g.node() == n && g != this ) {
539: goalList = goalList.removeFirst(g);
540:
541: }
542: }
543: }
544:
545: // ruleAppIndex.tacletIndex().setTaclets(parent.getNoPosTacletApps());
546:
547: removeTaclets();
548: setGlobalProgVars(parent.getGlobalProgVars());
549:
550: parent.cutChildrenSinks();
551: if (node.proof().env() != null) { // do not break everything
552: // because of ProofMgt
553: node.proof().mgt()
554: .ruleUnApplied(parent.getAppliedRuleApp());
555: }
556:
557: IteratorOfNode siblings = parent.childrenIterator();
558: Node[] sibls = new Node[parent.childrenCount()];
559: int i = 0;
560: while (siblings.hasNext()) {
561: sibls[i] = siblings.next();
562: i++;
563: }
564:
565: for (i = 0; i < sibls.length; i++) {
566: sibls[i].remove();
567: }
568:
569: setNode(parent);
570: removeAppliedRuleApp();
571:
572: updateRuleAppIndex();
573:
574: return goalList;
575: }
576:
577: private void resetTagManager() {
578: tagManager = new FormulaTagManager(this );
579: }
580:
581: private void removeTaclets() {
582: final IteratorOfNoPosTacletApp it = node.getNoPosTacletApps()
583: .iterator();
584: while (it.hasNext())
585: ruleAppIndex.removeNoPosTacletApp(it.next());
586: }
587:
588: public Constraint getClosureConstraint() {
589: return node().getClosureConstraint();
590: }
591:
592: public void addClosureConstraint(Constraint c) {
593: node().addClosureConstraint(c);
594: }
595:
596: public void addRestrictedMetavariable(Metavariable mv) {
597: node().addRestrictedMetavariable(mv);
598: }
599:
600: public void setBranchLabel(String s) {
601: node.getNodeInfo().setBranchLabel(s);
602: }
603:
604: /** fires the event that a rule has been applied */
605: protected void fireRuleApplied(ProofEvent p_e) {
606: synchronized (ruleAppListenerList) {
607: Iterator it = ruleAppListenerList.iterator();
608: while (it.hasNext()) {
609: ((RuleAppListener) it.next()).ruleApplied(p_e);
610: }
611: }
612: }
613:
614: public ListOfGoal apply(RuleApp p_ruleApp) {
615: //System.err.println(Thread.currentThread());
616:
617: final Proof proof = proof();
618:
619: // TODO: this is maybe not the right place for this check
620: assert proof.mgt().ruleApplicable(p_ruleApp, this ) : "Someone tried to apply the rule "
621: + p_ruleApp + " that is not justified";
622:
623: final NodeChangeJournal journal = new NodeChangeJournal(proof,
624: this );
625: addGoalListener(journal);
626:
627: final RuleApp ruleApp = completeRuleApp(p_ruleApp);
628:
629: final ListOfGoal goalList = ruleApp.execute(this , proof
630: .getServices());
631:
632: if (goalList == null) {
633: // this happens for the simplify decision procedure
634: // we do nothing in this case
635: } else if (goalList.isEmpty()) {
636: proof.closeGoal(this , ruleApp.constraint());
637: } else {
638: proof.replace(this , goalList);
639: if (ruleApp instanceof TacletApp
640: && ((TacletApp) ruleApp).taclet().closeGoal())
641: // the first new goal is the one to be closed
642: proof.closeGoal(goalList.head(), ruleApp.constraint());
643: }
644:
645: final RuleAppInfo ruleAppInfo = journal
646: .getRuleAppInfo(p_ruleApp);
647:
648: if (goalList != null)
649: fireRuleApplied(new ProofEvent(proof, ruleAppInfo));
650: return goalList;
651: }
652:
653: public static void applyUpdateSimplifier(ListOfGoal goalList) {
654: final IteratorOfGoal it = goalList.iterator();
655: while (it.hasNext()) {
656: it.next().applyUpdateSimplifier();
657: }
658: }
659:
660: public void applyUpdateSimplifier() {
661: applyUpdateSimplifier(true);
662: applyUpdateSimplifier(false);
663: }
664:
665: public void applyUpdateSimplifier(boolean antec) {
666: final Constraint userConstraint = proof().getUserConstraint()
667: .getConstraint();
668: final BuiltInRule rule = UpdateSimplificationRule.INSTANCE;
669:
670: final IteratorOfConstrainedFormula it = (antec ? sequent()
671: .antecedent() : sequent().succedent()).iterator();
672:
673: while (it.hasNext()) {
674: final ConstrainedFormula cfma = it.next();
675: final PosInOccurrence pos = new PosInOccurrence(cfma,
676: PosInTerm.TOP_LEVEL, antec);
677: if (rule.isApplicable(this , pos, userConstraint)) {
678: BuiltInRuleApp app = new BuiltInRuleApp(rule, pos,
679: userConstraint);
680: if (proof().mgt().ruleApplicable(app, this )) {
681: apply(app);
682: }
683: }
684: }
685: }
686:
687: /** toString */
688: public String toString() {
689: String result = (node.sequent().prettyprint(
690: proof().getServices()).toString());
691: return result;
692: }
693:
694: /** make Taclet instantions complete with regard to metavariables and
695: * skolem functions
696: */
697: private RuleApp completeRuleApp(RuleApp ruleApp) {
698: final Proof proof = proof();
699: if (ruleApp instanceof TacletApp) {
700: TacletApp tacletApp = (TacletApp) ruleApp;
701:
702: tacletApp = tacletApp.instantiateWithMV(this );
703:
704: ruleApp = tacletApp.createSkolemFunctions(proof
705: .getNamespaces().functions(), proof.getServices());
706: }
707: return ruleApp;
708: }
709:
710: public static void addRuleAppListener(RuleAppListener p) {
711: synchronized (ruleAppListenerList) {
712: ruleAppListenerList.add(p);
713: }
714: }
715:
716: public static void removeRuleAppListener(RuleAppListener p) {
717: synchronized (ruleAppListenerList) {
718: ruleAppListenerList.remove(p);
719: }
720: }
721:
722: }
|