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.*;
014:
015: import de.uka.ilkd.key.logic.Constraint;
016: import de.uka.ilkd.key.logic.ListOfRenamingTable;
017: import de.uka.ilkd.key.logic.Sequent;
018: import de.uka.ilkd.key.logic.op.*;
019: import de.uka.ilkd.key.proof.incclosure.*;
020: import de.uka.ilkd.key.proof.reuse.ReusePoint;
021: import de.uka.ilkd.key.rule.*;
022: import de.uka.ilkd.key.util.Debug;
023:
024: public class Node {
025: /** the proof the node belongs to */
026: private Proof proof;
027:
028: private Sequent seq = Sequent.EMPTY_SEQUENT;
029:
030: private List children = new LinkedList();
031:
032: private Node parent = null;
033:
034: private RuleApp appliedRuleApp;
035:
036: private SetOfProgramVariable globalProgVars = SetAsListOfProgramVariable.EMPTY_SET;
037:
038: private boolean closed = false;
039:
040: /** Root sink if this is a root node */
041: private BufferSink rootSink = null;
042:
043: private BufferSink localSink;
044:
045: /** Parent of all sinks on this branch */
046: private Sink branchSink;
047:
048: /** For children.size()>1 this merger will be used */
049: private MultiMerger forkMerger = null;
050:
051: /** contains non-logical content, used for user feedback */
052: private NodeInfo nodeInfo;
053:
054: int reuseCandidate = 0;
055:
056: private boolean persistentCandidate = false;
057:
058: private ReusePoint reuseSource;
059:
060: int serialNr;
061:
062: private int siblingNr = -1;
063:
064: private ListOfRenamingTable renamings;
065:
066: /**
067: * If the rule base has been extended e.g. by loading a new taclet as
068: * lemma or by applying a taclet with an addrule section on this node,
069: * then these taclets are stored in this set
070: */
071: private SetOfNoPosTacletApp localIntroducedRules = SetAsListOfNoPosTacletApp.EMPTY_SET;
072:
073: /** creates an empty node that is root and leaf.
074: */
075: public Node(Proof proof) {
076: this .proof = proof;
077: rootSink = new BufferSink(null);
078: branchSink = new BranchRestricter(rootSink);
079: ((BranchRestricter) branchSink).setNode(this );
080: localSink = new BufferSink(branchSink);
081: serialNr = proof.getServices().getCounter("nodes")
082: .getCountPlusPlus(this );
083: nodeInfo = new NodeInfo(this );
084: }
085:
086: /** creates a node with the given contents
087: */
088: public Node(Proof proof, Sequent seq) {
089: this (proof);
090: this .seq = seq;
091: serialNr = proof.getServices().getCounter("nodes")
092: .getCountPlusPlus(this );
093: }
094:
095: /** creates a node with the given contents, the given collection
096: * of children (all elements must be of class Node) and the given
097: * parent node.
098: */
099: public Node(Proof proof, Sequent seq, List children, Node parent,
100: Sink branchSink) {
101: this .proof = proof;
102: this .seq = seq;
103: this .parent = parent;
104: this .branchSink = branchSink;
105: localSink = new BufferSink(branchSink);
106: if (children != null) {
107: this .children = children;
108: }
109: serialNr = proof.getServices().getCounter("nodes")
110: .getCountPlusPlus(this );
111: nodeInfo = new NodeInfo(this );
112: }
113:
114: /** sets the sequent at this node
115: */
116: public void setSequent(Sequent seq) {
117: this .seq = seq;
118: }
119:
120: /** returns the sequent of this node */
121: public Sequent sequent() {
122: return seq;
123: }
124:
125: /**
126: * the node information object encapsulates non-logical information
127: * of the node, e.g.
128: *
129: * @return
130: */
131: public NodeInfo getNodeInfo() {
132: return nodeInfo;
133: }
134:
135: /** returns the proof the Node belongs to */
136: public Proof proof() {
137: return proof;
138: }
139:
140: public void setAppliedRuleApp(RuleApp ruleApp) {
141: this .appliedRuleApp = ruleApp;
142: }
143:
144: public void setRenamings(ListOfRenamingTable list) {
145: renamings = list;
146: }
147:
148: public ListOfRenamingTable getRenamingTable() {
149: return renamings;
150: }
151:
152: public RuleApp getAppliedRuleApp() {
153: return appliedRuleApp;
154: }
155:
156: /** Returns the set of NoPosTacletApps at this node */
157: public SetOfNoPosTacletApp getNoPosTacletApps() {
158: return localIntroducedRules;
159: }
160:
161: public SetOfProgramVariable getGlobalProgVars() {
162: return globalProgVars;
163: }
164:
165: public void setGlobalProgVars(SetOfProgramVariable progVars) {
166: globalProgVars = progVars;
167: }
168:
169: /**
170: * adds a new NoPosTacletApp to the set of available NoPosTacletApps
171: * at this node
172: */
173: public void addNoPosTacletApp(NoPosTacletApp s) {
174: localIntroducedRules = localIntroducedRules.add(s);
175: }
176:
177: /** returns the parent node of this node.
178: */
179: public Node parent() {
180: return parent;
181: }
182:
183: /** returns true, iff this node is a leaf, i.e. has no children.
184: */
185: public boolean leaf() {
186: return children.size() == 0;
187: }
188:
189: /** searches for a given node in the subtree starting with this node */
190: public boolean find(Node node) {
191: // we assume that the proof tree node is part of has proper
192: // links
193:
194: while (node != this ) {
195: if (node.root())
196: return false;
197: node = node.parent();
198: }
199:
200: return true;
201: }
202:
203: /**
204: * Search for the node being the root of the smallest subtree
205: * containing <code>this</code> and <code>p_node</code>; we assume
206: * that the two nodes are part of the same proof tree
207: */
208: public Node commonAncestor(Node p_node) {
209: if (root())
210: return this ;
211: if (p_node.root())
212: return p_node;
213:
214: HashSet paths = new HashSet();
215: Node n = this ;
216:
217: while (true) {
218: if (!paths.add(n))
219: return n;
220: if (n.root())
221: break;
222: n = n.parent();
223:
224: if (!paths.add(p_node))
225: return p_node;
226: if (p_node.root()) {
227: p_node = n;
228: break;
229: }
230: p_node = p_node.parent();
231: }
232:
233: while (!paths.contains(p_node))
234: p_node = p_node.parent();
235:
236: return p_node;
237: }
238:
239: /** returns true, iff this node is root, i.e. has no parents.
240: */
241: public boolean root() {
242: return parent == null;
243: }
244:
245: /**
246: * Reserve p_count sinks meant for children and return them. If
247: * ultimately more than one sink is needed, the first call to this
248: * method MUST have p_count>1.
249: */
250: public IteratorOfSink reserveSinks(int p_count) {
251: if (p_count == 1 && forkMerger == null)
252: return SLListOfSink.EMPTY_LIST.prepend(branchSink)
253: .iterator();
254: else {
255: int i = 0;
256:
257: if (forkMerger == null)
258: forkMerger = new MultiMerger(branchSink, p_count, proof
259: .getServices());
260: else {
261: i = forkMerger.getArity();
262: forkMerger.expand(i + p_count);
263: }
264:
265: IteratorOfSink it = forkMerger.getSinks();
266: while (i-- != 0)
267: it.next();
268:
269: return it;
270: }
271: }
272:
273: /**
274: * Remove a possibly existing merger, restore the old state by
275: * calling "localSink.reset()". Currently this doesn't really
276: * remove the connection between the children sinks and the branch
277: * sink.
278: */
279: public void cutChildrenSinks() {
280: if (forkMerger != null)
281: forkMerger = null;
282:
283: resetBranchSink();
284: }
285:
286: /**
287: *
288: */
289: public void resetBranchSink() {
290: localSink.reset();
291: }
292:
293: public BufferSink insertLocalRootSink() {
294: Debug.assertFalse(forkMerger == null,
295: "insertLocalRootSink() must only be called for "
296: + "nodes with multiple children");
297:
298: final BufferSink localRoot = new BufferSink(null);
299: forkMerger.setParent(localRoot);
300:
301: return localRoot;
302: }
303:
304: public void removeLocalRootSink() {
305: Debug.assertFalse(forkMerger == null,
306: "removeLocalRootSink() must only be called for "
307: + "nodes with multiple children");
308:
309: forkMerger.setParent(branchSink);
310: }
311:
312: /** makes the given node a child of this node.
313: */
314: public void add(Node child) {
315: child.siblingNr = children.size();
316: children.add(child);
317: child.parent = this ;
318: proof.fireProofExpanded(this );
319: }
320:
321: /** removes child/parent relationship between this node and its
322: * parent; if this node is root nothing happens.
323: */
324: public void remove() {
325: if (parent != null) {
326: parent.remove(this );
327: }
328: }
329:
330: /** removes child/parent relationship between the given node and
331: * this node; if the given node is not child of this node,
332: * nothing happens and then and only then false is returned.
333: * @return false iff the given node was not child of this node and
334: * nothing has been done.
335: */
336: public boolean remove(Node child) {
337: if (children.remove(child)) {
338: child.parent = null;
339:
340: final ListIterator it = children
341: .listIterator(child.siblingNr);
342: while (it.hasNext()) {
343: ((Node) it.next()).siblingNr--;
344: }
345: child.siblingNr = -1;
346: proof().fireProofPruned(this , child);
347: return true;
348: } else {
349: return false;
350: }
351: }
352:
353: /**
354: * computes the leaves of the current subtree and returns them
355: */
356: private List leaves() {
357: final List leaves = new LinkedList();
358: final LinkedList nodesToCheck = new LinkedList();
359: nodesToCheck.add(this );
360: while (!nodesToCheck.isEmpty()) {
361: final Node n = (Node) nodesToCheck.removeFirst();
362: if (n.leaf()) {
363: leaves.add(n);
364: } else {
365: nodesToCheck.addAll(0, n.children);
366: }
367: }
368: return leaves;
369: }
370:
371: /**
372: * returns an iterator for the leaves of the subtree below this
373: * node. The computation is called at every call!
374: */
375: public IteratorOfNode leavesIterator() {
376: return new NodeIterator(leaves().iterator());
377: }
378:
379: /** returns an iterator for the direct children of this node.
380: */
381: public IteratorOfNode childrenIterator() {
382: return new NodeIterator(children.iterator());
383: }
384:
385: /** returns number of children */
386: public int childrenCount() {
387: return children.size();
388: }
389:
390: /** returns i-th child */
391: public Node child(int i) {
392: return (Node) (children.get(i));
393: }
394:
395: /**
396: * @return the number of the node <code>p_node</code>, if it is a
397: * child of this node (starting with <code>0</code>),
398: * <code>-1</code> otherwise
399: */
400: public int getChildNr(Node p_node) {
401: int res = 0;
402: IteratorOfNode it = childrenIterator();
403:
404: while (it.hasNext()) {
405: if (it.next() == p_node)
406: return res;
407: ++res;
408: }
409:
410: return -1;
411: }
412:
413: /** helps toString method
414: * @param prefix needed to keep track if a line has to be printed
415: * @param tree the tree representation we want to add this subtree
416: " @param preEnumeration the enumeration of the parent without the
417: * last number
418: * @param postNr the last number of the parents enumeration
419: * @param maxNr the number of nodes at this level
420: * @param ownNr the place of this node at this level
421: */
422:
423: private StringBuffer toString(String prefix, StringBuffer tree,
424: String preEnumeration, int postNr, int maxNr, int ownNr) {
425: IteratorOfNode childrenIt = childrenIterator();
426: // Some constants
427: String frontIndent = (maxNr > 1 ? " " : "");
428: String backFill = " "; // same length as connectNode without
429: // frontIndent
430: String connectNode = (maxNr > 1 ? frontIndent + "+--" : "");
431: String verticalLine = (maxNr > 1 ? frontIndent + "|" + backFill
432: : " |");
433:
434: // get enumeration
435: String newEnumeration = preEnumeration;
436: int newPostNr = 0;
437: if (maxNr > 1) {
438: newEnumeration += postNr + "." + ownNr + ".";
439: newPostNr = 1;
440: } else {
441: newPostNr = postNr + ownNr;
442: }
443:
444: // node is printed
445:
446: if (postNr != 0) { // not starting node (usually not root)
447: // prefix is appended twice in order to get an
448: // empty line between two nodes
449: tree.append(prefix);
450: tree.append(verticalLine);
451: tree.append("\n");
452: tree.append(prefix);
453: // indent node
454: tree.append(connectNode);
455: }
456:
457: tree.append("(" + newEnumeration + newPostNr + ") "
458: + sequent().toString() + "\n");
459:
460: // create new prefix
461: if (ownNr < maxNr) {
462: // connect node with next node of same level
463: prefix += verticalLine;
464: } else if (ownNr == maxNr && maxNr > 1) {
465: // last node of level no further connection
466: prefix += frontIndent + " " + backFill;
467: } else if (ownNr != maxNr && maxNr <= 1) {
468: prefix = "";
469: }
470:
471: // print subtrees
472: int childId = 0;
473: while (childrenIt.hasNext()) {
474: childId++;
475: childrenIt.next().toString(prefix, tree, newEnumeration,
476: newPostNr, children.size(), childId);
477: }
478:
479: return tree;
480: }
481:
482: public String toString() {
483: StringBuffer tree = new StringBuffer();
484: return "\n" + toString("", tree, "", 0, 0, 1);
485: }
486:
487: public String name() { // XXX this is called way too often -- cache stuff!
488:
489: RuleApp rap = getAppliedRuleApp();
490: if (rap == null) {
491: Goal goal = proof.getGoal(this );
492: if (goal == null
493: || proof().getUserConstraint().displayClosed(this ))
494: return "Closed goal";
495: else
496: return "OPEN GOAL";
497: }
498: if (rap.rule() == null)
499: return "rule application without rule";
500:
501: if (nodeInfo.getFirstStatementString() != null) {
502: return nodeInfo.getFirstStatementString();
503: }
504:
505: String text = rap.rule().displayName();
506: if (text == null) {
507: text = "rule without name";
508: }
509: return text;
510: }
511:
512: private static Vector reuseCandidates = new Vector(20);
513:
514: public static Iterator reuseCandidatesIterator() {
515: return reuseCandidates.iterator();
516: }
517:
518: public static int reuseCandidatesNumber() {
519: return reuseCandidates.size();
520: }
521:
522: public void markReuseCandidate() {
523: reuseCandidate++;
524: reuseCandidates.add(this );
525: }
526:
527: public void markPersistentCandidate() {
528: persistentCandidate = true;
529: }
530:
531: public void unmarkReuseCandidate() {
532: if ((reuseCandidate > 1) || !persistentCandidate) {
533: reuseCandidate--;
534: reuseCandidates.remove(this );
535: }
536: }
537:
538: public static void clearReuseCandidates() {
539: Enumeration en = reuseCandidates.elements();
540: while (en.hasMoreElements()) {
541: Node n = (Node) en.nextElement();
542: n.reuseCandidate = 0;
543: n.persistentCandidate = false;
544: }
545: reuseCandidates = new Vector(20);
546: }
547:
548: public static void clearReuseCandidates(Proof p) {
549: Enumeration en = reuseCandidates.elements();
550: while (en.hasMoreElements()) {
551: Node n = (Node) en.nextElement();
552: if (n.proof() == p)
553: reuseCandidates.remove(n);
554: }
555: }
556:
557: public boolean isReuseCandidate() {
558: return reuseCandidate > 0;
559: }
560:
561: public void setReuseSource(ReusePoint rp) {
562: reuseSource = rp;
563: }
564:
565: public ReusePoint getReuseSource() {
566: return reuseSource;
567: }
568:
569: /**
570: * checks if the parent has this node as child and continues recursively
571: * with the children of this node.
572: * @return true iff the parent of this node has this node as child and
573: * this condition holds also for the own children.
574: */
575: public boolean sanityCheckDoubleLinks() {
576: if (!root()) {
577: if (!parent().children.contains(this )) {
578: return false;
579: }
580: if (parent.proof() != proof()) {
581: return false;
582: }
583: }
584: if (!leaf()) {
585: IteratorOfNode it = childrenIterator();
586: while (it.hasNext()) {
587: if (!it.next().sanityCheckDoubleLinks())
588: return false;
589: }
590: }
591: return true;
592: }
593:
594: public Constraint getClosureConstraint() {
595: return localSink.getConstraint();
596: }
597:
598: public void addClosureConstraint(Constraint c) {
599: localSink.put(c);
600: }
601:
602: public void addRestrictedMetavariable(Metavariable mv) {
603: localSink.addRestriction(mv);
604: }
605:
606: public SetOfMetavariable getRestrictedMetavariables() {
607: if (branchSink instanceof Restricter)
608: return ((Restricter) branchSink).getRestrictions();
609: else
610: return SetAsListOfMetavariable.EMPTY_SET;
611: }
612:
613: public BufferSink getRootSink() {
614: return rootSink;
615: }
616:
617: public Sink getBranchSink() {
618: return branchSink;
619: }
620:
621: /**
622: * This is called by "BranchRestricter" to indicate that the
623: * subtree below this Node is closed
624: */
625: public void subtreeCompletelyClosed() {
626: proof().subtreeCompletelyClosed(this );
627: }
628:
629: public void setClosed() {
630: final LinkedList subTreeNodes = new LinkedList();
631: subTreeNodes.add(this );
632: while (!subTreeNodes.isEmpty()) {
633: final Node n = (Node) subTreeNodes.removeFirst();
634: n.closed = true;
635: subTreeNodes.addAll(n.children);
636: }
637: }
638:
639: public boolean isClosed() {
640: return closed;
641: }
642:
643: /**
644: * retrieves number of nodes
645: */
646: public int countNodes() {
647: int nodes = 1 + children.size();
648: final LinkedList nodesToAdd = (LinkedList) ((LinkedList) children)
649: .clone();
650: while (!nodesToAdd.isEmpty()) {
651: final Node n = (Node) nodesToAdd.removeFirst();
652: nodesToAdd.addAll(n.children);
653: nodes += n.children.size();
654: }
655: return nodes;
656: }
657:
658: /**
659: * retrieves number of branches
660: */
661: public int countBranches() {
662: return leaves().size();
663: }
664:
665: public int serialNr() {
666: return serialNr;
667: }
668:
669: /**
670: * returns the sibling number of this node or <tt>-1</tt> if
671: * it is the root node
672: * @return the sibling number of this node or <tt>-1</tt> if
673: * it is the root node
674: */
675: public int siblingNr() {
676: return siblingNr;
677: }
678:
679: // inner iterator class
680: private class NodeIterator implements IteratorOfNode {
681: private Iterator it;
682:
683: NodeIterator(Iterator it) {
684: this .it = it;
685: }
686:
687: public boolean hasNext() {
688: return it.hasNext();
689: }
690:
691: public Node next() {
692: return (Node) it.next();
693: }
694: }
695:
696: private int getIntroducedRulesCount() {
697: int c = 0;
698:
699: if (parent != null) {
700: c = parent.getIntroducedRulesCount();
701: }
702:
703: return c + localIntroducedRules.size();
704: }
705:
706: public int getUniqueTacletNr() {
707: return getIntroducedRulesCount();
708: }
709:
710: }
|