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