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.logic;
012:
013: import junit.framework.TestCase;
014: import de.uka.ilkd.key.logic.op.Function;
015: import de.uka.ilkd.key.logic.op.Metavariable;
016: import de.uka.ilkd.key.logic.op.RigidFunction;
017: import de.uka.ilkd.key.logic.sort.PrimitiveSort;
018: import de.uka.ilkd.key.logic.sort.Sort;
019:
020: /** class tests the PosInOccurrence
021: */
022:
023: public class TestPosInOcc extends TestCase {
024:
025: public TestPosInOcc(String name) {
026: super (name);
027: }
028:
029: public void testIterator() {
030: TermFactory tf = TermFactory.DEFAULT;
031: Sort sort1 = new PrimitiveSort(new Name("S1"));
032: Metavariable x = new Metavariable(new Name("x"), sort1);
033: Function f = new RigidFunction(new Name("f"), sort1,
034: new Sort[] { sort1 });
035: Function p = new RigidFunction(new Name("p"), Sort.FORMULA,
036: new Sort[] { sort1 });
037:
038: Term terms[] = new Term[3];
039: terms[0] = tf.createFunctionTerm(x);
040: terms[1] = tf.createFunctionTerm(f, new Term[] { terms[0] });
041: terms[2] = tf.createFunctionTerm(p, new Term[] { terms[1] });
042:
043: PosInOccurrence pio = new PosInOccurrence(
044: new ConstrainedFormula(terms[2], Constraint.BOTTOM),
045: PosInTerm.TOP_LEVEL, true);
046:
047: PIOPathIterator it = pio.iterator();
048:
049: // a top-level position
050:
051: assertTrue(it.hasNext());
052: assertTrue(it.next() == -1 && it.getSubTerm() == terms[2]
053: && it.getPosInOccurrence().subTerm() == terms[2]
054: && it.getChild() == -1);
055:
056: // two nodes deeper
057:
058: pio = pio.down(0).down(0);
059: it = pio.iterator();
060:
061: assertTrue(it.hasNext());
062: assertTrue(it.next() == 0 && it.getSubTerm() == terms[2]
063: && it.getPosInOccurrence().subTerm() == terms[2]
064: && it.getChild() == 0);
065:
066: assertTrue(it.hasNext());
067: assertTrue(it.next() == 0 && it.getSubTerm() == terms[1]
068: && it.getPosInOccurrence().subTerm() == terms[1]
069: && it.getChild() == 0);
070:
071: assertTrue(it.hasNext());
072: assertTrue(it.next() == -1 && it.getSubTerm() == terms[0]
073: && it.getPosInOccurrence().subTerm() == terms[0]
074: && it.getChild() == -1);
075:
076: assertFalse(it.hasNext());
077:
078: // add a term below a metavariable
079:
080: pio = pio.setTermBelowMetavariable(terms[1]);
081: it = pio.iterator();
082:
083: assertTrue(it.hasNext());
084: assertTrue(it.next() == 0 && it.getSubTerm() == terms[2]
085: && it.getPosInOccurrence().subTerm() == terms[2]
086: && it.getChild() == 0);
087:
088: assertTrue(it.hasNext());
089: assertTrue(it.next() == 0 && it.getSubTerm() == terms[1]
090: && it.getPosInOccurrence().subTerm() == terms[1]
091: && it.getChild() == 0);
092:
093: assertTrue(it.hasNext());
094: assertTrue(it.next() == -1 && it.getSubTerm() == terms[1]
095: && it.getPosInOccurrence().subTerm() == terms[1]
096: && it.getChild() == -1);
097:
098: assertFalse(it.hasNext());
099:
100: // add a term below a metavariable
101:
102: pio = pio.down(0);
103: it = pio.iterator();
104:
105: assertTrue(it.hasNext());
106: assertTrue(it.next() == 0 && it.getSubTerm() == terms[2]
107: && it.getPosInOccurrence().subTerm() == terms[2]
108: && it.getChild() == 0);
109:
110: assertTrue(it.hasNext());
111: assertTrue(it.next() == 0 && it.getSubTerm() == terms[1]
112: && it.getPosInOccurrence().subTerm() == terms[1]
113: && it.getChild() == 0);
114:
115: assertTrue(it.hasNext());
116: assertTrue(it.next() == 0 && it.getSubTerm() == terms[1]
117: && it.getPosInOccurrence().subTerm() == terms[1]
118: && it.getChild() == 0);
119:
120: assertTrue(it.hasNext());
121: assertTrue(it.next() == -1 && it.getSubTerm() == terms[0]
122: && it.getPosInOccurrence().subTerm() == terms[0]
123: && it.getChild() == -1);
124:
125: assertFalse(it.hasNext());
126:
127: // without the <code>hasNext()</code>-calls
128:
129: it = pio.iterator();
130:
131: assertTrue(it.next() == 0 && it.getSubTerm() == terms[2]
132: && it.getPosInOccurrence().subTerm() == terms[2]
133: && it.getChild() == 0);
134:
135: assertTrue(it.next() == 0 && it.getSubTerm() == terms[1]
136: && it.getPosInOccurrence().subTerm() == terms[1]
137: && it.getChild() == 0);
138:
139: assertTrue(it.next() == 0 && it.getSubTerm() == terms[1]
140: && it.getPosInOccurrence().subTerm() == terms[1]
141: && it.getChild() == 0);
142:
143: assertTrue(it.next() == -1 && it.getSubTerm() == terms[0]
144: && it.getPosInOccurrence().subTerm() == terms[0]
145: && it.getChild() == -1);
146: }
147:
148: public void testReplaceConstrainedFormula() {
149: TermFactory tf = TermFactory.DEFAULT;
150: Sort sort1 = new PrimitiveSort(new Name("S1"));
151: Metavariable x = new Metavariable(new Name("x"), sort1);
152: Metavariable y = new Metavariable(new Name("y"), sort1);
153: Function c = new RigidFunction(new Name("c"), sort1,
154: new Sort[] {});
155: Function f = new RigidFunction(new Name("f"), sort1,
156: new Sort[] { sort1 });
157: Function p = new RigidFunction(new Name("p"), Sort.FORMULA,
158: new Sort[] { sort1 });
159:
160: Term terms[] = new Term[3];
161: terms[0] = tf.createFunctionTerm(x);
162: terms[1] = tf.createFunctionTerm(f, new Term[] { terms[0] });
163: terms[2] = tf.createFunctionTerm(p, new Term[] { terms[1] });
164: ConstrainedFormula cfma = new ConstrainedFormula(terms[2]);
165:
166: Term terms2[] = new Term[4];
167: terms2[0] = tf.createFunctionTerm(c);
168: terms2[1] = tf.createFunctionTerm(f, new Term[] { terms2[0] });
169: terms2[2] = tf.createFunctionTerm(f, new Term[] { terms2[1] });
170: terms2[3] = tf.createFunctionTerm(p, new Term[] { terms2[2] });
171: ConstrainedFormula cfma2 = new ConstrainedFormula(terms2[3]);
172:
173: Term terms3[] = new Term[4];
174: terms3[0] = tf.createFunctionTerm(y);
175: terms3[1] = tf.createFunctionTerm(f, new Term[] { terms3[0] });
176: terms3[2] = tf.createFunctionTerm(f, new Term[] { terms3[1] });
177: terms3[3] = tf.createFunctionTerm(p, new Term[] { terms3[2] });
178: ConstrainedFormula cfma3 = new ConstrainedFormula(terms3[3]);
179:
180: final PosInOccurrence topPIO = new PosInOccurrence(cfma,
181: PosInTerm.TOP_LEVEL, true);
182:
183: // Test without metavariables involved
184: PosInOccurrence pio = topPIO.down(0);
185: assertTrue(pio.subTerm() == terms[1]);
186: PosInOccurrence pio2 = pio.replaceConstrainedFormula(cfma);
187: assertEquals(pio, pio2);
188: pio = pio.replaceConstrainedFormula(cfma2);
189: assertTrue(pio.subTerm() == terms2[2]);
190:
191: // PIO pointing to metavariable, without term below
192: pio = topPIO.down(0).down(0);
193: assertTrue(pio.subTerm() == terms[0]);
194: pio2 = pio.replaceConstrainedFormula(cfma);
195: assertEquals(pio, pio2);
196: pio = pio.replaceConstrainedFormula(cfma2);
197: assertTrue(pio.subTerm() == terms2[1]);
198:
199: // PIO pointing to a term that is mounted below a metavariable
200: pio = topPIO.down(0).down(0)
201: .setTermBelowMetavariable(terms2[1]);
202: assertTrue(pio.subTerm() == terms2[1]);
203: pio2 = pio.replaceConstrainedFormula(cfma);
204: assertEquals(pio, pio2);
205: pio = pio.replaceConstrainedFormula(cfma2);
206: assertTrue(pio.subTerm() == terms2[1]);
207:
208: // PIO pointing to a position within a term that is mounted below a
209: // metavariable
210: pio = topPIO.down(0).down(0)
211: .setTermBelowMetavariable(terms2[1]).down(0);
212: assertTrue(pio.subTerm() == terms2[0]);
213: pio2 = pio.replaceConstrainedFormula(cfma);
214: assertEquals(pio, pio2);
215: pio = pio.replaceConstrainedFormula(cfma2);
216: assertTrue(pio.subTerm() == terms2[0]);
217:
218: // PIO pointing to a position (a metavariable) within a term that is
219: // mounted below a metavariable
220: pio = topPIO.down(0).down(0)
221: .setTermBelowMetavariable(terms3[1]).down(0);
222: assertTrue(pio.subTerm() == terms3[0]);
223: pio2 = pio.replaceConstrainedFormula(cfma);
224: assertEquals(pio, pio2);
225: pio = pio.replaceConstrainedFormula(cfma3);
226: assertTrue(pio.subTerm() == terms3[0]);
227:
228: // PIO pointing to a position within a term that is mounted below a
229: // metavariable
230: pio = topPIO.down(0).down(0)
231: .setTermBelowMetavariable(terms2[2]).down(0);
232: assertTrue(pio.subTerm() == terms2[1]);
233: pio2 = pio.replaceConstrainedFormula(cfma);
234: assertEquals(pio, pio2);
235: pio = pio.replaceConstrainedFormula(cfma2);
236: assertTrue(pio.subTerm() == terms2[0]);
237: }
238: }
|