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.gui;
012:
013: import java.io.StringReader;
014:
015: import de.uka.ilkd.key.logic.*;
016: import de.uka.ilkd.key.logic.op.*;
017: import de.uka.ilkd.key.logic.sort.PrimitiveSort;
018: import de.uka.ilkd.key.logic.sort.Sort;
019: import de.uka.ilkd.key.parser.KeYLexer;
020: import de.uka.ilkd.key.parser.KeYParser;
021: import de.uka.ilkd.key.parser.ParserMode;
022: import de.uka.ilkd.key.proof.TacletIndex;
023: import de.uka.ilkd.key.rule.*;
024:
025: public class TestTacletPopup {
026:
027: static AntecTaclet impleft;
028: static SuccTaclet impright;
029: static AntecTaclet notleft;
030: static SuccTaclet notright;
031: static SuccTaclet close;
032: static SuccTaclet allright;
033: static AntecTaclet allleft;
034: static AntecTaclet remove_or_left;
035: static SuccTaclet remove_or_right;
036: static AntecTaclet remove_and_left;
037: static SuccTaclet remove_and_right;
038: static RewriteTaclet contradiction;
039: static NoFindTaclet cut;
040: static RewriteTaclet predsuccelim;
041: static RewriteTaclet pluszeroelim;
042: static RewriteTaclet zeropluselim;
043: static RewriteTaclet succelim;
044: static RewriteTaclet switchsecondsucc;
045: static RewriteTaclet switchfirstsucc;
046: static SuccTaclet closewitheq;
047:
048: static Sequent seq_test1;
049: static Sequent seq_test2;
050: static Sequent seq_test3;
051: static Sequent seq_testAll;
052: static Sequent seq_testNat;
053:
054: static SchemaVariable b;
055: static SchemaVariable x;
056: static SchemaVariable x0;
057: static SchemaVariable t0;
058: static LogicVariable z;
059:
060: static Sort nat = new PrimitiveSort(new Name("Nat"));
061:
062: static TermFactory tf = TermFactory.DEFAULT;
063:
064: public static Namespace var_ns = new Namespace();
065: public static Namespace func_ns = new Namespace();
066: public static Namespace sort_ns = new Namespace();
067:
068: private TestTacletPopup() {
069: }
070:
071: static {
072: sort_ns.add(Sort.FORMULA);
073: sort_ns.add(nat);
074:
075: // imp-left rule
076: // find(b->b0 =>) replacewith(b0 =>) replacewith(=> b)
077: AntecTacletBuilder impleftbuilder = new AntecTacletBuilder();
078: b = SchemaVariableFactory.createFormulaSV(new Name("b"), false);
079: SchemaVariable b0 = SchemaVariableFactory.createFormulaSV(
080: new Name("b0"), false);
081: Term t_b = tf.createFunctionTerm((SortedSchemaVariable) b,
082: new Term[0]);
083: Term t_b0 = tf.createFunctionTerm((SortedSchemaVariable) b0,
084: new Term[0]);
085: Term t_bimpb0 = tf.createJunctorTerm(Op.IMP, new Term[] { t_b,
086: t_b0 });
087: Term t_bandb0 = tf.createJunctorTerm(Op.AND, t_b, t_b0);
088: Term t_borb0 = tf.createJunctorTerm(Op.OR, t_b, t_b0);
089:
090: impleftbuilder.setFind(t_bimpb0);
091: impleftbuilder.setName(new Name("imp-left"));
092: Sequent ante = Sequent.createSequent(
093: Semisequent.EMPTY_SEMISEQUENT
094: .insert(
095: 0,
096: new ConstrainedFormula(t_b0,
097: Constraint.BOTTOM))
098: .semisequent(), Semisequent.EMPTY_SEMISEQUENT);
099: impleftbuilder
100: .addTacletGoalTemplate(new AntecSuccTacletGoalTemplate(
101: Sequent.EMPTY_SEQUENT,
102: SLListOfTaclet.EMPTY_LIST, ante));
103: Sequent succ = Sequent.createSequent(
104: Semisequent.EMPTY_SEMISEQUENT,
105: Semisequent.EMPTY_SEMISEQUENT.insert(0,
106: new ConstrainedFormula(t_b, Constraint.BOTTOM))
107: .semisequent());
108: impleftbuilder
109: .addTacletGoalTemplate(new AntecSuccTacletGoalTemplate(
110: Sequent.EMPTY_SEQUENT,
111: SLListOfTaclet.EMPTY_LIST, succ));
112: impleft = impleftbuilder.getAntecTaclet();
113:
114: // imp-right rule
115: // find(=> b->b0) replacewith(b => b0)
116: SuccTacletBuilder imprightbuilder = new SuccTacletBuilder();
117: imprightbuilder.setFind(t_bimpb0);
118: Sequent seq = Sequent.createSequent(
119: Semisequent.EMPTY_SEMISEQUENT.insert(0,
120: new ConstrainedFormula(t_b, Constraint.BOTTOM))
121: .semisequent(), Semisequent.EMPTY_SEMISEQUENT
122: .insert(
123: 0,
124: new ConstrainedFormula(t_b0,
125: Constraint.BOTTOM))
126: .semisequent());
127: imprightbuilder
128: .addTacletGoalTemplate(new AntecSuccTacletGoalTemplate(
129: Sequent.EMPTY_SEQUENT,
130: SLListOfTaclet.EMPTY_LIST, seq));
131: imprightbuilder.setName(new Name("imp-right"));
132: impright = imprightbuilder.getSuccTaclet();
133:
134: // not-left rule
135: // find(not b=>) replacewith(=>b)
136: Term t_notb = tf.createJunctorTerm(Op.NOT, new Term[] { t_b });
137: AntecTacletBuilder notleftbuilder = new AntecTacletBuilder();
138: notleftbuilder.setFind(t_notb);
139: seq = Sequent.createSequent(Semisequent.EMPTY_SEMISEQUENT,
140: Semisequent.EMPTY_SEMISEQUENT.insert(0,
141: new ConstrainedFormula(t_b, Constraint.BOTTOM))
142: .semisequent());
143: notleftbuilder
144: .addTacletGoalTemplate(new AntecSuccTacletGoalTemplate(
145: Sequent.EMPTY_SEQUENT,
146: SLListOfTaclet.EMPTY_LIST, seq));
147: notleftbuilder.setName(new Name("not-left"));
148: notleft = notleftbuilder.getAntecTaclet();
149:
150: // not-right rule
151: // find(=>not b) replacewith(b=>)
152: SuccTacletBuilder notrightbuilder = new SuccTacletBuilder();
153: notrightbuilder.setFind(t_notb);
154: seq = Sequent.createSequent(Semisequent.EMPTY_SEMISEQUENT
155: .insert(0,
156: new ConstrainedFormula(t_b, Constraint.BOTTOM))
157: .semisequent(), Semisequent.EMPTY_SEMISEQUENT);
158: notrightbuilder
159: .addTacletGoalTemplate(new AntecSuccTacletGoalTemplate(
160: Sequent.EMPTY_SEQUENT,
161: SLListOfTaclet.EMPTY_LIST, seq));
162: notrightbuilder.setName(new Name("not-right"));
163: notright = notrightbuilder.getSuccTaclet();
164:
165: // cut rule
166: // add(b=>) add(=>b)
167: NoFindTacletBuilder nfbuilder = new NoFindTacletBuilder();
168: seq = Sequent.createSequent(Semisequent.EMPTY_SEMISEQUENT
169: .insert(0,
170: new ConstrainedFormula(t_b, Constraint.BOTTOM))
171: .semisequent(), Semisequent.EMPTY_SEMISEQUENT);
172: nfbuilder.addTacletGoalTemplate(new TacletGoalTemplate(seq,
173: SLListOfTaclet.EMPTY_LIST));
174:
175: seq = Sequent.createSequent(Semisequent.EMPTY_SEMISEQUENT,
176: Semisequent.EMPTY_SEMISEQUENT.insert(0,
177: new ConstrainedFormula(t_b, Constraint.BOTTOM))
178: .semisequent());
179:
180: nfbuilder.addTacletGoalTemplate(new TacletGoalTemplate(seq,
181: SLListOfTaclet.EMPTY_LIST));
182: nfbuilder.setName(new Name("cut rule"));
183:
184: cut = nfbuilder.getNoFindTaclet();
185:
186: ListOfTaclet emptyTacletList = SLListOfTaclet.EMPTY_LIST;
187:
188: // close rule
189: // if (b=>) find(=>b)
190: SuccTacletBuilder closebuilder = new SuccTacletBuilder();
191: closebuilder.setFind(t_b);
192: seq = Sequent.createSequent(Semisequent.EMPTY_SEMISEQUENT
193: .insert(0,
194: new ConstrainedFormula(t_b, Constraint.BOTTOM))
195: .semisequent(), Semisequent.EMPTY_SEMISEQUENT);
196: closebuilder.setIfSequent(seq);
197: closebuilder.setName(new Name("close"));
198: close = closebuilder.getSuccTaclet();
199:
200: // contradiction rule
201: // find(b->b0) replacewith(-b0 -> -b)
202: Term t_notb0 = tf
203: .createJunctorTerm(Op.NOT, new Term[] { t_b0 });
204: Term t_notb0impnotb = tf.createJunctorTerm(Op.IMP, new Term[] {
205: t_notb0, t_notb });
206:
207: RewriteTacletBuilder rwbuilder = new RewriteTacletBuilder();
208: rwbuilder.setFind(t_bimpb0);
209: seq = Sequent.createSequent(Semisequent.EMPTY_SEMISEQUENT
210: .insert(0,
211: new ConstrainedFormula(t_b, Constraint.BOTTOM))
212: .semisequent(), Semisequent.EMPTY_SEMISEQUENT);
213: rwbuilder
214: .addTacletGoalTemplate(new RewriteTacletGoalTemplate(
215: Sequent.EMPTY_SEQUENT, emptyTacletList,
216: t_notb0impnotb));
217: rwbuilder.setName(new Name("contradiction rule"));
218: contradiction = rwbuilder.getRewriteTaclet();
219:
220: // all-right
221: // find (=>Vx:b) add(=>b[x/t0])
222: SuccTacletBuilder allrightbuilder = new SuccTacletBuilder();
223: x = SchemaVariableFactory.createVariableSV(new Name("x"), nat,
224: false);
225: t0 = SchemaVariableFactory.createTermSV(new Name("t0"), nat,
226: false);
227: Term t_t0 = tf.createFunctionTerm((SortedSchemaVariable) t0,
228: new Term[0]);
229: Term t_allxb = tf
230: .createQuantifierTerm(
231: Op.ALL,
232: new SortedSchemaVariable[] { (SortedSchemaVariable) x },
233: t_b);
234: Term t_subxt0b = tf.createSubstitutionTerm(Op.SUBST,
235: (SortedSchemaVariable) x, t_t0, t_b);
236: allrightbuilder.setFind(t_allxb);
237: seq = Sequent.createSequent(Semisequent.EMPTY_SEMISEQUENT,
238: Semisequent.EMPTY_SEMISEQUENT.insert(
239: 0,
240: new ConstrainedFormula(t_subxt0b,
241: Constraint.BOTTOM)).semisequent());
242:
243: allrightbuilder
244: .addTacletGoalTemplate(new AntecSuccTacletGoalTemplate(
245: seq, SLListOfTaclet.EMPTY_LIST,
246: Sequent.EMPTY_SEQUENT));
247: allrightbuilder.setName(new Name("all-right"));
248: allright = allrightbuilder.getSuccTaclet();
249:
250: // all-left
251: // find (Vx:b=>) add (b[x/t0]=>)
252: AntecTacletBuilder allleftbuilder = new AntecTacletBuilder();
253: allleftbuilder.setFind(t_allxb);
254: seq = Sequent.createSequent(Semisequent.EMPTY_SEMISEQUENT
255: .insert(
256: 0,
257: new ConstrainedFormula(t_subxt0b,
258: Constraint.BOTTOM)).semisequent(),
259: Semisequent.EMPTY_SEMISEQUENT);
260:
261: allleftbuilder
262: .addTacletGoalTemplate(new AntecSuccTacletGoalTemplate(
263: seq, SLListOfTaclet.EMPTY_LIST,
264: Sequent.EMPTY_SEQUENT));
265: allleftbuilder.setName(new Name("all-left"));
266: allleft = allleftbuilder.getAntecTaclet();
267:
268: // remove-and-left
269: // find (b & c=>) replacewith (b, c=>)
270: AntecTacletBuilder remove_and_leftbuilder = new AntecTacletBuilder();
271:
272: remove_and_leftbuilder.setFind(t_bandb0);
273: seq = Sequent.createSequent(
274: Semisequent.EMPTY_SEMISEQUENT
275: .insert(
276: 0,
277: new ConstrainedFormula(t_b0,
278: Constraint.BOTTOM))
279: .semisequent().insert(
280: 0,
281: new ConstrainedFormula(t_b,
282: Constraint.BOTTOM))
283: .semisequent(), Semisequent.EMPTY_SEMISEQUENT);
284:
285: remove_and_leftbuilder
286: .addTacletGoalTemplate(new AntecSuccTacletGoalTemplate(
287: Sequent.EMPTY_SEQUENT,
288: SLListOfTaclet.EMPTY_LIST, seq));
289: remove_and_leftbuilder.setName(new Name("remove-and-left"));
290: remove_and_left = remove_and_leftbuilder.getAntecTaclet();
291:
292: // remove-or-left
293: // find (b | c=>) replacewith (b =>); replacewith(c => )
294: AntecTacletBuilder remove_or_leftbuilder = new AntecTacletBuilder();
295: remove_or_leftbuilder.setFind(t_borb0);
296: seq = Sequent.createSequent(Semisequent.EMPTY_SEMISEQUENT
297: .insert(0,
298: new ConstrainedFormula(t_b, Constraint.BOTTOM))
299: .semisequent(), Semisequent.EMPTY_SEMISEQUENT);
300:
301: remove_or_leftbuilder
302: .addTacletGoalTemplate(new AntecSuccTacletGoalTemplate(
303: Sequent.EMPTY_SEQUENT,
304: SLListOfTaclet.EMPTY_LIST, seq));
305:
306: seq = Sequent.createSequent(
307: Semisequent.EMPTY_SEMISEQUENT
308: .insert(
309: 0,
310: new ConstrainedFormula(t_b0,
311: Constraint.BOTTOM))
312: .semisequent(), Semisequent.EMPTY_SEMISEQUENT);
313:
314: remove_or_leftbuilder
315: .addTacletGoalTemplate(new AntecSuccTacletGoalTemplate(
316: Sequent.EMPTY_SEQUENT,
317: SLListOfTaclet.EMPTY_LIST, seq));
318:
319: remove_or_leftbuilder.setName(new Name("remove-or-left"));
320: remove_or_left = remove_or_leftbuilder.getAntecTaclet();
321:
322: // remove-and-right
323: // find (=> b & c) replacewith (=> b); replacewith(=>c)
324: SuccTacletBuilder remove_and_rightbuilder = new SuccTacletBuilder();
325: remove_and_rightbuilder.setFind(t_bandb0);
326: seq = Sequent.createSequent(Semisequent.EMPTY_SEMISEQUENT,
327: Semisequent.EMPTY_SEMISEQUENT.insert(0,
328: new ConstrainedFormula(t_b, Constraint.BOTTOM))
329: .semisequent());
330:
331: remove_and_rightbuilder
332: .addTacletGoalTemplate(new AntecSuccTacletGoalTemplate(
333: Sequent.EMPTY_SEQUENT,
334: SLListOfTaclet.EMPTY_LIST, seq));
335:
336: seq = Sequent.createSequent(Semisequent.EMPTY_SEMISEQUENT,
337: Semisequent.EMPTY_SEMISEQUENT
338: .insert(
339: 0,
340: new ConstrainedFormula(t_b0,
341: Constraint.BOTTOM))
342: .semisequent());
343:
344: remove_and_rightbuilder
345: .addTacletGoalTemplate(new AntecSuccTacletGoalTemplate(
346: Sequent.EMPTY_SEQUENT,
347: SLListOfTaclet.EMPTY_LIST, seq));
348:
349: remove_and_rightbuilder.setName(new Name("remove-and-right"));
350: remove_and_right = remove_and_rightbuilder.getSuccTaclet();
351:
352: // remove-or-right
353: // find (=> b or c) replacewith (=>b, c)
354: SuccTacletBuilder remove_or_rightbuilder = new SuccTacletBuilder();
355: remove_or_rightbuilder.setFind(t_borb0);
356: seq = Sequent.createSequent(Semisequent.EMPTY_SEMISEQUENT,
357: Semisequent.EMPTY_SEMISEQUENT
358: .insert(
359: 0,
360: new ConstrainedFormula(t_b0,
361: Constraint.BOTTOM))
362: .semisequent().insert(
363: 0,
364: new ConstrainedFormula(t_b,
365: Constraint.BOTTOM))
366: .semisequent());
367:
368: remove_or_rightbuilder
369: .addTacletGoalTemplate(new AntecSuccTacletGoalTemplate(
370: Sequent.EMPTY_SEQUENT,
371: SLListOfTaclet.EMPTY_LIST, seq));
372: remove_or_rightbuilder.setName(new Name("remove-or-right"));
373: remove_or_right = remove_or_rightbuilder.getSuccTaclet();
374:
375: //decls for nat
376: Function func_0 = new RigidFunction(new Name("zero"), nat,
377: new Sort[] {});
378: func_ns.add(func_0);
379: Function func_plus = new RigidFunction(new Name("plus"), nat,
380: new Sort[] { nat, nat });
381: func_ns.add(func_plus);
382: Function func_min1 = new RigidFunction(new Name("pred"), nat,
383: new Sort[] { nat });
384: func_ns.add(func_min1);
385: Function func_plus1 = new RigidFunction(new Name("succ"), nat,
386: new Sort[] { nat });
387: func_ns.add(func_plus1);
388: SchemaVariable var_rn = SchemaVariableFactory.createTermSV(
389: new Name("rn"), nat, false);
390: SchemaVariable var_rm = SchemaVariableFactory.createTermSV(
391: new Name("rm"), nat, false);
392:
393: Term t_rn = tf.createFunctionTerm(
394: (SortedSchemaVariable) var_rn, new Term[] {});
395: Term t_rm = tf.createFunctionTerm(
396: (SortedSchemaVariable) var_rm, new Term[] {});
397: Term t_0 = tf.createFunctionTerm(func_0, new Term[] {});
398: Term t_rnminus1 = tf.createFunctionTerm(func_min1,
399: new Term[] { t_rn });
400: Term t_rnminus1plus1 = tf.createFunctionTerm(func_plus1,
401: new Term[] { t_rnminus1 });
402: // Term t_0minus1=tf.createFunctionTerm(func_min1,
403: // new Term[]{t_0});
404: Term t_0plus1 = tf.createFunctionTerm(func_plus1,
405: new Term[] { t_0 });
406:
407: // help rule r1: find(rn) replacewith(0) replacewith(0
408: RewriteTacletBuilder rwb1 = new RewriteTacletBuilder();
409: rwb1.setName(new Name("r1"));
410: rwb1.setFind(t_rn);
411: rwb1.addTacletGoalTemplate(new RewriteTacletGoalTemplate(
412: Sequent.EMPTY_SEQUENT, SLListOfTaclet.EMPTY_LIST, t_0));
413:
414: //pred-succ-elim-rule
415: // find(rn -1 +1) replacewith(rn) replacewith(0 +1) addrule(r1)
416: rwbuilder = new RewriteTacletBuilder();
417: rwbuilder.setFind(t_rnminus1plus1);
418: rwbuilder
419: .addTacletGoalTemplate(new RewriteTacletGoalTemplate(
420: Sequent.EMPTY_SEQUENT,
421: SLListOfTaclet.EMPTY_LIST, t_rn));
422: rwbuilder.addTacletGoalTemplate(new RewriteTacletGoalTemplate(
423: Sequent.EMPTY_SEQUENT, emptyTacletList.prepend(rwb1
424: .getTaclet()), t_0plus1));
425: rwbuilder.setName(new Name("pred-succ-elim"));
426: pluszeroelim = rwbuilder.getRewriteTaclet();
427:
428: //plus-zero-elim
429: // find(rn + 0) replacewith(rn)
430: rwbuilder = new RewriteTacletBuilder();
431: rwbuilder.setFind(tf.createFunctionTerm(func_plus, new Term[] {
432: t_rn, t_0 }));
433: rwbuilder
434: .addTacletGoalTemplate(new RewriteTacletGoalTemplate(
435: Sequent.EMPTY_SEQUENT,
436: SLListOfTaclet.EMPTY_LIST, t_rn));
437: rwbuilder.setName(new Name("plus-zero-elim"));
438: predsuccelim = rwbuilder.getRewriteTaclet();
439:
440: //zero-plus-elim
441: // find(0 + rn) replacewith(rn)
442: rwbuilder = new RewriteTacletBuilder();
443: rwbuilder.setFind(tf.createFunctionTerm(func_plus, new Term[] {
444: t_0, t_rn }));
445: rwbuilder
446: .addTacletGoalTemplate(new RewriteTacletGoalTemplate(
447: Sequent.EMPTY_SEQUENT,
448: SLListOfTaclet.EMPTY_LIST, t_rn));
449: rwbuilder.setName(new Name("zero-plus-elim"));
450: zeropluselim = rwbuilder.getRewriteTaclet();
451:
452: //closewitheq
453: // find(=> rn=rn)
454: SuccTacletBuilder sbuilder = new SuccTacletBuilder();
455: Term t_rneqrn = tf.createEqualityTerm(t_rn, t_rn);
456: sbuilder.setFind(t_rneqrn);
457: sbuilder.setName(new Name("close-with-eq"));
458: closewitheq = sbuilder.getSuccTaclet();
459:
460: //switch first succ
461: // find((rn +1) + rm) replacewith((rn + rm) +1)
462: Term t_rnplus1 = tf.createFunctionTerm(func_plus1,
463: new Term[] { t_rn });
464: Term t_rnplus1plusrm = tf.createFunctionTerm(func_plus,
465: new Term[] { t_rnplus1, t_rm });
466:
467: Term t_rnplusrm = tf.createFunctionTerm(func_plus, new Term[] {
468: t_rn, t_rm });
469: Term t_rnplusrmplus1 = tf.createFunctionTerm(func_plus1,
470: new Term[] { t_rnplusrm });
471:
472: rwbuilder = new RewriteTacletBuilder();
473: rwbuilder.setFind(t_rnplus1plusrm);
474: rwbuilder.addTacletGoalTemplate(new RewriteTacletGoalTemplate(
475: Sequent.EMPTY_SEQUENT, SLListOfTaclet.EMPTY_LIST,
476: t_rnplusrmplus1));
477: rwbuilder.setName(new Name("switch-first-succ"));
478: switchfirstsucc = rwbuilder.getRewriteTaclet();
479:
480: //switch second succ
481: // find(rn + (rm +1)) replacewith((rn + rm) +1)
482: Term t_rmplus1 = tf.createFunctionTerm(func_plus1,
483: new Term[] { t_rm });
484: Term t_rnplus_rmplus1 = tf.createFunctionTerm(func_plus,
485: new Term[] { t_rn, t_rmplus1 });
486: rwbuilder = new RewriteTacletBuilder();
487: rwbuilder.setFind(t_rnplus_rmplus1);
488: rwbuilder.addTacletGoalTemplate(new RewriteTacletGoalTemplate(
489: Sequent.EMPTY_SEQUENT, SLListOfTaclet.EMPTY_LIST,
490: t_rnplusrmplus1));
491: rwbuilder.setName(new Name("switch-second-succ"));
492: switchsecondsucc = rwbuilder.getRewriteTaclet();
493:
494: //elim-succ
495: // find(rn +1 = rm +1) replacewith(rn=rm)
496: Term t_rneqrm = tf.createEqualityTerm(t_rn, t_rm);
497: rwbuilder = new RewriteTacletBuilder();
498: rwbuilder.setFind(tf.createEqualityTerm(t_rnplus1, t_rmplus1));
499: rwbuilder.addTacletGoalTemplate(new RewriteTacletGoalTemplate(
500: Sequent.EMPTY_SEQUENT, SLListOfTaclet.EMPTY_LIST,
501: t_rneqrm));
502: rwbuilder.setName(new Name("succ-elim"));
503: succelim = rwbuilder.getRewriteTaclet();
504:
505: // problem
506:
507: String test1 = "\\predicates {A; B;} (A -> B) -> (!(!(A -> B)))";
508: Term t_test1 = null;
509: try {
510: StringReader fr = new StringReader(test1);
511: KeYParser parser = new KeYParser(ParserMode.PROBLEM,
512: new KeYLexer(fr, null));
513: t_test1 = parser.problem();
514: } catch (Exception e) {
515: System.err.println("Parser Error or Input Error");
516: System.exit(-1);
517: //fail("Parser Error");
518: }
519:
520: ConstrainedFormula cf = new ConstrainedFormula(t_test1,
521: Constraint.BOTTOM);
522: ConstrainedFormula cf2 = new ConstrainedFormula(t_test1,
523: Constraint.BOTTOM);
524: seq_test1 = Sequent.createSequent(
525: Semisequent.EMPTY_SEMISEQUENT,
526: Semisequent.EMPTY_SEMISEQUENT.insert(0, cf)
527: .semisequent());
528:
529: seq_test2 = Sequent.createSequent(Semisequent.EMPTY_SEMISEQUENT
530: .insert(0, cf).semisequent(),
531: Semisequent.EMPTY_SEMISEQUENT);
532:
533: seq_test3 = Sequent.createSequent(Semisequent.EMPTY_SEMISEQUENT
534: .insert(0, cf).semisequent(),
535: Semisequent.EMPTY_SEMISEQUENT.insert(0, cf2)
536: .semisequent());
537:
538: z = new LogicVariable(new Name("z"), nat);
539: Function p = new RigidFunction(new Name("P"), Sort.FORMULA,
540: new Sort[] { nat });
541: func_ns.add(p);
542: Term t_z = tf.createFunctionTerm(z, new Term[0]);
543: Term t_allzpz = tf.createQuantifierTerm(Op.ALL,
544: new QuantifiableVariable[] { z }, tf
545: .createFunctionTerm(p, new Term[] { t_z }));
546: ConstrainedFormula cf3 = new ConstrainedFormula(t_allzpz,
547: Constraint.BOTTOM);
548: seq_testAll = Sequent.createSequent(
549: Semisequent.EMPTY_SEMISEQUENT,
550: Semisequent.EMPTY_SEMISEQUENT.insert(0, cf3)
551: .semisequent());
552:
553: //nat problem:
554: Function const_c = new RigidFunction(new Name("c"), nat,
555: new Sort[0]);
556: func_ns.add(const_c);
557: Function const_d = new RigidFunction(new Name("d"), nat,
558: new Sort[0]);
559: func_ns.add(const_d);
560:
561: Term t_c = tf.createFunctionTerm(const_c, new Term[] {});
562: Term t_d = tf.createFunctionTerm(const_d, new Term[] {});
563: Term t_cplusd = tf.createFunctionTerm(func_plus, new Term[] {
564: t_c, t_d });
565: Term t_dminus1 = tf.createFunctionTerm(func_min1,
566: new Term[] { t_d });
567: Term t_dminus1plus1 = tf.createFunctionTerm(func_plus1,
568: new Term[] { t_dminus1 });
569: Term t_dminus1plus1plusc = tf.createFunctionTerm(func_plus,
570: new Term[] { t_dminus1plus1, t_c });
571: Term t_eq1 = tf.createEqualityTerm(t_cplusd,
572: t_dminus1plus1plusc);
573:
574: Term t_cplus1 = tf.createFunctionTerm(func_plus1,
575: new Term[] { t_c });
576: Term t_cplus1plusd = tf.createFunctionTerm(func_plus,
577: new Term[] { t_cplus1, t_d });
578: Term t_dpluscplus1 = tf.createFunctionTerm(func_plus,
579: new Term[] { t_d, t_cplus1 });
580: Term t_eq2 = tf
581: .createEqualityTerm(t_cplus1plusd, t_dpluscplus1);
582: Term tnat = tf.createJunctorTerm(Op.IMP, t_eq1, t_eq2);
583:
584: // => (c+d) = ((d -1 +1) +c) -> (c +1)+d = (d+c) +1
585: seq_testNat = Sequent.createSequent(
586: Semisequent.EMPTY_SEMISEQUENT,
587: Semisequent.EMPTY_SEMISEQUENT
588: .insert(
589: 0,
590: new ConstrainedFormula(tnat,
591: Constraint.BOTTOM))
592: .semisequent());
593:
594: }
595:
596: public static TacletIndex createTacletIndex() {
597: TacletIndex index = new TacletIndex();
598:
599: index.add(allleft);
600: index.add(allright);
601: index.add(remove_and_left);
602: index.add(remove_and_right);
603: index.add(remove_or_right);
604: index.add(remove_or_left);
605:
606: index.add(cut);
607: index.add(close);
608: index.add(impleft);
609: index.add(impright);
610: index.add(notleft);
611: index.add(notright);
612: index.add(contradiction);
613: index.add(cut);
614: index.add(predsuccelim);
615: index.add(pluszeroelim);
616: index.add(zeropluselim);
617: index.add(succelim);
618: index.add(switchsecondsucc);
619: index.add(switchfirstsucc);
620: index.add(closewitheq);
621:
622: return index;
623: }
624:
625: }
|