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: package de.uka.ilkd.key.proof.decproc;
011:
012: import java.util.HashMap;
013: import java.util.Iterator;
014: import java.util.Vector;
015:
016: import org.apache.log4j.Logger;
017:
018: import de.uka.ilkd.key.collection.ListOfString;
019: import de.uka.ilkd.key.collection.SLListOfString;
020: import de.uka.ilkd.key.java.Services;
021: import de.uka.ilkd.key.logic.*;
022: import de.uka.ilkd.key.logic.op.*;
023: import de.uka.ilkd.key.logic.sort.Sort;
024: import de.uka.ilkd.key.rule.SyntacticalReplaceVisitor;
025: import de.uka.ilkd.key.util.Debug;
026:
027: /**
028: *
029: * @author daniels
030: *
031: * The class responsible for converting a sequent into the Simplify input language.
032: * It is public because ASM-KeY inherits form it to provide a version suppporting
033: * asm operators.
034: */
035: public class SimplifyTranslation extends DecProcTranslation {
036:
037: private HashMap cacheForUninterpretedSymbols = null;
038: private ListOfString sortAxioms = SLListOfString.EMPTY_LIST;
039: private boolean quantifiersOccur = false;
040: private Sort jbyteSort;
041: private Sort jshortSort;
042: private Sort jintSort;
043: private Sort jlongSort;
044: private Sort jcharSort;
045: private Sort integerSort;
046: private static long counter = 0;
047:
048: /**
049: * Just a constructor which starts the conversion to Simplify syntax. The
050: * result can be fetched with
051: *
052: * @see getText-
053: * @param sequent
054: * The sequent which shall be translated.
055: * @param cs
056: * The constraints which shall be incorporated.
057: * @param localmv
058: * The local metavariables, should be the ones introduced after
059: * the last branch.
060: */
061: public SimplifyTranslation(Sequent sequent, ConstraintSet cs,
062: SetOfMetavariable localmv, Services services,
063: boolean lightWeight) throws SimplifyException {
064: super (sequent, cs, localmv, services);
065: jbyteSort = services.getTypeConverter().getByteLDT()
066: .targetSort();
067: jshortSort = services.getTypeConverter().getShortLDT()
068: .targetSort();
069: jintSort = services.getTypeConverter().getIntLDT().targetSort();
070: jlongSort = services.getTypeConverter().getLongLDT()
071: .targetSort();
072: jcharSort = services.getTypeConverter().getCharLDT()
073: .targetSort();
074: integerSort = services.getTypeConverter().getIntegerLDT()
075: .targetSort();
076: cacheForUninterpretedSymbols = new HashMap();
077: StringBuffer hb = translate(sequent, lightWeight);
078: text = predicate.toString() + produceClosure(hb);
079: logger.info("SimplifyTranslation:\n" + text);
080: if (notes.length() > 0) {
081: logger.info(notes);
082: }
083: }
084:
085: public SimplifyTranslation(Sequent sequent, ConstraintSet cs,
086: SetOfMetavariable localmv, Services services)
087: throws SimplifyException {
088: this (sequent, cs, localmv, services, false);
089: }
090:
091: /**
092: * For translating only terms and not complete sequents.
093: */
094: public SimplifyTranslation(Services s) throws SimplifyException {
095: this (null, null, null, s, false);
096: }
097:
098: /**
099: * Goes through the collected metavariables and quantifies them with
100: * universal-quantifieres if they are global and with existential
101: * quantifiers if they are local.
102: * @param s The StringBuffer the quantifieres shall be pre- and
103: * the trailing parantheses be appended.
104: * @returns The modified StringBuffer as a String.
105: */
106: protected String produceClosure(StringBuffer s) {
107: StringBuffer tmp = new StringBuffer("(");
108: tmp.append(DecisionProcedureSimplifyOp.ALL).append(" (");
109: for (Iterator i = usedGlobalMv.iterator(); i.hasNext();) {
110: tmp.append(' ').append(
111: getUniqueVariableName((Metavariable) i.next()));
112: }
113: tmp.append(")");
114: tmp.append("(").append(DecisionProcedureSimplifyOp.EX).append(
115: " (");
116: for (Iterator i = usedLocalMv.iterator(); i.hasNext();) {
117: tmp.append(' ').append(
118: getUniqueVariableName((Operator) i.next()));
119: }
120: tmp.append(")\n ");
121: tmp.append(s);
122: tmp.append("\n))");
123: return tmp.toString();
124: }
125:
126: protected final StringBuffer translate(Sequent sequent)
127: throws SimplifyException {
128: return translate(sequent, false);
129: }
130:
131: /**
132: * Translates the given sequent into "Simplify" input syntax and adds the
133: * resulting string to the StringBuffer sb.
134: *
135: * @param s
136: * the Sequent which should be written in Simplify syntax
137: */
138: protected final StringBuffer translate(Sequent sequent,
139: boolean lightWeight) throws SimplifyException {
140: // computeModuloConstraints(sequent);
141: StringBuffer hb = new StringBuffer();
142: hb.append('(').append(DecisionProcedureSimplifyOp.IMP).append(
143: ' ');
144: hb.append(translate(sequent.antecedent(), ANTECEDENT,
145: lightWeight));
146: hb.append("\n");
147: hb
148: .append(translate(sequent.succedent(), SUCCEDENT,
149: lightWeight));
150: hb.append(')');
151:
152: if (sortAxioms != SLListOfString.EMPTY_LIST && quantifiersOccur) {
153: String sar[] = sortAxioms.toArray();
154: String axioms = sar[0];
155: for (int i = 1; i < sar.length; i++) {
156: axioms = "(" + DecisionProcedureSimplifyOp.AND + " "
157: + axioms + " " + sar[i] + ")";
158: }
159: hb.insert(0, "(" + DecisionProcedureSimplifyOp.IMP + " "
160: + axioms);
161: hb.append(')');
162: //System.out.println(axioms);
163: }
164:
165: return hb;
166: }
167:
168: protected final StringBuffer translate(Semisequent ss,
169: int skolemization) throws SimplifyException {
170: return translate(ss, skolemization, false);
171: }
172:
173: /**
174: * Translates the given Semisequent into "Simplify" input syntax and adds
175: * the resulting string to the StringBuffer sb.
176: *
177: * @param ss
178: * the SemiSequent which should be written in Simplify syntax
179: * @param antesucc
180: * true for antecedent, false for succedent
181: */
182: protected final StringBuffer translate(Semisequent ss,
183: int skolemization, boolean lightWeight)
184: throws SimplifyException {
185: StringBuffer hb = new StringBuffer();
186: hb.append('(');
187: if (skolemization == ANTECEDENT) {
188: hb.append(DecisionProcedureSimplifyOp.AND);
189: } else {
190: hb.append(DecisionProcedureSimplifyOp.OR);
191: }
192: for (int i = 0; i < ss.size(); ++i) {
193: hb.append(' ');
194: hb.append(translate(ss.get(i), lightWeight));
195: }
196: // if (skolemization == ANTECEDENT) {
197: // hb.append(' ');
198: // hb.append(DecisionProcedureSimplifyOp.LIMIT_FACTS);
199: // hb.append('\n').append(translate(moduloConjoin(), new Vector()));
200: // }
201: hb.append(')');
202: return hb;
203: }
204:
205: /**
206: * Translates the given ConstrainedFormula into "Simplify" input syntax and
207: * adds the resulting string to the StringBuffer sb.
208: *
209: * @param cf
210: * the ConstrainedFormula which should be written in Simplify
211: * syntax
212: */
213: protected final StringBuffer translate(ConstrainedFormula cf,
214: boolean lightWeight) throws SimplifyException {
215: StringBuffer hb = new StringBuffer();
216: if (constraintSet.used(cf)) {
217: SyntacticalReplaceVisitor srVisitor = new SyntacticalReplaceVisitor(
218: constraintSet.chosenConstraint());
219: cf.formula().execPostOrder(srVisitor);
220: Term t = srVisitor.getTerm();
221: Operator op = t.op();
222: if (!lightWeight || !(op instanceof Modality)
223: && !(op instanceof IUpdateOperator)
224: && !(op instanceof IfThenElse) && op != Op.ALL
225: && op != Op.EX) {
226: hb.append(translate(t, new Vector()));
227: }
228: }
229: return hb;
230: }
231:
232: /**
233: * Translates the given term into "Simplify" input syntax and adds the
234: * resulting string to the StringBuffer sb.
235: *
236: * @param term
237: * the Term which should be written in Simplify syntax
238: * @param quantifiedVars
239: * a Vector containing all variables that have been bound in
240: * super-terms. It is only used for the translation of modulo
241: * terms, but must be looped through until we get there.
242: */
243: public final StringBuffer translate(Term term, Vector quantifiedVars)
244: throws SimplifyException {
245: Operator op = term.op();
246: if (op == Op.NOT) {
247: return (translateSimpleTerm(term,
248: DecisionProcedureSimplifyOp.NOT, quantifiedVars));
249: } else if (op == Op.AND) {
250: return (translateSimpleTerm(term,
251: DecisionProcedureSimplifyOp.AND, quantifiedVars));
252: } else if (op == Op.OR) {
253: return (translateSimpleTerm(term,
254: DecisionProcedureSimplifyOp.OR, quantifiedVars));
255: } else if (op == Op.IMP) {
256: return (translateSimpleTerm(term,
257: DecisionProcedureSimplifyOp.IMP, quantifiedVars));
258: } else if (op == Op.EQV) {
259: return (translateSimpleTerm(term,
260: DecisionProcedureSimplifyOp.EQV, quantifiedVars));
261: } else if (op == Op.EQUALS) {
262: return (translateSimpleTerm(term,
263: DecisionProcedureSimplifyOp.EQUALS, quantifiedVars));
264: } else if (op == Op.ALL || op == Op.EX) {
265: quantifiersOccur = true;
266: StringBuffer hb = new StringBuffer();
267: Debug.assertTrue(term.arity() == 1);
268: hb.append('(').append(
269: op == Op.ALL ? DecisionProcedureSimplifyOp.ALL
270: : DecisionProcedureSimplifyOp.EX).append(
271: " (");
272: ArrayOfQuantifiableVariable vars = term.varsBoundHere(0);
273: Debug.assertTrue(vars.size() == 1);
274: String v = translateVariable(
275: vars.getQuantifiableVariable(0)).toString();
276: hb.append(v);
277: Vector cloneVars = (Vector) quantifiedVars.clone();
278: collectQuantifiedVars(cloneVars, term);
279: hb.append(") ");
280: // we now add an implication or conjunction of a type predicate if the type is
281: // different from int
282:
283: hb.append("(").append(
284: op == Op.ALL ? DecisionProcedureSimplifyOp.IMP
285: : DecisionProcedureSimplifyOp.AND);
286: Sort sort = vars.getQuantifiableVariable(0).sort();
287: if (isSomeIntegerSort(sort))
288: sort = integerSort;
289: hb.append("(" + getUniqueVariableName(sort) + " " + v
290: + " )");
291: addPredicate(getUniqueVariableName(sort).toString(), 1);
292: hb.append(translate(term.sub(0), cloneVars));
293: hb.append("))");
294:
295: return hb;
296: } else if (op == Op.TRUE) {
297: return (new StringBuffer(DecisionProcedureSimplifyOp.TRUE));
298: } else if (op == Op.FALSE) {
299: return (new StringBuffer(DecisionProcedureSimplifyOp.FALSE));
300: } else if (op instanceof AttributeOp) {
301: return (translateAttributeOpTerm(term, quantifiedVars));
302: } else if (op instanceof ProgramMethod) {
303: return (translateSimpleTerm(term, getUniqueVariableName(op)
304: .toString(), quantifiedVars));
305: } else if (op instanceof LogicVariable
306: || op instanceof ProgramVariable) {
307: return (translateVariable(op));
308: } else if (op instanceof Metavariable) {
309: if (localMetavariables.contains((Metavariable) op)) {
310: usedLocalMv.add(op);
311: } else {
312: usedGlobalMv.add(op);
313: }
314: return (translateVariable(op));
315: } else if (op instanceof ArrayOp) {
316: return (translateSimpleTerm(term, "ArrayOp", quantifiedVars));
317: } else if (op instanceof Function) {
318: String name = op.name().toString().intern();
319: if (name.equals("add")) {
320: return (translateSimpleTerm(term,
321: DecisionProcedureSimplifyOp.PLUS,
322: quantifiedVars));
323: } else if (name.equals("sub")) {
324: return (translateSimpleTerm(term,
325: DecisionProcedureSimplifyOp.MINUS,
326: quantifiedVars));
327: } else if (name.equals("neg")) {
328: //%%: This is not really hygienic
329: return (translateUnaryMinus(term,
330: DecisionProcedureSimplifyOp.MINUS,
331: quantifiedVars));
332: } else if (name.equals("mul")) {
333: return (translateSimpleTerm(term,
334: DecisionProcedureSimplifyOp.MULT,
335: quantifiedVars));
336: } else if (name.equals("div")) {
337: notes
338: .append(
339: "Division encountered which is not "
340: + "supported by Simplify.")
341: .append(
342: "It is treated as an uninterpreted function.\n");
343: return (translateSimpleTerm(term,
344: getUniqueVariableName(op).toString(),
345: quantifiedVars));
346: // }
347: // else if (name.equals("mod")) {
348: // Term tt = translateModulo(term, quantifiedVars);
349: // if (tt == null) {
350: // return uninterpretedTerm(term, true);
351: // } else {
352: // return translate(tt, quantifiedVars);
353: // }
354: } else if (name.equals("lt")) {
355: return (translateSimpleTerm(term,
356: DecisionProcedureSimplifyOp.LT, quantifiedVars));
357: } else if (name.equals("gt")) {
358: return (translateSimpleTerm(term,
359: DecisionProcedureSimplifyOp.GT, quantifiedVars));
360: } else if (name.equals("leq")) {
361: return (translateSimpleTerm(term,
362: DecisionProcedureSimplifyOp.LEQ, quantifiedVars));
363: } else if (name.equals("geq")) {
364: return (translateSimpleTerm(term,
365: DecisionProcedureSimplifyOp.GEQ, quantifiedVars));
366: } else if (name.equals("Z") || name.equals("C")) {
367: Debug.assertTrue(term.arity() == 1);
368:
369: String res = NumberTranslation.translate(term.sub(0))
370: .toString();
371: final Sort sort;
372: if (isSomeIntegerSort(term.sort()))
373: sort = integerSort;
374: else
375: sort = term.sort();
376: String ax = "("
377: + getUniqueVariableName(sort).toString() + " "
378: + res + ")";
379: if (!sortAxioms.contains(ax)) {
380: sortAxioms = sortAxioms
381: .prepend(new String[] { ax });
382: addPredicate(
383: getUniqueVariableName(sort).toString(), 1);
384: }
385: return (new StringBuffer(res));
386: /*
387: // it's sick but if you need to give a demo...
388: } else if (name.equals("short_MIN")) {
389: return new StringBuffer("-32768");
390: } else if (name.equals("short_MAX")) {
391: return new StringBuffer("32767");
392: } else if (name.equals("int_MIN")) {
393: return new StringBuffer("-500000");
394: } else if (name.equals("int_MAX")) {
395: return new StringBuffer("500000");
396: */
397: } else if (name.equals("byte_MIN")
398: | name.equals("byte_MAX")
399: | name.equals("byte_RANGE")
400: | name.equals("byte_HALFRANGE")
401: | name.equals("short_MIN")
402: | name.equals("short_MAX")
403: | name.equals("short_RANGE")
404: | name.equals("short_HALFRANGE")
405: | name.equals("int_MIN") | name.equals("int_MAX")
406: | name.equals("int_RANGE")
407: | name.equals("int_HALFRANGE")
408: | name.equals("long_MIN") | name.equals("long_MAX")
409: | name.equals("long_RANGE")
410: | name.equals("long_HALFRANGE")) {
411: return (translateSimpleTerm(term, name, quantifiedVars));
412: } else {
413: if (term.sort() == Sort.FORMULA) {
414: addPredicate(getUniqueVariableName(op).toString(),
415: op.arity());
416: }
417: return (translateSimpleTerm(term,
418: getUniqueVariableName(op).toString(),
419: quantifiedVars));
420: }
421: } else if ((op instanceof Modality)
422: || (op instanceof IUpdateOperator)
423: || (op instanceof IfThenElse)) {
424: return (uninterpretedTerm(term, true));
425: } else {
426: return (translateUnknown(term));
427: }
428: }
429:
430: /**
431: * Takes care of sequent tree parts that were not matched in translate(term,
432: * skolemization). In this class it just produces a warning, nothing more.
433: * It is provided as a hook for subclasses.
434: *
435: * @param term
436: * The Term given to translate
437: * @throws SimplifyException
438: */
439: protected StringBuffer translateUnknown(Term term)
440: throws SimplifyException {
441: return (opNotKnownWarning(term));
442: }
443:
444: protected StringBuffer opNotKnownWarning(Term term)
445: throws SimplifyException {
446: logger
447: .warn("Warning: unknown operator while translating into Simplify "
448: + "syntax. Translation to Simplify will be stopped here.\n"
449: + "opClass="
450: + term.op().getClass().getName()
451: + ", opName="
452: + term.op().name()
453: + ", sort="
454: + term.sort().name());
455: throw new SimplifyException(term.op().name()
456: + " not known by Simplify");
457: }
458:
459: /**
460: * Used to give a variable (program, logic, meta) a unique name.
461: *
462: * @param op
463: * The variable to be translated/renamed.
464: */
465: protected final StringBuffer translateVariable(Operator op) {
466: StringBuffer res = getUniqueVariableName(op);
467: if (op instanceof ProgramVariable || op instanceof Metavariable) {
468: final Sort sort;
469: if (isSomeIntegerSort(op.sort(null)))
470: sort = integerSort;
471: else
472: sort = op.sort(null);
473: String ax = "(" + getUniqueVariableName(sort).toString()
474: + " " + res + ")";
475: if (!sortAxioms.contains(ax)) {
476: sortAxioms = sortAxioms.prepend(new String[] { ax });
477: addPredicate(getUniqueVariableName(sort).toString(), 1);
478: }
479: }
480: return res;
481: }
482:
483: /**
484: * produces a unique name for the given Variable, enclosed in '|' and with a
485: * unique hashcode.
486: *
487: * @param op
488: * The variable to get a new name.
489: */
490: protected final StringBuffer getUniqueVariableName(Named op) {
491: String name = op.name().toString();
492: if (name.indexOf("undef(") != -1) {
493: name = "_undef";
494: }
495: if (name.indexOf("::") == -1 && name.indexOf(".") == -1
496: && name.indexOf("-") == -1 && !name.startsWith("_")
497: && name.indexOf("[") == -1 && name.indexOf("]") == -1) {
498: return new StringBuffer(name).append("_").append(
499: getUniqueHashCode(op));
500: }
501: return new StringBuffer("|").append(name).append("_").append(
502: getUniqueHashCode(op)).append("|");
503: }
504:
505: protected final StringBuffer uninterpretedTerm(Term term,
506: boolean modRenaming) {
507: if (cacheForUninterpretedSymbols.containsKey(term))
508: return (StringBuffer) cacheForUninterpretedSymbols
509: .get(term);
510: StringBuffer hb = new StringBuffer();
511: StringBuffer temp = new StringBuffer();
512: temp.append('|').append(term.op().name()).append('_');
513: if (modRenaming) {
514: temp.append(getUniqueHashCodeForUninterpretedTerm(term));
515: } else {
516: temp.append(getUniqueHashCode(term));
517: }
518: temp.append('|');
519: hb.append(temp);
520: IteratorOfQuantifiableVariable i;
521: for (i = term.freeVars().iterator(); i.hasNext();) {
522: hb.append(' ');
523: hb.append(translateVariable(i.next()));
524: }
525:
526: if (term.sort() != Sort.FORMULA) {
527: String ax;
528: final Sort sort;
529: if (isSomeIntegerSort(term.sort()))
530: sort = integerSort;
531: else
532: sort = term.sort();
533: if (term.arity() > 0)
534: ax = "(" + getUniqueVariableName(sort).toString()
535: + " (" + hb + "))";
536: else
537: ax = "(" + getUniqueVariableName(sort).toString() + " "
538: + hb + ")";
539: if (!sortAxioms.contains(ax)) {
540: sortAxioms = sortAxioms.prepend(new String[] { ax });
541: addPredicate(getUniqueVariableName(sort).toString(), 1);
542: }
543: }
544:
545: hb.insert(0, '(');
546: hb.append(')');
547:
548: if (term.sort() == Sort.FORMULA)
549: addPredicate(temp.toString(), term.freeVars().size());
550: cacheForUninterpretedSymbols.put(term, hb);
551: return hb;
552: }
553:
554: /**
555: * Takes a term and translates it with its argument in the Simplify syntax.
556: *
557: * @param term
558: * The term to be converted.
559: * @param name
560: * The name that should be used for the term (should be unique,
561: * it should be taken care of that somewhere else (if desired)).
562: * @param quantifiedVars
563: * a Vector containing all variables that have been bound in
564: * super-terms. It is only used for the translation of modulo
565: * terms, but must be looped through until we get there.
566: */
567: protected final StringBuffer translateSimpleTerm(Term term,
568: String name, Vector quantifiedVars)
569: throws SimplifyException {
570: StringBuffer hb = new StringBuffer();
571: hb.append('(').append(name);
572: StringBuffer res = null;
573: for (int i = 0; i < term.arity(); ++i) {
574: Debug.assertTrue(term.varsBoundHere(i).size() == 0);
575: hb.append(' ');
576: res = translate(term.sub(i), quantifiedVars);
577: if (res != null && term.sub(i).sort() != Sort.FORMULA) {
578: final Sort sort;
579: if (isSomeIntegerSort(term.sub(i).sort()))
580: sort = integerSort;
581: else
582: sort = term.sub(i).sort();
583: String ax = "("
584: + getUniqueVariableName(sort).toString() + " "
585: + res + ")";
586: if (!sortAxioms.contains(ax)) {
587: sortAxioms = sortAxioms
588: .prepend(new String[] { ax });
589: addPredicate(
590: getUniqueVariableName(sort).toString(), 1);
591: }
592: }
593:
594: hb.append(res);
595: }
596: hb.append(')');
597:
598: // add sort axioms
599: return hb;
600: }
601:
602: /**
603: * Takes an AttributeOp and translates it into the Simplify syntax.
604: *
605: * @param term
606: * The term to be converted.
607: * @param quantifiedVars
608: * a Vector containing all variables that have been bound in
609: * super-terms. It is only used for the translation of modulo
610: * terms, but must be looped through until we get there.
611: */
612: protected final StringBuffer translateAttributeOpTerm(Term term,
613: Vector quantifiedVars) throws SimplifyException {
614: StringBuffer hb = new StringBuffer();
615: if (logger.isDebugEnabled()) {
616: logger.debug("opClass=" + term.op().getClass().getName()
617: + ", opName=" + term.op().name() + ", sort="
618: + term.sort().name());
619: }
620:
621: hb.append(getUniqueVariableName(term.op()));
622: Debug.assertTrue(term.varsBoundHere(0).size() == 0);
623: hb.append(' ');
624: hb.append(translate(term.sub(0), quantifiedVars));
625: hb.insert(0, '(');
626: hb.append(')');
627:
628: final Sort sort;
629: if (isSomeIntegerSort(term.sort()))
630: sort = integerSort;
631: else
632: sort = term.sort();
633: String ax = "(" + getUniqueVariableName(sort).toString() + " "
634: + hb + ")";
635: if (!sortAxioms.contains(ax)) {
636: sortAxioms = sortAxioms.prepend(new String[] { ax });
637: addPredicate(getUniqueVariableName(sort).toString(), 1);
638: }
639:
640: return hb;
641: }
642:
643: /**
644: * Translates the unary minus ~m into a "0 -" construct. Could be solved
645: * better with a newly created term!!!
646: *
647: * @param term
648: * The term to be converted.
649: * @param name
650: * The name that should be used for the term (should be unique,
651: * it should be taken care of that somewhere else (if desired)).
652: * @param quantifiedVars
653: * a Vector containing all variables that have been bound in
654: * super-terms. It is only used for the translation of modulo
655: * terms, but must be looped through until we get there.
656: */
657: protected final StringBuffer translateUnaryMinus(Term term,
658: String name, Vector quantifiedVars)
659: throws SimplifyException {
660: StringBuffer hb = new StringBuffer();
661: hb.append('(').append(name).append(" 0");
662: hb.append(translate(term.sub(0), quantifiedVars));
663: hb.append(')');
664: return hb;
665: }
666:
667: /**
668: * Adds a predicate to the internal set and adds a line to declare the
669: * predicate to the declarator stringbuffer.
670: *
671: * @param name
672: * The name of the predicate (no KeY representation jas to
673: * exist).
674: * @param arity
675: * The arity of the term.
676: */
677: protected final void addPredicate(String name, int arity) {
678: if (!predicateSet.contains(name)) {
679: predicateSet.add(name);
680: predicate.append("(DEFPRED (").append(name);
681: for (int i = 0; i < arity; ++i) {
682: predicate.append(" x").append(counter++);
683: }
684: predicate.append("))\n");
685: }
686: }
687:
688: /**
689: * For some terms (AttributeOps) the order in KeY is different than the
690: * order of the user or Simplify expects.
691: *
692: * @return the simplified version of the Term t in reversed order
693: * @param t
694: * the Term which should be written in Simplify syntax, but in
695: * reverse order compared to the internal order in KeY
696: */
697: protected final StringBuffer printlastfirst(Term t) {
698: StringBuffer sbuff = new StringBuffer();
699: if (t.op().arity() > 0) {
700: Debug.assertTrue(t.op().arity() == 1);
701: sbuff.append(printlastfirst(t.sub(0)));
702: //sbuff.append('.');
703: }
704: sbuff.append(t.op().name()).append("\\|").append(
705: getUniqueHashCode(t.op()));
706: return sbuff;
707: }
708:
709: static Logger logger = Logger.getLogger(SimplifyTranslation.class
710: .getName());
711:
712: /**
713: * Used just to be called from DecProcTranslation
714: * @see de.uka.ilkd.key.proof.decproc.DecProcTranslation#translate(de.uka.ilkd.key.logic.Term, int)
715: */
716: protected final StringBuffer translate(Term term,
717: int skolemization, Vector quantifiedVars)
718: throws SimplifyException {
719: return translate(term, quantifiedVars);
720: }
721:
722: private boolean isSomeIntegerSort(Sort s) {
723: if (s == jbyteSort || s == jshortSort || s == jintSort
724: || s == jlongSort || s == jcharSort)
725: return true;
726: return false;
727: }
728: }
|