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.translation;
012:
013: import java.math.BigInteger;
014: import java.util.HashMap;
015: import java.util.HashSet;
016: import org.apache.log4j.Logger;
017: import de.uka.ilkd.key.logic.op.Function;
018: import de.uka.ilkd.key.logic.op.Operator;
019: import de.uka.ilkd.key.logic.sort.ObjectSort;
020: import de.uka.ilkd.key.logic.sort.Sort;
021: import de.uka.ilkd.key.proof.decproc.DecisionProcedureSmtAufliaOp;
022: import de.uka.ilkd.key.proof.decproc.SmtAufliaTranslation;
023: import de.uka.ilkd.key.proof.decproc.TypeBoundTranslation;
024: import de.uka.ilkd.key.proof.decproc.smtlib.*;
025:
026: /** This class represents the translation rule for <tt>Function</tt>s.
027: * <p>
028: * There are several classes of KeY <tt>Function</tt>s that are translated diffenently:
029: * <ul>
030: * <li>ADD, SUB, NEG and the linear MUL are translated into SMT-LIB <tt>InterpretedFunction</tt>s</li>
031: * <li>GT, GEQ, LT and LEQ are translated into SMT-LIB <tt>PredicateFormula</tt>e</li>
032: * <li>inBYTE, inSHORT, inINT, inLONG and inCHAR are translated into a <tt>ConnectiveFormula</tt>
033: * consisting of two LT-<tt>PredicateFormula</tt></li>
034: * <li>Type boundaries like int_MIN, int_MAX, int_RANGE, int_HALFRANGE, ... (same for byte, short,
035: * long and char) are translated into a <tt>NumberConstantTerm</tt> or a
036: * <tt>InterpretedFuncTerm</tt>s if they represent a negative value<li>
037: * <li>TRUE and FALSE as constant <tt>Function</tt>s of <tt>Sort</tt> boolean are translated into
038: * <tt>TruthValueFormula</tt>s</li>
039: * <li><tt>Function</tt> symbols like #, Z, C, NEGLIT and 0..9, which represent number and character
040: * constants in KeY, are parsed and translated into an SMT-LIB <tt>NumberConstantTerm</tt>
041: * or an <tt>InterpretedFuncTerm</tt>, if the constants are negative</li>
042: * <li>All further <tt>Function</tt>s of <tt>Sort</tt> INT or OBJECT are translated into SMT-LIB
043: * <tt>UninterpretedFuncTerm</tt>s</li>
044: * <li>All further <tt>Function</tt>s of <tt>Sort</tt> <tt>FORMULA</tt> or BOOLEAN are translated
045: * into SMT-LIB <tt>UninterpretedPredFormula</tt>e</li>
046: * </ul>
047: * All uninterpreted function and predicate names consists of a prefix indicating that they
048: * represent translations of a <tt>Function</tt> and a suffix allowing to quickly distinguish
049: * between uninterpreted functoins and predicates
050: *
051: * @author akuwertz
052: * @version 1.4, 11/10/2006 (Added type predicates for uninterpreted functions)
053: */
054:
055: public class TranslateFunction implements IOperatorTranslation {
056:
057: /* Additional fields */
058:
059: /** A prefix used in the names of the uninterpreted functions and predicates respectively to
060: * indicate that they represent the translation of a <tt>Function</tt> */
061: private static final String funcPrefix = "Func_";
062:
063: /** A suffix used in the name of the created uninterpreted function to indicate that it
064: * represents the translation of an integer attribute */
065: private static final String funcIntSuffix = "_int";
066: /** A suffix used in the name of the created uninterpreted function to indicate that it
067: * represents the translation of an object attribute */
068: private static final String funcObjectSuffix = "_object";
069:
070: /** A suffix used in the name of the created uninterpreted function to mark it as function */
071: private static final String funcUifSuffix = "_UIF";
072: /** A suffix used in the name of the created uninterpreted predicate to mark it as predicate */
073: private static final String funcUipSuffix = "_UIP";
074:
075: /** A <tt>HashMap</tt> containing the translation of all functions having interpreted
076: * equivalents in SMT-LIB */
077: private static final HashMap interpredFuncs = new HashMap(4, 1);
078: /** A <tt>HashMap</tt> containing the translation of all comparative predicates */
079: private static final HashMap compPreds = new HashMap(4, 1);
080: /** A <tt>HashSet</tt> containing the names of all type boundary predicates */
081: private static final HashSet typeBoundPreds = new HashSet(8);
082: /** A <tt>HashSet</tt> containing the <tt>String</tt> representations of all type boundaries */
083: private static final HashSet typeBounds = new HashSet(32);
084:
085: /** The common prefix of type boundary predicates */
086: private static final String typePredPrefix = "in";
087: /** The common suffix of the mininum type boundary */
088: private static final String typeBoundMinSuffix = "_MIN";
089: /** The common suffix of the maximum type boundary */
090: private static final String typeBoundMaxSuffix = "_MAX";
091:
092: /** A cache for <tt>BigInteger</tt> instances using during number constant translation */
093: private static final BigInteger[] cachedBigInts = new BigInteger[11];
094:
095: /** A <tt>Logger</tt> for logging and debugging operator translation */
096: private static final Logger logger = Logger
097: .getLogger(TranslateFunction.class.getName());
098: // Logger is created hierarchical to inherit configuration and behaviour from parent
099:
100: /* String constants for error messages */
101: private static final String translationFailure = "Translation of function failed due to illegal arguments on visitor stack:\n";
102: private static final String failurerCauseNoTerm = " expected an argument of class Term (SMT-LIB) and found the object:\n";
103: private static final String failureCauseNoBigInt = " expected an argument of class BigInteger and found the object:\n";
104: private static final String unsupportedFunction = "Translation of function failed: ";
105: private static final String unsupportedFunctionFailure = "\nCaused by unsupported Sort: ";
106:
107: /** Just a mere constructor. */
108: public TranslateFunction() {
109:
110: // Set translations for functions having interpreted equivalents
111: interpredFuncs.put("add", DecisionProcedureSmtAufliaOp.PLUS);
112: interpredFuncs.put("sub", DecisionProcedureSmtAufliaOp.MINUS);
113: interpredFuncs.put("neg", DecisionProcedureSmtAufliaOp.UMINUS);
114: interpredFuncs.put("mul", DecisionProcedureSmtAufliaOp.MULT);
115:
116: // Set translations for comparative predicates
117: compPreds.put("gt", DecisionProcedureSmtAufliaOp.GT);
118: compPreds.put("geq", DecisionProcedureSmtAufliaOp.GEQ);
119: compPreds.put("lt", DecisionProcedureSmtAufliaOp.LT);
120: compPreds.put("leq", DecisionProcedureSmtAufliaOp.LEQ);
121:
122: // Initialise set of type boundary predicates
123: final String[] typePredsArray = { "inByte", "inShort", "inInt",
124: "inLong", "inChar" };
125: for (int i = 0; i < typePredsArray.length; i++)
126: typeBoundPreds.add(typePredsArray[i]);
127:
128: // Initialise set of type boundary strings
129: final String[] typeBoundsArray = { "int_MIN", "int_MAX",
130: "int_HALFRANGE", "int_RANGE", "char_MIN", "char_MAX",
131: "char_RANGE", "long_MIN", "long_MAX", "long_HALFRANGE",
132: "long_RANGE", "byte_MIN", "byte_MAX", "byte_HALFRANGE",
133: "byte_RANGE", "short_MIN", "short_MAX",
134: "short_HALFRANGE", "short_RANGE" };
135: for (int i = 0; i < typeBoundsArray.length; i++)
136: typeBounds.add(typeBoundsArray[i]);
137: }
138:
139: /* Public method implementation */
140:
141: /* (non-Javadoc)
142: * @see de.uka.ilkd.key.proof.decproc.translation.IOperatorTranslation#isApplicable(de.uka.ilkd.key.logic.op.Operator)
143: */
144: public boolean isApplicable(Operator op) {
145: return op instanceof Function;
146: }
147:
148: /* (non-Javadoc)
149: * @see de.uka.ilkd.key.proof.decproc.translation.IOperatorTranslation#translate(de.uka.ilkd.key.logic.op.Operator, de.uka.ilkd.key.proof.decproc.translation.TermTranslationVisitor)
150: */
151: public Object translate(Operator op,
152: TermTranslationVisitor ttVisitor) {
153:
154: Object[] args;
155: Term[] convArgs;
156: String opName = op.name().toString();
157:
158: // First terms which are translated into interpreted functions
159: if (interpredFuncs.containsKey(opName)) {
160: logger.info("Found '" + opName
161: + "' function, starting operator translation...");
162: logger.debug("Popping " + op.arity()
163: + " argument terms from stack");
164: args = ttVisitor.getTranslatedArguments(op.arity());
165: convArgs = new Term[op.arity()];
166: for (int i = 0; i < op.arity(); i++) {
167: if (args[i] instanceof Term)
168: convArgs[i] = (Term) args[i];
169: else
170: throw new IllegalArgumentException(
171: translationFailure + op.name()
172: + failurerCauseNoTerm + args[i]);
173: }
174: // Non linear multiplication must be treated as uninterpreted function
175: if (opName == "mul"
176: && !(args[0] instanceof NumberConstantTerm || args[1] instanceof NumberConstantTerm)) {
177: Signature sig = Signature.intSignature(2, true);
178: logger
179: .info("Creating uninterpreted (nonlinear) multiply function");
180: String funcName = funcPrefix + "non_linear_mult"
181: + funcUifSuffix + funcIntSuffix;
182: ttVisitor.createTypePredUif(ttVisitor.getCurrentTerm()
183: .sort(), funcName, 2);
184: return new UninterpretedFuncTerm(funcName, convArgs,
185: sig);
186: }
187: String transOp = (String) interpredFuncs.get(opName);
188: logger.info("Creating '" + transOp + "' function");
189: return new InterpretedFuncTerm(transOp, convArgs);
190: }
191:
192: // Now the comparative predicates
193: if (compPreds.containsKey(opName)) {
194: logger
195: .info("Found predicate, starting operator translation...");
196: logger.debug("Popping 2 argument terms from stack");
197: args = ttVisitor.getTranslatedArguments(2);
198: if (args[0] instanceof Term && args[1] instanceof Term) {
199: convArgs = new Term[] { (Term) args[0], (Term) args[1] };
200: logger.info("Creating '" + opName + "' predicate");
201: return new PredicateFormula((String) compPreds
202: .get(opName), convArgs);
203: }
204: throw new IllegalArgumentException(errorMsg(args, opName));
205: }
206:
207: // Now the predicates for data type boundaries
208: if (typeBoundPreds.contains(opName)) {
209: logger
210: .info("Found predicate, starting operator translation...");
211: logger.debug("Popping 1 argument term from stack");
212: args = ttVisitor.getTranslatedArguments(1);
213: if (args[0] instanceof Term) {
214: logger.info("Found " + opName + " predicate");
215: Term[] minArgs, maxArgs;
216: BigInteger value;
217: Term minBoundValue, maxBoundValue;
218: // Parse opName to get the type (replace "in")
219: String typeName = opName.replaceFirst(typePredPrefix,
220: "").toLowerCase();
221: // Assemble type bound strings from parsing result and translate them into terms
222: value = new BigInteger(TypeBoundTranslation
223: .getTypeBoundValue(typeName
224: + typeBoundMinSuffix));
225: minBoundValue = getTermRepresentation(value);
226: value = new BigInteger(TypeBoundTranslation
227: .getTypeBoundValue(typeName
228: + typeBoundMaxSuffix));
229: maxBoundValue = getTermRepresentation(value);
230: minArgs = new Term[] { minBoundValue, (Term) args[0] };
231: maxArgs = new Term[] { (Term) args[0], maxBoundValue };
232: logger
233: .info("Creating two 'leq' predicates, connected by an 'and' connective");
234: PredicateFormula minConstraint = new PredicateFormula(
235: DecisionProcedureSmtAufliaOp.LEQ, minArgs);
236: PredicateFormula maxConstraint = new PredicateFormula(
237: DecisionProcedureSmtAufliaOp.LEQ, maxArgs);
238: Formula[] transParts = new Formula[] { minConstraint,
239: maxConstraint };
240: return new ConnectiveFormula(
241: DecisionProcedureSmtAufliaOp.AND, transParts);
242: }
243: throw new IllegalArgumentException();
244: }
245:
246: // Now the type boundaries theirselves
247: if (typeBounds.contains(opName)) {
248: logger.info("Found type boundary '" + opName
249: + "', creating number constant term");
250: BigInteger value = new BigInteger(TypeBoundTranslation
251: .getTypeBoundValue(opName));
252: return getTermRepresentation(value);
253: }
254:
255: // Now the boolean constants
256: if (opName.equals("TRUE") || opName.equals("FALSE")) {
257: logger
258: .info("Found '" + opName + "' function, "
259: + "creating '" + opName.toLowerCase()
260: + "' formula");
261: return TruthValueFormula.getInstance(opName.equals("TRUE"));
262: }
263:
264: // Now number and character constants
265:
266: if (opName.equals("#")) {
267: // Start translation of number constant
268: // Return zero to allow unique treatment of operator names representing digits
269: logger
270: .info("Found '#' function, starting number constant translation with BigInteger"
271: + "constant 0 ... ");
272: return BigInteger.ZERO;
273: }
274:
275: if (opName.length() == 1 && opName.charAt(0) >= '0'
276: && opName.charAt(0) <= '9') {
277: logger
278: .info("Found number constant, starting to process it...");
279: logger.debug("Popping 1 BigInteger from stack");
280: args = ttVisitor.getTranslatedArguments(1);
281: if (args[0] instanceof BigInteger) {
282: BigInteger value = ((BigInteger) args[0])
283: .multiply(getBigInt(10));
284: logger
285: .info("Creating BigInteger for calculated result");
286: return value.add(getBigInt(opName.charAt(0) - '0'));
287: }
288: throw new IllegalArgumentException(translationFailure
289: + op.name() + failureCauseNoBigInt + args[0]);
290: }
291:
292: if (opName.equals("neglit")) {
293: logger
294: .info("Found 'neglit' function, starting operator translation");
295: logger.debug("Popping 1 BigInteger from stack");
296: args = ttVisitor.getTranslatedArguments(1);
297: if (args[0] instanceof BigInteger) {
298: logger.info("Creating negated BigInteger");
299: return ((BigInteger) args[0]).negate();
300: }
301: throw new IllegalArgumentException(translationFailure
302: + op.name() + failureCauseNoBigInt + args[0]);
303: }
304:
305: if (opName.equals("Z") || opName.equals("C")) {
306: // These symbols indicate the end of the number/character constants
307: // They are treated in the same way, i.e. character constants also become integers
308: String constantType = opName.equals("Z") ? "number"
309: : "character";
310: logger.info("Found '" + opName + "' function,"
311: + " finalizing " + constantType
312: + " constant translation...");
313: logger.debug("Popping 1 BigInteger from stack");
314: args = ttVisitor.getTranslatedArguments(1);
315: if (args[0] instanceof BigInteger) {
316: // Create SMT-LIB representation for the parsed number/character constant
317: logger
318: .info("Creating term representation for processed "
319: + constantType + " constant");
320: return getTermRepresentation((BigInteger) args[0]);
321: }
322: throw new IllegalArgumentException(translationFailure
323: + op.name() + failureCauseNoBigInt + args[0]);
324: }
325:
326: // Last but not least all remaining function operaters are translated into uninterpreted
327: // predicates and functions respectively
328:
329: logger
330: .info("Found unknown function, starting function translation...");
331: logger.debug("Popping " + op.arity()
332: + " argument terms from stack");
333: args = ttVisitor.getTranslatedArguments(op.arity());
334: Sort integerSort = ttVisitor.getServices().getTypeConverter()
335: .getIntegerLDT().targetSort();
336: Sort booleanSort = ttVisitor.getServices().getTypeConverter()
337: .getBooleanLDT().targetSort();
338: Sort currentTermSort = ttVisitor.getCurrentTerm().sort();
339:
340: if (currentTermSort.extendsTrans(integerSort)
341: || currentTermSort instanceof ObjectSort
342: || currentTermSort == booleanSort
343: || currentTermSort == Sort.FORMULA) {
344: String generatedName = funcPrefix
345: + SmtAufliaTranslation.legaliseIdentifier(opName);
346: convArgs = new Term[op.arity()];
347: for (int i = 0; i < op.arity(); i++) {
348: if (args[i] instanceof Term)
349: convArgs[i] = (Term) args[i];
350: else
351: throw new IllegalArgumentException(
352: translationFailure + opName
353: + failurerCauseNoTerm + args[i]);
354: }
355: // Every operator of Sort int or object is translated into an uninterpreted function
356: if (currentTermSort.extendsTrans(integerSort)
357: || currentTermSort instanceof ObjectSort) {
358: generatedName += funcUifSuffix;
359: if (currentTermSort.extendsTrans(integerSort)) {
360: logger
361: .info("Function has integer sort, creating uninterpreted function");
362: generatedName += funcIntSuffix;
363: } else {
364: logger
365: .info("Function has object sort , creating uninterpreted function");
366: generatedName += funcObjectSuffix;
367: }
368: ttVisitor.createTypePredUif(currentTermSort,
369: generatedName, op.arity());
370: Signature uiSig = Signature.intSignature(op.arity(),
371: true);
372: return new UninterpretedFuncTerm(generatedName,
373: convArgs, uiSig);
374: }
375: // Operators of Sort FORMULA or boolean are translated into an uninterpreted predicate
376: logger.info("Function has sort '" + currentTermSort + "' ,"
377: + " creating uninterpreted predicate");
378: Signature uiSig = Signature.intSignature(op.arity(), false);
379: generatedName += funcUipSuffix;
380: return new UninterpretedPredFormula(generatedName,
381: convArgs, uiSig);
382: }
383:
384: // The given function is of an untranslatable sort!
385: logger
386: .info("Found unsupported function, exiting with exception!");
387: throw new UnsupportedOperationException(unsupportedFunction
388: + opName + unsupportedFunctionFailure + currentTermSort);
389: }
390:
391: /* Private helper methods */
392:
393: /** Returns a cached <tt>BigInteger</tt> instance representing the specified <tt>int</tt>
394: * @param number the value which the returned <tt>BigInteger</tt> should represent
395: * @return a cached <tt>BigInteger</tt> instance
396: *
397: * @throws IndexOutOfBoundsException if <tt>number</tt> is negative or greater than 10
398: */
399: private BigInteger getBigInt(int number) {
400: if (cachedBigInts[number] == null) {
401: cachedBigInts[number] = new BigInteger("" + number);
402: }
403: return cachedBigInts[number];
404: }
405:
406: /** Returns an SMT-LIB <tt>Term</tt> representing the given <tt>BigInteger</tt>
407: *
408: * @param value the number value to be represented in SMT-LIB syntax
409: * @return a <tt>NumberConstantTerm</tt> or an <tt>InterpretedFuncTerm</tt> ( if value < 0!)
410: * as representation of the given number value
411: */
412: private Term getTermRepresentation(BigInteger value) {
413: Term representation = NumberConstantTerm.getInstance(value
414: .abs());
415: if (value.signum() == -1) {
416: representation = new InterpretedFuncTerm(
417: DecisionProcedureSmtAufliaOp.UMINUS,
418: new Term[] { representation });
419: }
420: return representation;
421: }
422:
423: /** Helper function to generate specific error message
424: * @param args the <tt>Object</tt> array of arguments for the translation
425: * @param opName the name of the <tt>Function</tt> to be translated on which the error occured
426: * @return a <tt>String</tt> representing a specific error message
427: */
428: private String errorMsg(Object[] args, String opName) {
429: String errorMsg = translationFailure + opName
430: + failurerCauseNoTerm;
431: return errorMsg
432: + ((args[0] instanceof Term) ? args[1] : args[0]);
433: }
434: }
|