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.rule.*;
017:
018: public class TestTacletIndex extends TestCase {
019:
020: Taclet ruleRewriteNonH1H2;
021: Taclet ruleNoFindNonH1H2H3;
022: Taclet ruleAntecH1;
023: Taclet ruleSucc;
024: Taclet ruleMisMatch;
025: Taclet notfreeconflict;
026:
027: RuleSet h1;
028: RuleSet h2;
029: RuleSet h3;
030:
031: TacletIndex variante_one;
032:
033: public TestTacletIndex(String name) {
034: super (name);
035: }
036:
037: private Taclet taclet(String name) {
038: return TacletForTests.getTaclet(name).taclet();
039: }
040:
041: public void setUp() {
042: TacletForTests
043: .parse(System.getProperty("key.home")
044: + java.io.File.separator
045: + "system"
046: + java.io.File.separator
047: + "de/uka/ilkd/key/proof/ruleForTestTacletIndex.taclet");
048:
049: h1 = (RuleSet) TacletForTests.getHeuristics().lookup(
050: new Name("h1"));
051: h2 = (RuleSet) TacletForTests.getHeuristics().lookup(
052: new Name("h2"));
053: h3 = (RuleSet) TacletForTests.getHeuristics().lookup(
054: new Name("h3"));
055:
056: ruleRewriteNonH1H2 = taclet("rewrite_noninteractive_h1_h2");
057: ruleNoFindNonH1H2H3 = taclet("nofind_noninteractive_h1_h2_h3");
058: ruleAntecH1 = taclet("rule_antec_h1");
059: ruleSucc = taclet("rule_succ");
060: ruleMisMatch = taclet("antec_mismatch");
061: notfreeconflict = taclet("not_free_conflict");
062:
063: variante_one = new TacletIndex();
064: variante_one.add(ruleRewriteNonH1H2);
065: variante_one.add(ruleNoFindNonH1H2H3);
066: variante_one.add(ruleAntecH1);
067: variante_one.add(ruleSucc);
068:
069: }
070:
071: public void tearDown() {
072: ruleRewriteNonH1H2 = null;
073: ruleNoFindNonH1H2H3 = null;
074: ruleAntecH1 = null;
075: ruleSucc = null;
076: ruleMisMatch = null;
077: notfreeconflict = null;
078:
079: h1 = null;
080: h2 = null;
081: h3 = null;
082:
083: variante_one = null;
084: }
085:
086: private boolean isRuleIn(ListOfNoPosTacletApp l, Taclet rule) {
087: IteratorOfNoPosTacletApp it = l.iterator();
088: while (it.hasNext()) {
089: if (it.next().taclet() == rule)
090: return true;
091: }
092: return false;
093: }
094:
095: private boolean isRuleIn(ListOfTacletApp l, Taclet rule) {
096: IteratorOfTacletApp it = l.iterator();
097: while (it.hasNext()) {
098: if (it.next().taclet() == rule)
099: return true;
100: }
101: return false;
102: }
103:
104: /**
105: * test disabled. Since 0.632 "noninteractive" is disabled
106: */
107: public void disabled_testNonInteractiveIsShownOnlyIfHeuristicIsMissed() {
108: Term term_p1 = TacletForTests.parseTerm("p(one, zero)");
109: ListOfRuleSet listofHeuristic = SLListOfRuleSet.EMPTY_LIST;
110: listofHeuristic = listofHeuristic.prepend(h3);
111: PosInOccurrence pos = new PosInOccurrence(
112: new ConstrainedFormula(term_p1, Constraint.BOTTOM),
113: PosInTerm.TOP_LEVEL, true);
114: assertTrue(
115: "Noninteractive antecrule is not in list, but none of its"
116: + "heuristics is active.", isRuleIn(
117: variante_one.getAntecedentTaclet(pos,
118: new IHTacletFilter(true,
119: listofHeuristic), null,
120: Constraint.BOTTOM), ruleRewriteNonH1H2));
121:
122: assertTrue(
123: "Noninteractive antecrule is in list, but one of its "
124: + "heuristics is active.", !isRuleIn(
125: variante_one.getAntecedentTaclet(pos,
126: new IHTacletFilter(true,
127: listofHeuristic.prepend(h1)),
128: null, Constraint.BOTTOM),
129: ruleRewriteNonH1H2));
130:
131: assertTrue(
132: "Noninteractive nofindrule is not in list, but none of its "
133: + "heuristics is active.", isRuleIn(
134: variante_one.getNoFindTaclet(
135: new IHTacletFilter(true,
136: SLListOfRuleSet.EMPTY_LIST),
137: null, Constraint.BOTTOM),
138: ruleNoFindNonH1H2H3));
139:
140: assertTrue(
141: "Noninteractive nofindrule is in list, but one of its "
142: + "heuristics is active.",
143: !isRuleIn(variante_one.getNoFindTaclet(
144: new IHTacletFilter(true, listofHeuristic),
145: null, Constraint.BOTTOM), ruleNoFindNonH1H2H3));
146:
147: }
148:
149: public void testShownIfHeuristicFits() {
150: Services services = new Services();
151: ListOfRuleSet listofHeuristic = SLListOfRuleSet.EMPTY_LIST;
152: listofHeuristic = listofHeuristic.prepend(h3).prepend(h2);
153:
154: Term term_p1 = TacletForTests.parseTerm("p(one, zero)");
155:
156: ConstrainedFormula cfma = new ConstrainedFormula(term_p1,
157: Constraint.BOTTOM);
158:
159: PosInOccurrence posSucc = new PosInOccurrence(cfma,
160: PosInTerm.TOP_LEVEL, false);
161:
162: assertTrue("ruleSucc has no heuristics, but is"
163: + " not in succ list.", isRuleIn(variante_one
164: .getSuccedentTaclet(posSucc, new IHTacletFilter(true,
165: listofHeuristic), services, Constraint.BOTTOM),
166: ruleSucc));
167:
168: assertTrue("ruleSucc has no heuristics, but is"
169: + " in rewrite list.", !isRuleIn(variante_one
170: .getRewriteTaclet(posSucc, Constraint.BOTTOM,
171: new IHTacletFilter(true, listofHeuristic),
172: services, Constraint.BOTTOM), ruleSucc));
173:
174: assertTrue("ruleSucc has no heuristics, but is"
175: + " in heuristic succ list.", !isRuleIn(variante_one
176: .getSuccedentTaclet(posSucc, new IHTacletFilter(false,
177: listofHeuristic), services, Constraint.BOTTOM),
178: ruleSucc));
179:
180: assertTrue("ruleSucc has no heuristics, but is"
181: + " in heuristic of nofind list.", !isRuleIn(
182: variante_one.getNoFindTaclet(new IHTacletFilter(false,
183: listofHeuristic), services, Constraint.BOTTOM),
184: ruleSucc));
185: }
186:
187: public void testNoMatchingFindRule() {
188: Services services = new Services();
189: ListOfRuleSet listofHeuristic = SLListOfRuleSet.EMPTY_LIST;
190:
191: Term term_p2 = TacletForTests.parseTerm(
192: "\\forall nat z; p(z, one)").sub(0);
193:
194: PosInOccurrence posAntec = new PosInOccurrence(
195: new ConstrainedFormula(term_p2, Constraint.BOTTOM),
196: PosInTerm.TOP_LEVEL, true);
197: PosInOccurrence posSucc = new PosInOccurrence(
198: new ConstrainedFormula(term_p2, Constraint.BOTTOM),
199: PosInTerm.TOP_LEVEL, true);
200:
201: assertTrue("rule matched, but no match possible", !isRuleIn(
202: variante_one.getAntecedentTaclet(posAntec,
203: new IHTacletFilter(true, listofHeuristic),
204: services, Constraint.BOTTOM),
205: ruleRewriteNonH1H2));
206:
207: listofHeuristic = listofHeuristic.prepend(h3).prepend(h2)
208: .prepend(h1);
209:
210: assertTrue("ruleSucc matched but matching not possible",
211: !isRuleIn(variante_one.getSuccedentTaclet(posSucc,
212: new IHTacletFilter(true, listofHeuristic),
213: services, Constraint.BOTTOM), ruleSucc));
214: }
215:
216: public void testMatchConflictOccurs() {
217: Services services = new Services();
218: TacletIndex ruleIdx = new TacletIndex();
219: ruleIdx.add(ruleRewriteNonH1H2);
220: ruleIdx.add(ruleNoFindNonH1H2H3);
221: ruleIdx.add(ruleAntecH1);
222: ruleIdx.add(ruleSucc);
223: ruleIdx.add(ruleMisMatch);
224:
225: Term term_p4 = TacletForTests.parseTerm("p(zero, one)");
226:
227: ListOfRuleSet listofHeuristic = SLListOfRuleSet.EMPTY_LIST;
228: PosInOccurrence posAntec = new PosInOccurrence(
229: new ConstrainedFormula(term_p4, Constraint.BOTTOM),
230: PosInTerm.TOP_LEVEL, true);
231:
232: assertTrue("rule matched, but no match possible", !isRuleIn(
233: ruleIdx.getAntecedentTaclet(posAntec,
234: new IHTacletFilter(true, listofHeuristic),
235: services, Constraint.BOTTOM), ruleMisMatch));
236:
237: }
238:
239: public void testNotFreeInYConflict() {
240: TacletIndex ruleIdx = new TacletIndex();
241: ruleIdx.add(notfreeconflict);
242:
243: Term term_p5 = TacletForTests
244: .parseTerm("\\forall nat z; p(f(z), z)");
245: ConstrainedFormula cfma_p5 = new ConstrainedFormula(term_p5);
246: Sequent seq_p5 = Sequent
247: .createAnteSequent(Semisequent.EMPTY_SEMISEQUENT
248: .insertFirst(cfma_p5).semisequent());
249: PosInOccurrence pio_p5 = new PosInOccurrence(cfma_p5,
250: PosInTerm.TOP_LEVEL, true);
251: RuleAppIndex appIdx = createGoalFor(seq_p5, ruleIdx);
252:
253: assertTrue("No rule should match", !isRuleIn(appIdx
254: .getTacletAppAt(TacletFilter.TRUE, pio_p5, null,
255: Constraint.BOTTOM), notfreeconflict));
256:
257: Term term_p6 = TacletForTests
258: .parseTerm("\\forall nat z; p(zero, z)");
259:
260: ConstrainedFormula cfma_p6 = new ConstrainedFormula(term_p6);
261: Sequent seq_p6 = Sequent
262: .createAnteSequent(Semisequent.EMPTY_SEMISEQUENT
263: .insertFirst(cfma_p6).semisequent());
264: PosInOccurrence pio_p6 = new PosInOccurrence(cfma_p6,
265: PosInTerm.TOP_LEVEL, true);
266: appIdx = createGoalFor(seq_p6, ruleIdx);
267:
268: assertTrue("One rule should match", isRuleIn(appIdx
269: .getTacletAppAt(TacletFilter.TRUE, pio_p6, null,
270: Constraint.BOTTOM), notfreeconflict));
271:
272: }
273:
274: private RuleAppIndex createGoalFor(Sequent seq_p5,
275: TacletIndex ruleIdx) {
276: final Node node_p5 = new Node(new Proof(new Services()), seq_p5);
277: final BuiltInRuleAppIndex builtinIdx = new BuiltInRuleAppIndex(
278: new BuiltInRuleIndex());
279: final Goal goal_p5 = new Goal(node_p5, new RuleAppIndex(
280: ruleIdx, builtinIdx));
281: return goal_p5.ruleAppIndex();
282: }
283:
284: }
|