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: /** tests the TacletIndex class.*/package de.uka.ilkd.key.proof;
012:
013: import junit.framework.TestCase;
014: import de.uka.ilkd.key.java.Services;
015: import de.uka.ilkd.key.logic.*;
016: import de.uka.ilkd.key.logic.op.Metavariable;
017: import de.uka.ilkd.key.rule.*;
018:
019: public class TestTermTacletAppIndex extends TestCase {
020:
021: Taclet ruleRewriteNonH1H2;
022: Taclet ruleNoFindNonH1H2H3;
023: Taclet ruleAntecH1;
024: Taclet ruleSucc;
025: Taclet ruleMisMatch;
026: Taclet notfreeconflict;
027: Taclet remove_f;
028: Taclet remove_ff;
029: Taclet remove_zero;
030: Metavariable x;
031:
032: public TestTermTacletAppIndex(String name) {
033: super (name);
034: }
035:
036: private Taclet taclet(String name) {
037: return TacletForTests.getTaclet(name).taclet();
038: }
039:
040: public void setUp() {
041: TacletForTests
042: .parse(System.getProperty("key.home")
043: + java.io.File.separator
044: + "system"
045: + java.io.File.separator
046: + "de/uka/ilkd/key/proof/ruleForTestTacletIndex.taclet");
047:
048: ruleRewriteNonH1H2 = taclet("rewrite_noninteractive_h1_h2");
049: ruleNoFindNonH1H2H3 = taclet("nofind_noninteractive_h1_h2_h3");
050: ruleAntecH1 = taclet("rule_antec_h1");
051: ruleSucc = taclet("rule_succ");
052: ruleMisMatch = taclet("antec_mismatch");
053: notfreeconflict = taclet("not_free_conflict");
054: remove_f = taclet("remove_f");
055: remove_ff = taclet("remove_ff");
056: remove_zero = taclet("remove_zero");
057:
058: x = new Metavariable(new Name("X"), TacletForTests
059: .sortLookup("nat"));
060: TacletForTests.getVariables().add(x);
061: }
062:
063: public void tearDown() {
064: x = null;
065: ruleRewriteNonH1H2 = null;
066: ruleNoFindNonH1H2H3 = null;
067: ruleAntecH1 = null;
068: ruleSucc = null;
069: ruleMisMatch = null;
070: notfreeconflict = null;
071: remove_f = null;
072: remove_ff = null;
073: remove_zero = null;
074: realCache = null;
075: noCache = null;
076: }
077:
078: private TermTacletAppIndexCacheSet realCache = new TermTacletAppIndexCacheSet();
079:
080: private TermTacletAppIndexCacheSet noCache = new TermTacletAppIndexCacheSet() {
081: public ITermTacletAppIndexCache getAntecCache() {
082: return getNoCache();
083: }
084:
085: public ITermTacletAppIndexCache getSuccCache() {
086: return getNoCache();
087: }
088: };
089:
090: public void testIndex0() {
091: doTestIndex0(noCache);
092: }
093:
094: public void testIndex0WithCache() {
095: for (int i = 0; i != 3; ++i)
096: doTestIndex0(realCache);
097: }
098:
099: private void doTestIndex0(TermTacletAppIndexCacheSet cache) {
100: Services serv = TacletForTests.services();
101:
102: TacletIndex ruleIdx = new TacletIndex();
103: ruleIdx.add(remove_f);
104: ruleIdx.add(remove_zero);
105:
106: Term term = TacletForTests.parseTerm("f(f(f(zero)))=one");
107: ConstrainedFormula cfma = new ConstrainedFormula(term);
108:
109: PosInOccurrence pio = new PosInOccurrence(cfma,
110: PosInTerm.TOP_LEVEL, false);
111:
112: TermTacletAppIndex termIdx = TermTacletAppIndex.create(pio,
113: serv, Constraint.BOTTOM, ruleIdx,
114: NullNewRuleListener.INSTANCE, TacletFilter.TRUE, cache);
115:
116: checkTermIndex(pio, termIdx);
117:
118: // this should not alter the index, as the formula actually
119: // did not change
120: termIdx = termIdx.update(pio.down(0), serv, Constraint.BOTTOM,
121: ruleIdx, NullNewRuleListener.INSTANCE, cache);
122:
123: checkTermIndex(pio, termIdx);
124:
125: // now a real change
126: Term term2 = TacletForTests.parseTerm("f(f(zero))=one");
127: ConstrainedFormula cfma2 = new ConstrainedFormula(term2);
128: PosInOccurrence pio2 = new PosInOccurrence(cfma2,
129: PosInTerm.TOP_LEVEL, false);
130:
131: termIdx = termIdx.update(pio2.down(0).down(0).down(0), serv,
132: Constraint.BOTTOM, ruleIdx,
133: NullNewRuleListener.INSTANCE, cache);
134: checkTermIndex2(pio2, termIdx);
135:
136: // add a new taclet to the index
137: ruleIdx.add(remove_ff);
138: SetRuleFilter filter = new SetRuleFilter();
139: filter.addRuleToSet(ruleIdx.lookup(remove_ff.name()).rule());
140: termIdx = termIdx.addTaclets(filter, pio2, serv,
141: Constraint.BOTTOM, ruleIdx,
142: NullNewRuleListener.INSTANCE);
143: checkTermIndex3(pio2, termIdx);
144: }
145:
146: public void testIndexWithMV() {
147: doTestIndexWithMV(noCache);
148: }
149:
150: public void testIndexWithMVWithCache() {
151: for (int i = 0; i != 3; ++i)
152: doTestIndexWithMV(realCache);
153: }
154:
155: private void doTestIndexWithMV(TermTacletAppIndexCacheSet cache) {
156: Services serv = TacletForTests.services();
157:
158: TacletIndex ruleIdx = new TacletIndex();
159: ruleIdx.add(remove_f);
160: ruleIdx.add(remove_zero);
161:
162: Term t1 = TacletForTests.parseTerm("f(zero)");
163: Term t2 = TacletForTests.parseTerm("X");
164:
165: Constraint c = Constraint.BOTTOM.unify(t1, t2, null);
166: assertTrue(c.isSatisfiable());
167: Term term = TacletForTests.parseTerm("f(f(X))=one");
168: ConstrainedFormula cfma = new ConstrainedFormula(term, c);
169: // System.out.println(cfma);
170:
171: PosInOccurrence pio = new PosInOccurrence(cfma,
172: PosInTerm.TOP_LEVEL, false);
173:
174: TermTacletAppIndex termIdx = TermTacletAppIndex.create(pio,
175: serv, Constraint.BOTTOM, ruleIdx,
176: NullNewRuleListener.INSTANCE, TacletFilter.TRUE, cache);
177:
178: checkTermIndex(pio, termIdx);
179:
180: // this should not alter the index, as the formula actually
181: // did not change
182: termIdx = termIdx.update(pio.down(0), serv, Constraint.BOTTOM,
183: ruleIdx, NullNewRuleListener.INSTANCE, cache);
184:
185: checkTermIndex(pio, termIdx);
186:
187: // now a real change
188: Term term2 = TacletForTests.parseTerm("f(f(zero))=one");
189: ConstrainedFormula cfma2 = new ConstrainedFormula(term2, c);
190: PosInOccurrence pio2 = new PosInOccurrence(cfma2,
191: PosInTerm.TOP_LEVEL, false);
192:
193: termIdx = termIdx.update(pio2.down(0).down(0).down(0), serv,
194: Constraint.BOTTOM, ruleIdx,
195: NullNewRuleListener.INSTANCE, cache);
196: checkTermIndex2(pio2, termIdx);
197:
198: // add a new taclet to the index
199: ruleIdx.add(remove_ff);
200: SetRuleFilter filter = new SetRuleFilter();
201: filter.addRuleToSet(ruleIdx.lookup(remove_ff.name()).rule());
202: termIdx = termIdx.addTaclets(filter, pio2, serv,
203: Constraint.BOTTOM, ruleIdx,
204: NullNewRuleListener.INSTANCE);
205: checkTermIndex3(pio2, termIdx);
206: }
207:
208: private void checkAtPos(PosInOccurrence pio,
209: TermTacletAppIndex termIdx, ListOfTaclet list) {
210: checkTacletList(termIdx.getTacletAppAt(pio, TacletFilter.TRUE),
211: list);
212: }
213:
214: private PosInOccurrence down(PosInOccurrence pio, int i) {
215: return handleDisplayConstraint(pio.down(i), pio
216: .constrainedFormula().constraint());
217: }
218:
219: private void checkTermIndex(PosInOccurrence pio,
220: TermTacletAppIndex termIdx) {
221: ListOfTaclet listA = SLListOfTaclet.EMPTY_LIST;
222: ListOfTaclet listB = listA.prepend(remove_f);
223: ListOfTaclet listC = listA.prepend(remove_zero);
224:
225: checkAtPos(pio, termIdx, listA);
226: checkAtPos(down(pio, 0), termIdx, listB);
227: checkAtPos(down(down(pio, 0), 0), termIdx, listB);
228: checkAtPos(down(down(down(pio, 0), 0), 0), termIdx, listB);
229: checkAtPos(down(down(down(down(pio, 0), 0), 0), 0), termIdx,
230: listC);
231: checkAtPos(down(pio, 1), termIdx, listA);
232: }
233:
234: private void checkTermIndex2(PosInOccurrence pio,
235: TermTacletAppIndex termIdx) {
236: ListOfTaclet listA = SLListOfTaclet.EMPTY_LIST;
237: ListOfTaclet listB = listA.prepend(remove_f);
238: ListOfTaclet listC = listA.prepend(remove_zero);
239:
240: checkAtPos(pio, termIdx, listA);
241: checkAtPos(down(pio, 0), termIdx, listB);
242: checkAtPos(down(down(pio, 0), 0), termIdx, listB);
243: checkAtPos(down(down(down(pio, 0), 0), 0), termIdx, listC);
244: checkAtPos(down(pio, 1), termIdx, listA);
245: }
246:
247: private void checkTermIndex3(PosInOccurrence pio,
248: TermTacletAppIndex termIdx) {
249: ListOfTaclet listA = SLListOfTaclet.EMPTY_LIST;
250: ListOfTaclet listB = listA.prepend(remove_f);
251: ListOfTaclet listC = listA.prepend(remove_zero);
252: ListOfTaclet listD = listB.prepend(remove_ff);
253:
254: checkAtPos(pio, termIdx, listA);
255: checkAtPos(down(pio, 0), termIdx, listD);
256: checkAtPos(down(down(pio, 0), 0), termIdx, listB);
257: checkAtPos(down(down(down(pio, 0), 0), 0), termIdx, listC);
258: checkAtPos(down(pio, 1), termIdx, listA);
259: }
260:
261: private void checkTacletList(ListOfNoPosTacletApp p_toCheck,
262: ListOfTaclet p_template) {
263: assertTrue(p_toCheck.size() == p_template.size());
264: IteratorOfNoPosTacletApp it = p_toCheck.iterator();
265: while (it.hasNext())
266: assertTrue(p_template.contains(it.next().taclet()));
267: }
268:
269: /**
270: * Check whether the given term is a metavariable, and replace it
271: * with a concrete term provided that such a term is determined by
272: * the user constraint
273: * @return A <code>PosInOccurrence</code> object in which
274: * eventually the metavariable has been replaced with a term as
275: * given by the user constraint. In any case the object points to
276: * the same position of a term as the <code>pos</code> parameter
277: */
278: private static PosInOccurrence handleDisplayConstraint(
279: PosInOccurrence pos, Constraint displayConstraint) {
280:
281: Term term = pos.subTerm();
282:
283: if (term.op() instanceof Metavariable) {
284: if (pos.termBelowMetavariable() == null) {
285: Term metaTerm = displayConstraint
286: .getInstantiation((Metavariable) term.op());
287: if (metaTerm.op() != term.op())
288: return pos.setTermBelowMetavariable(metaTerm);
289: }
290: }
291:
292: return pos;
293: }
294:
295: }
|