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.unittest.cogent;
012:
013: import java.util.HashMap;
014:
015: import de.uka.ilkd.key.logic.Semisequent;
016: import de.uka.ilkd.key.logic.Sequent;
017: import de.uka.ilkd.key.logic.Term;
018: import de.uka.ilkd.key.logic.op.*;
019: import de.uka.ilkd.key.logic.sort.ArraySort;
020: import de.uka.ilkd.key.logic.sort.Sort;
021: import de.uka.ilkd.key.proof.decproc.NumberTranslation;
022: import de.uka.ilkd.key.unittest.ModelGenerator;
023:
024: public class CogentTranslation {
025:
026: private Sequent sequent;
027: // private ConstrainedSet cs;
028: private HashMap array2pointer;
029: private String arrayAxioms = "";
030: private String boundaryAxioms = "";
031: private int pointerCounter = 0;
032:
033: public CogentTranslation(Sequent sequent) {
034: this .sequent = sequent;
035: array2pointer = new HashMap();
036: // this.cs = cs;
037: }
038:
039: protected String translate() throws CogentException {
040: String ante = translate(sequent.antecedent(), true);
041: String succ = translate(sequent.succedent(), false);
042: return "!" + "(" + arrayAxioms + boundaryAxioms + ante
043: + ") || (" + succ + ")";
044: }
045:
046: public String translate(Semisequent ss, boolean ante)
047: throws CogentException {
048: String junctor = ante ? " && " : " || ";
049: String result = ante ? "1" : "0";
050: for (int i = 0; i < ss.size(); i++) {
051: if (cogentizable(ss.get(i).formula())) {
052: try {
053: result += junctor + translate(ss.get(i).formula());
054: } catch (UndefinedTermException e) {
055: //do nothing - formula containing undefined term not added
056: } catch (CogentException e) {
057: //do nothing
058: }
059: }
060: }
061: return result;
062: }
063:
064: public boolean cogentizable(Term t) {
065: Operator op = t.op();
066: return !(ModelGenerator.containsImplicitAttr(t) || op == Op.ALL
067: || op == Op.EX || (op instanceof Modality) || (op instanceof IUpdateOperator));
068: }
069:
070: //convenience method
071: public String translate(Term term) throws CogentException {
072: return translate(term, true);
073: }
074:
075: public String translate(Term term, boolean boundaryAxiom)
076: throws CogentException {
077: Operator op = term.op();
078: if (boundaryAxiom && term.sort() != Sort.FORMULA) {
079: boundaryAxioms += "(" + translate(term, false)
080: + ">=-2147483648) && (" + translate(term, false)
081: + "<=2147483647) &&";
082: }
083: if (op == Op.NOT) {
084: return "(!" + translate(term.sub(0)) + ")";
085: } else if (op == Op.AND) {
086: return "(" + translate(term.sub(0)) + " && "
087: + translate(term.sub(1)) + ")";
088: } else if (op == Op.OR) {
089: return "(" + translate(term.sub(0)) + " || "
090: + translate(term.sub(1)) + ")";
091: } else if (op == Op.IMP) {
092: return "(!" + translate(term.sub(0)) + " || "
093: + translate(term.sub(1)) + ")";
094: } else if (op == Op.EQV || op == Op.EQUALS) {
095: return "(" + translate(term.sub(0)) + " == "
096: + translate(term.sub(1)) + ")";
097: } else if (op == Op.TRUE) {
098: return "1";
099: } else if (op == Op.FALSE) {
100: return "0";
101: } else if (op instanceof AttributeOp) {
102: String attrName = ((AttributeOp) op).attribute().name()
103: .toString();
104: if (attrName.equals("length")
105: && (term.sub(0).sort() instanceof ArraySort)) {
106: arrayAxioms += "(" + translate(term.sub(0)) + "."
107: + attrName + ">=0) &&";
108: }
109: return translate(term.sub(0)) + "."
110: + attrName.substring(attrName.lastIndexOf(":") + 1);
111: } else if (op instanceof ProgramVariable) {
112: String s = op.name().toString();
113: if (s.indexOf(":") != -1) {
114: return s.substring(0, s.indexOf(":"))
115: + s.substring(s.indexOf(":") + 2);
116: }
117: return s;
118: } else if (op instanceof ArrayOp) {
119: String arrayName = (String) array2pointer.get(term);
120: if (arrayName == null) {
121: arrayName = "_arrayPlaceHolder" + (pointerCounter++);
122: array2pointer.put(term, arrayName);
123: }
124: createArrayAxiom(arrayName, term);
125: return "*" + arrayName;
126: } else if (term.op() == Op.NULL) {
127: return "null";
128: } else if (op instanceof RigidFunction && term.arity() == 0
129: && op.name().toString().indexOf("undef(") == -1
130: && !(op instanceof Metavariable)) {
131: if (op.name().toString().equals("int_Min")) {
132: return "-2147483648";
133: } else if (op.name().toString().equals("int_Max")) {
134: return "2147483647";
135: } else if (op.name().toString().equals("short_Min")) {
136: return "-32768";
137: } else if (op.name().toString().equals("short_Max")) {
138: return "32767";
139: } else if (op.name().toString().equals("byte_Min")) {
140: return "-128";
141: } else if (op.name().toString().equals("byte_Max")) {
142: return "127";
143: } else if (op.name().toString().equals("char_Min")) {
144: return "0";
145: } else if (op.name().toString().equals("char_Max")) {
146: return "65535";
147: } else {
148: return op.name().toString();
149: }
150: } else if (op instanceof Function) {
151: String name = op.name().toString().intern();
152: if (name.equals("add") || name.equals("jadd")) {
153: return "(" + translate(term.sub(0)) + " + "
154: + translate(term.sub(1)) + ")";
155: } else if (name.equals("sub") || name.equals("jsub")
156: || name.equals("subJint")) {
157: return "(" + translate(term.sub(0)) + " - "
158: + translate(term.sub(1)) + ")";
159: } else if (name.equals("neg") || name.equals("jneg")
160: || name.equals("negJint")) {
161: return "-" + translate(term.sub(0));
162: } else if (name.equals("mul") || name.equals("jmul")
163: || name.equals("mulJint")) {
164: return "(" + translate(term.sub(0)) + " * "
165: + translate(term.sub(1)) + ")";
166: } else if (name.equals("div") || name.equals("jdiv")
167: || name.equals("divJint")) {
168: return "(" + translate(term.sub(0)) + " / "
169: + translate(term.sub(1)) + ")";
170: } else if (name.equals("mod") || name.equals("jmod")
171: || name.equals("modJint")) {
172: return "(" + translate(term.sub(0)) + " % "
173: + translate(term.sub(1)) + ")";
174: } else if (name.equals("lt")) {
175: return "(" + translate(term.sub(0)) + " < "
176: + translate(term.sub(1)) + ")";
177: } else if (name.equals("gt")) {
178: return "(" + translate(term.sub(0)) + " > "
179: + translate(term.sub(1)) + ")";
180: } else if (name.equals("leq")) {
181: return "(" + translate(term.sub(0)) + " <= "
182: + translate(term.sub(1)) + ")";
183: } else if (name.equals("geq")) {
184: return "(" + translate(term.sub(0)) + " >= "
185: + translate(term.sub(1)) + ")";
186: } else if (name.equals("undef")) {
187: throw new UndefinedTermException(term);
188: } else if (name.equals("Z") || name.equals("C")) {
189: return NumberTranslation.translate(term.sub(0))
190: .toString();
191: }
192: }
193: throw new CogentException("Term " + term
194: + " not translatable to " + "Congent input syntax.");
195: }
196:
197: private void createArrayAxiom(String arrayName, Term term)
198: throws CogentException {
199: arrayAxioms += "(" + arrayName + "==" + translate(term.sub(0))
200: + " + " + translate(term.sub(1)) + ") &&";
201: }
202: }
|