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.HashSet;
015: import java.util.List;
016: import java.util.Vector;
017:
018: import de.uka.ilkd.key.gui.GUIEvent;
019: import de.uka.ilkd.key.gui.configuration.ProofSettings;
020: import de.uka.ilkd.key.gui.configuration.SettingsListener;
021: import de.uka.ilkd.key.java.JavaInfo;
022: import de.uka.ilkd.key.java.Services;
023: import de.uka.ilkd.key.logic.*;
024: import de.uka.ilkd.key.pp.AbbrevMap;
025: import de.uka.ilkd.key.proof.init.InitConfig;
026: import de.uka.ilkd.key.proof.init.Profile;
027: import de.uka.ilkd.key.proof.mgt.BasicTask;
028: import de.uka.ilkd.key.proof.mgt.DefaultProofCorrectnessMgt;
029: import de.uka.ilkd.key.proof.mgt.ProofCorrectnessMgt;
030: import de.uka.ilkd.key.proof.mgt.ProofEnvironment;
031: import de.uka.ilkd.key.rule.UpdateSimplifier;
032: import de.uka.ilkd.key.strategy.Strategy;
033: import de.uka.ilkd.key.strategy.StrategyFactory;
034: import de.uka.ilkd.key.strategy.StrategyProperties;
035:
036: /**
037: * A proof is represented as a tree whose nodes are created by
038: * applying rules on the current (open) goals and dividing them up
039: * into several new subgoals. To distinguish between open goals (the
040: * ones we are working on) and closed goals or inner nodes we restrict
041: * the use of the word goal to open goals which are a subset of the
042: * proof tree's leaves. This proof class represents a proof and
043: * encapsulates its tree structure. The {@link Goal} class represents
044: * a goal with all needed extra information, and methods to apply
045: * rules. Furthermore it offers services that deliver the open goals,
046: * namespaces and several other informations about the current state
047: * of the proof.
048: */
049: public class Proof implements Named {
050:
051: /** name of the proof */
052: private Name name;
053:
054: /** the root of the proof */
055: private Node root;
056:
057: /**
058: * list with prooftree listeners of this proof
059: * attention: firing events makes use of array list's random access
060: * nature
061: */
062: private List listenerList = new ArrayList(10);
063:
064: /** list with the open goals of the proof */
065: private ListOfGoal openGoals = SLListOfGoal.EMPTY_LIST;
066:
067: /** during closure this can be set by "subTreeCompletelyClosed" */
068: private Node closedSubtree = null;
069:
070: /** declarations &c, read from a problem file or otherwise */
071: private String problemHeader = "";
072:
073: /** the update simplifier (may be moved to nodes)*/
074: private UpdateSimplifier upd_simplifier;
075:
076: /** the java information object: JavaInfo+TypeConverter */
077: private final Services services;
078:
079: /** maps the Abbreviations valid for this proof to their corresponding terms.*/
080: private AbbrevMap abbreviations = new AbbrevMap();
081:
082: /** User constraint */
083: private ConstraintTableModel userConstraint = new ConstraintTableModel();
084:
085: /** Deliverer for new metavariables */
086: private MetavariableDeliverer metavariableDeliverer;
087:
088: /** the environment of the proof with specs and java model*/
089: private ProofEnvironment proofEnv;
090:
091: /** the environment of the proof with specs and java model*/
092: private ProofCorrectnessMgt localMgt;
093:
094: private BasicTask task;
095:
096: private ProofSettings settings;
097:
098: /**
099: * when different users load and save a proof this vector fills up with
100: * Strings containing the user names.
101: * */
102: public Vector userLog;
103:
104: /**
105: * when load and save a proof with different versions of key this vector
106: * fills up with Strings containing the prcs versions.
107: */
108: public Vector keyVersionLog;
109:
110: private Strategy activeStrategy;
111:
112: /** constructs a new empty proof with name */
113: private Proof(Name name, Services services, ProofSettings settings) {
114: this .name = name;
115: assert services != null : "Tried to create proof without valid services.";
116: this .services = services.copyProofSpecific();
117: this .settings = settings;
118:
119: metavariableDeliverer = new MetavariableDeliverer(this );
120: addConstraintListener();
121:
122: addStrategyListener();
123: }
124:
125: /**
126: * initialises the strategies
127: */
128: private void initStrategy() {
129: StrategyProperties activeStrategyProperties = settings
130: .getStrategySettings().getActiveStrategyProperties();
131:
132: final Profile profile = settings.getProfile();
133:
134: if (profile.supportsStrategyFactory(settings
135: .getStrategySettings().getStrategy())) {
136: setActiveStrategy(profile.getStrategyFactory(
137: settings.getStrategySettings().getStrategy())
138: .create(this , activeStrategyProperties));
139: } else {
140: setActiveStrategy(profile.getDefaultStrategyFactory()
141: .create(this , activeStrategyProperties));
142: }
143: }
144:
145: /** constructs a new empty proof */
146: public Proof(Services services) {
147: this ("", services);
148: }
149:
150: /** constructs a new empty proof with name */
151: public Proof(String name, Services services) {
152: this (new Name(name), services, new ProofSettings(
153: ProofSettings.DEFAULT_SETTINGS));
154: }
155:
156: private Proof(String name, Sequent problem, TacletIndex rules,
157: BuiltInRuleIndex builtInRules, Services services,
158: ProofSettings settings) {
159:
160: this (new Name(name), services, settings);
161:
162: localMgt = new DefaultProofCorrectnessMgt(this );
163:
164: Node rootNode = new Node(this , problem);
165: setRoot(rootNode);
166:
167: Goal firstGoal = new Goal(rootNode, new RuleAppIndex(
168: new TacletAppIndex(rules), new BuiltInRuleAppIndex(
169: builtInRules)));
170: openGoals = openGoals.prepend(firstGoal);
171:
172: if (closed())
173: fireProofClosed();
174: }
175:
176: public Proof(String name, Term problem, String header,
177: TacletIndex rules, BuiltInRuleIndex builtInRules,
178: Services services, ProofSettings settings) {
179: this (name, Sequent
180: .createSuccSequent(Semisequent.EMPTY_SEMISEQUENT
181: .insert(0, new ConstrainedFormula(problem))
182: .semisequent()), rules, builtInRules, services,
183: settings);
184: problemHeader = header;
185: }
186:
187: public Proof(String name, Sequent sequent, String header,
188: TacletIndex rules, BuiltInRuleIndex builtInRules,
189: Services services, ProofSettings settings) {
190: this (name, sequent, rules, builtInRules, services, settings);
191: problemHeader = header;
192: }
193:
194: /** copy constructor */
195: public Proof(Proof p) {
196: this (p.name, p.env().getInitConfig().getServices(),
197: new ProofSettings(p.settings));
198: activeStrategy = StrategyFactory.create(this , p
199: .getActiveStrategy().name().toString(), getSettings()
200: .getStrategySettings().getActiveStrategyProperties());
201:
202: InitConfig ic = p.env().getInitConfig();
203: Node rootNode = new Node(this , p.root.sequent());
204: setRoot(rootNode);
205: Goal firstGoal = new Goal(rootNode, new RuleAppIndex(
206: new TacletAppIndex(ic.createTacletIndex()),
207: new BuiltInRuleAppIndex(ic.createBuiltInRuleIndex())));
208: localMgt = new DefaultProofCorrectnessMgt(this );
209: openGoals = openGoals.prepend(firstGoal);
210: setNamespaces(ic.namespaces());
211: }
212:
213: public Proof(String name, Term problem, String header,
214: TacletIndex rules, BuiltInRuleIndex builtInRules,
215: Services services) {
216: this (name, problem, header, rules, builtInRules, services,
217: new ProofSettings(ProofSettings.DEFAULT_SETTINGS));
218: }
219:
220: /**
221: * returns the name of the proof. Describes in short what has to be proved.
222: * @return the name of the proof
223: */
224: public Name name() {
225: return name;
226: }
227:
228: public String header() {
229: return problemHeader;
230: }
231:
232: public ProofCorrectnessMgt mgt() {
233: return localMgt;
234: }
235:
236: /**
237: * returns a collection of the namespaces valid for this proof
238: */
239: public NamespaceSet getNamespaces() {
240: return getServices().getNamespaces();
241: }
242:
243: /** returns the JavaInfo with the java type information */
244: public JavaInfo getJavaInfo() {
245: return getServices().getJavaInfo();
246: }
247:
248: /** returns the Services with the java service classes */
249: public Services getServices() {
250: return services;
251: }
252:
253: /** sets the variable, function, sort, heuristics namespaces */
254: public void setNamespaces(NamespaceSet ns) {
255: getServices().setNamespaces(ns);
256: if (openGoals().size() > 1)
257: throw new IllegalStateException(
258: "Proof: ProgVars set too late");
259: openGoals().head().addProgramVariables(ns.programVariables());
260: }
261:
262: public void setBasicTask(BasicTask t) {
263: task = t;
264: }
265:
266: public BasicTask getBasicTask() {
267: return task;
268: }
269:
270: public AbbrevMap abbreviations() {
271: return abbreviations;
272: }
273:
274: public Strategy getActiveStrategy() {
275: if (activeStrategy == null) {
276: initStrategy();
277: }
278: return activeStrategy;
279: }
280:
281: public void setActiveStrategy(Strategy activeStrategy) {
282: this .activeStrategy = activeStrategy;
283: getSettings().getStrategySettings().setStrategy(
284: activeStrategy.name());
285: updateStrategyOnGoals();
286: }
287:
288: private void updateStrategyOnGoals() {
289: Strategy ourStrategy = getActiveStrategy();
290:
291: final IteratorOfGoal it = openGoals().iterator();
292: while (it.hasNext())
293: it.next().setGoalStrategy(ourStrategy);
294: }
295:
296: /**
297: * returns the default simplifier to be used (may be overwritten by branch
298: * specific simplifiers in the future)
299: * @return the UpdateSimplifier to be used as default one
300: */
301: public UpdateSimplifier simplifier() {
302: return upd_simplifier;
303: }
304:
305: /**
306: * sets the default simplifier
307: * @param upd_simplifier the UpdateSimplifier to be used as
308: * default (may be overwritten by branch specific simplifiers in the future)
309: */
310: public void setSimplifier(UpdateSimplifier upd_simplifier) {
311: this .upd_simplifier = upd_simplifier;
312: }
313:
314: /** returns the user constraint (table model)
315: * @return the user constraint
316: */
317: public ConstraintTableModel getUserConstraint() {
318: return userConstraint;
319: }
320:
321: private void addConstraintListener() {
322: getUserConstraint().addConstraintTableListener(
323: new ConstraintTableListener() {
324: public void constraintChanged(ConstraintTableEvent e) {
325: clearAndDetachRuleAppIndexes();
326: }
327: });
328: }
329:
330: private void addStrategyListener() {
331: getSettings().getStrategySettings().addSettingsListener(
332: new SettingsListener() {
333: public void settingsChanged(GUIEvent config) {
334: updateStrategyOnGoals();
335: }
336: });
337: }
338:
339: private void clearAndDetachRuleAppIndexes() {
340: // Taclet indices of the particular goals have to
341: // be rebuilt
342: final IteratorOfGoal it = openGoals().iterator();
343: while (it.hasNext())
344: it.next().clearAndDetachRuleAppIndex();
345: }
346:
347: /** @return Deliverer of new metavariables (with unique names)*/
348: public MetavariableDeliverer getMetavariableDeliverer() {
349: return metavariableDeliverer;
350: }
351:
352: public JavaModel getJavaModel() {
353: return proofEnv.getJavaModel();
354: }
355:
356: public void setProofEnv(ProofEnvironment env) {
357: proofEnv = env;
358: }
359:
360: public ProofEnvironment env() {
361: return proofEnv;
362: }
363:
364: /**
365: * returns the root node of the proof
366: */
367: public Node root() {
368: return root;
369: }
370:
371: /** sets the root of the proof */
372: public void setRoot(Node root) {
373: if (this .root != null) {
374: throw new IllegalStateException(
375: "Tried to reset the root of the proof.");
376: } else {
377: this .root = root;
378: fireProofStructureChanged();
379:
380: if (closed())
381: fireProofClosed();
382: }
383: }
384:
385: public void setSettings(ProofSettings newSettings) {
386: settings = newSettings;
387: addStrategyListener();
388: }
389:
390: public ProofSettings getSettings() {
391: return settings;
392: }
393:
394: /**
395: * returns the list of open goals
396: * @return list with the open goals
397: */
398: public ListOfGoal openGoals() {
399: return openGoals;
400: }
401:
402: /**
403: * removes the given goal and adds the new goals in list
404: * @param oldGoal the old goal that has to be removed from list
405: * @param newGoals the ListOfGoal with the new goals that were
406: * result of a rule application on goal
407: */
408: public void replace(Goal oldGoal, ListOfGoal newGoals) {
409: openGoals = openGoals.removeAll(oldGoal);
410:
411: if (closed())
412: fireProofClosed();
413: else {
414: fireProofGoalRemoved(oldGoal);
415: add(newGoals);
416: }
417: }
418:
419: /**
420: * Add the given constraint to the closure constraint of the given
421: * goal, i.e. the given goal is closed if p_c is satisfied.
422: */
423: public void closeGoal(Goal p_goal, Constraint p_c) {
424: p_goal.addClosureConstraint(p_c);
425:
426: removeClosedSubtree();
427:
428: if (closed())
429: fireProofClosed();
430: }
431:
432: /**
433: * This is called by a Node that is the root of a subtree that is
434: * closed
435: */
436: public void subtreeCompletelyClosed(Node p_node) {
437: // This method will be called for nodes with increasing
438: // distance to the root
439: if (closedSubtree == null)
440: closedSubtree = p_node;
441: }
442:
443: /**
444: * Use this information to remove the goals of the closed subtree
445: */
446: protected void removeClosedSubtree() {
447: // give the information that a subtree is closed
448: // to all nodes below this node
449: if (closedSubtree != null)
450: closedSubtree.setClosed();
451:
452: if (!closed() && closedSubtree != null) {
453:
454: boolean b = false;
455: IteratorOfNode it = closedSubtree.leavesIterator();
456: Goal goal;
457:
458: while (it.hasNext()) {
459: goal = getGoal(it.next());
460: if (goal != null) {
461: b = true;
462: remove(goal);
463: }
464: }
465:
466: if (b)
467: // For the moment it is necessary to fire the message ALWAYS
468: // in order to detect branch closing.
469: fireProofGoalsAdded(SLListOfGoal.EMPTY_LIST);
470: }
471:
472: closedSubtree = null;
473: }
474:
475: /** removes the given goal from the list of open goals. Take care
476: * removing the last goal will fire the proofClosed event
477: * @param goal the Goal to be removed
478: */
479: public void remove(Goal goal) {
480: ListOfGoal newOpenGoals = openGoals.removeAll(goal);
481: if (newOpenGoals != openGoals) {
482: openGoals = newOpenGoals;
483: if (closed()) {
484: fireProofClosed();
485: } else {
486: fireProofGoalRemoved(goal);
487: }
488: }
489: }
490:
491: /** adds a new goal to the list of goals
492: * @param goal the Goal to be added
493: */
494: public void add(Goal goal) {
495: ListOfGoal newOpenGoals = openGoals.prepend(goal);
496: if (openGoals != newOpenGoals) {
497: openGoals = newOpenGoals;
498: fireProofGoalsAdded(goal);
499: }
500: }
501:
502: /** adds a list with new goals to the list of open goals
503: * @param goals the ListOfGoal to be prepended
504: */
505: public void add(ListOfGoal goals) {
506: ListOfGoal newOpenGoals = openGoals.prepend(goals);
507: if (openGoals != newOpenGoals) {
508: openGoals = newOpenGoals;
509: }
510:
511: // For the moment it is necessary to fire the message ALWAYS
512: // in order to detect branch closing.
513: fireProofGoalsAdded(goals);
514:
515: }
516:
517: /** Return whether the remaining goals can be closed, i.e. whether
518: * the conjunction of the constraints of the open goals is
519: * satisfiable. In this case all remaining open goals are removed.
520: */
521: public boolean closed() {
522: if (root().getRootSink().isSatisfiable()) {
523: Goal goal;
524: while (openGoals != SLListOfGoal.EMPTY_LIST) {
525: goal = openGoals.head();
526: openGoals = openGoals.tail();
527: fireProofGoalRemoved(goal);
528: }
529: return true;
530: }
531: return false;
532: }
533:
534: /** returns true iff sets back to the step that created the given
535: * goal. If the undo operation was succesful true is returned.
536: * @param goal the Goal desribing the location where to set back
537: * @return true iff undo operation was succesfull.
538: */
539: public boolean setBack(Goal goal) {
540: if (goal != null) {
541: Node parent = goal.node().parent();
542: if (parent != null) {
543: getServices().setBackCounters(goal.node());
544: openGoals = goal.setBack(openGoals);
545: fireProofGoalsChanged();
546: return true;
547: }
548: }
549: // root reached or proof closed
550: return false;
551: }
552:
553: /** Prunes away the subtree beneath <code>node</code>.
554: * <code>node</code> is going to be the last node on its
555: * branch.
556: * @param node the node desribing the location where to set back
557: * @return true iff undo operation was succesfull.
558: */
559: public boolean setBack(Node node) {
560: final Goal goal = getGoal(node);
561: if (goal != null) {
562: return true;
563: } else {
564: final ListOfGoal goalList = getSubtreeGoals(node);
565: if (!goalList.isEmpty()) {
566: // The subtree goals (goalList) are scanned for common
567: // direct ancestors (parents). Afterwards the remove
568: // list is the greatest subset of the subtree goals such
569: // that the parents of the goals are disjoint.
570: final HashSet parentSet = new HashSet();
571: final IteratorOfGoal goalIt = goalList.iterator();
572: ListOfGoal removeList = SLListOfGoal.EMPTY_LIST;
573: while (goalIt.hasNext()) {
574: final Goal nextGoal = goalIt.next();
575: if (!parentSet.contains(nextGoal.node().parent())) {
576: removeList = removeList.prepend(nextGoal);
577: parentSet.add(nextGoal.node().parent());
578: }
579: }
580: //call setBack(Goal) on each element in the remove
581: //list. The former parents become the new goals
582: final IteratorOfGoal removeIt = removeList.iterator();
583: while (removeIt.hasNext()) {
584: setBack(removeIt.next());
585: }
586: return setBack(node);
587: }
588: return false;
589: }
590: }
591:
592: // ?? seems to be required for presentation uses
593: // I think there is a mismatch between what the method does and the method's
594: // name. Can the one who implemented this method check the name and write a
595: // short comment about its purpose %%RB
596: public void updateProof() {
597: fireProofGoalsChanged();
598: }
599:
600: /** fires the event that the proof has been expanded at the given node */
601: protected void fireProofExpanded(Node node) {
602: ProofTreeEvent e = new ProofTreeEvent(this , node);
603: for (int i = 0; i < listenerList.size(); i++) {
604: ((ProofTreeListener) listenerList.get(i)).proofExpanded(e);
605: }
606: }
607:
608: /** fires the event that the proof has been pruned at the given node */
609: protected void fireProofPruned(Node node, Node removedNode) {
610: ProofTreeEvent e = new ProofTreeRemovedNodeEvent(this , node,
611: removedNode);
612: for (int i = 0; i < listenerList.size(); i++) {
613: ((ProofTreeListener) listenerList.get(i)).proofPruned(e);
614: }
615: }
616:
617: /** fires the event that the proof has been restructured */
618: protected void fireProofStructureChanged() {
619: ProofTreeEvent e = new ProofTreeEvent(this );
620: for (int i = 0; i < listenerList.size(); i++) {
621: ((ProofTreeListener) listenerList.get(i))
622: .proofStructureChanged(e);
623: }
624: }
625:
626: /** fires the event that a goal has been removed from the list of goals */
627: protected void fireProofGoalRemoved(Goal goal) {
628: ProofTreeEvent e = new ProofTreeEvent(this , goal);
629: for (int i = 0; i < listenerList.size(); i++) {
630: ((ProofTreeListener) listenerList.get(i))
631: .proofGoalRemoved(e);
632: }
633: }
634:
635: /** fires the event that new goals have been added to the list of
636: * goals
637: */
638: protected void fireProofGoalsAdded(ListOfGoal goals) {
639: ProofTreeEvent e = new ProofTreeEvent(this , goals);
640: for (int i = 0; i < listenerList.size(); i++) {
641: ((ProofTreeListener) listenerList.get(i))
642: .proofGoalsAdded(e);
643: }
644: }
645:
646: /** fires the event that new goals have been added to the list of
647: * goals
648: */
649: protected void fireProofGoalsAdded(Goal goal) {
650: fireProofGoalsAdded(SLListOfGoal.EMPTY_LIST.prepend(goal));
651: }
652:
653: /** fires the event that the proof has been restructured */
654: protected void fireProofGoalsChanged() {
655: ProofTreeEvent e = new ProofTreeEvent(this , openGoals());
656: for (int i = 0; i < listenerList.size(); i++) {
657: ((ProofTreeListener) listenerList.get(i))
658: .proofGoalsChanged(e);
659: }
660: }
661:
662: /** fires the event that the proof has closed.
663: * This event fired instead of the proofGoalRemoved event when
664: * the last goal in list is removed.
665: */
666: protected void fireProofClosed() {
667: ProofTreeEvent e = new ProofTreeEvent(this );
668: for (int i = 0; i < listenerList.size(); i++) {
669: ((ProofTreeListener) listenerList.get(i)).proofClosed(e);
670: }
671: }
672:
673: /**
674: * adds a listener to the proof
675: * @param listener the ProofTreeListener to be added
676: */
677: public synchronized void addProofTreeListener(
678: ProofTreeListener listener) {
679: synchronized (listenerList) {
680: listenerList.add(listener);
681: }
682: }
683:
684: /**
685: * removes a listener from the proof
686: * @param listener the ProofTreeListener to be removed
687: */
688: public synchronized void removeProofTreeListener(
689: ProofTreeListener listener) {
690: synchronized (listenerList) {
691: listenerList.remove(listener);
692: }
693: }
694:
695: public synchronized boolean containsProofTreeListener(
696: ProofTreeListener listener) {
697: synchronized (listenerList) {
698: return listenerList.contains(listener);
699: }
700: }
701:
702: /** returns true if the given node is part of a Goal
703: * @return true if the given node is part of a Goal
704: */
705: public boolean isGoal(Node node) {
706: return getGoal(node) != null;
707: }
708:
709: /** returns the goal that belongs to the given node or null if the
710: * node is an inner one
711: * @return the goal that belongs to the given node or null if the
712: * node is an inner one
713: */
714: public Goal getGoal(Node node) {
715: Goal result = null;
716: IteratorOfGoal it = openGoals.iterator();
717: while (it.hasNext()) {
718: result = it.next();
719: if (result.node() == node) {
720: return result;
721: }
722: }
723: return null;
724: }
725:
726: /** returns the list of goals of the subtree starting with node
727: * @param node the Node where to start from
728: * @return the list of goals of the subtree starting with node
729: */
730: public ListOfGoal getSubtreeGoals(Node node) {
731: ListOfGoal result = SLListOfGoal.EMPTY_LIST;
732: final IteratorOfGoal goalsIt = openGoals.iterator();
733: while (goalsIt.hasNext()) {
734: final Goal goal = goalsIt.next();
735: final IteratorOfNode leavesIt = node.leavesIterator();
736: while (leavesIt.hasNext()) {
737: if (leavesIt.next() == goal.node()) {
738: result = result.prepend(goal);
739: }
740: }
741: }
742: return result;
743: }
744:
745: /** returns true iff the given node is found in the proof tree
746: * @param node the Node to search for
747: * @return true iff the given node is found in the proof tree
748: */
749: public boolean find(Node node) {
750: if (root == null) {
751: return false;
752: }
753: return root.find(node);
754: }
755:
756: /**
757: * retrieves number of nodes
758: */
759: public int countNodes() {
760: return root.countNodes();
761: }
762:
763: /**
764: * Currently the rule app index can either operate in interactive mode (and
765: * contain applications of all existing taclets) or in automatic mode (and
766: * only contain a restricted set of taclets that can possibly be applied
767: * automated). This distinction could be replaced with a more general way to
768: * control the contents of the rule app index
769: */
770: public void setRuleAppIndexToAutoMode() {
771: IteratorOfGoal it = openGoals.iterator();
772: while (it.hasNext()) {
773: it.next().ruleAppIndex().autoModeStarted();
774: }
775: }
776:
777: public void setRuleAppIndexToInteractiveMode() {
778: IteratorOfGoal it = openGoals.iterator();
779: while (it.hasNext()) {
780: it.next().ruleAppIndex().autoModeStopped();
781: }
782: }
783:
784: public void addRuleSource(RuleSource src) {
785: problemHeader += src.getInclusionString() + "\n";
786: }
787:
788: /**
789: * retrieves number of branches
790: */
791: public int countBranches() {
792: return root.countBranches();
793: }
794:
795: public String statistics() {
796: return "Nodes:" + countNodes() + "\n" + "Branches: "
797: + countBranches() + "\n";
798: }
799:
800: /** toString */
801: public String toString() {
802: StringBuffer result = new StringBuffer();
803: result.append("Proof -- ");
804: if (!"".equals(name.toString())) {
805: result.append(name.toString());
806: } else {
807: result.append("unnamed");
808: }
809: result.append("\nProoftree:\n");
810: result.append(root.toString());
811: return result.toString();
812: }
813:
814: }
|