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 org.apache.log4j.Logger;
014: import de.uka.ilkd.key.logic.op.ArrayOp;
015: import de.uka.ilkd.key.logic.op.Operator;
016: import de.uka.ilkd.key.logic.sort.ArraySort;
017: import de.uka.ilkd.key.logic.sort.ObjectSort;
018: import de.uka.ilkd.key.logic.sort.Sort;
019: import de.uka.ilkd.key.proof.decproc.smtlib.*;
020:
021: /** This class represents the translation rule for <tt>ArrayOp</tt>s.
022: * <p>
023: * Thereby the array access represented by the <tt>ArrayOp</tt> is translated into an SMT-LIB
024: * <tt>UninterpretedFuncTerm</tt>, if the array is of <tt>Sort</tt> INT or OBJECT. If it is of
025: * boolean <tt>Sort</tt>, it is translated into an SMT-LIB <tt>UninterpretedPredFormula</tt>.<br>
026: * The created functions or predicates consist of two arguments: their first argument represents the
027: * accessed array itself, and the second argument specifies the index to be accessed
028: * <p>
029: *
030: * @author akuwertz
031: * @version 1.3, 12/13/2006 (Minor fixes for AUFLIA support)
032: */
033:
034: public class TranslateArrayOp implements IOperatorTranslation {
035:
036: /* Additional fields */
037:
038: /** A prefix used in the names of the uninterpreted functions and predicates respectively to
039: * indicate that they represent a translation of an <tt>ArrayOp</tt> */
040: private static final String arrayOpPrefix = "Array";
041:
042: /** A suffix used in the name of the created uninterpreted function to mark it as function */
043: private static final String arrayOpUifSuffix = "_UIF";
044: /** A suffix used in the name of the created uninterpreted predicate to mark it as predicate */
045: private static final String arrayOpUipSuffix = "_UIP";
046:
047: /** A suffix used in the name of the created uninterpreted function to indicate that it
048: * represents the translation of an integer attribute */
049: private static final String arrayOpIntSuffix = "_int";
050:
051: /** A <tt>Logger</tt> for logging and debugging operator translation */
052: private static final Logger logger = Logger
053: .getLogger(TranslateArrayOp.class.getName());
054: // Logger is created hierarchical to inherit configuration and behaviour from parent
055:
056: /* String constants for error messages */
057: private static final String translationFailure = "Translation of array operator failed due to illegal arguments on visitor stack:\n";
058: private static final String failureCause = " expected an argument of class Term (SMT-LIB) and found the object:\n";
059: private static final String failureCauseNoFuncTerm = " expected an argument of class UninterpretedFuncTerm (SMT-LIB) and found the object:\n";
060: private static final String unsupportedArrayOp = "Translation of array op failed because its element sort could not be handled by this class: ";
061:
062: /* Public method implementation */
063:
064: /* (non-Javadoc)
065: * @see de.uka.ilkd.key.proof.decproc.translation.IOperatorTranslation#isApplicable(de.uka.ilkd.key.logic.op.Operator)
066: */
067: public boolean isApplicable(Operator op) {
068: return op instanceof ArrayOp;
069: }
070:
071: /* (non-Javadoc)
072: * @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)
073: */
074: public Object translate(Operator op,
075: TermTranslationVisitor ttVisitor) {
076:
077: logger.debug("Popping two argument terms from stack");
078: Object[] args = ttVisitor.getTranslatedArguments(2);
079: Term[] convArgs;
080:
081: Sort elementSort = ((ArraySort) ((ArrayOp) op).arraySort())
082: .elementSort();
083: Sort integerSort = ttVisitor.getServices().getTypeConverter()
084: .getIntegerLDT().targetSort();
085: Sort booleanSort = ttVisitor.getServices().getTypeConverter()
086: .getBooleanLDT().targetSort();
087: Signature uiSig;
088:
089: // The first argument represents the array itself
090: if (!(args[0] instanceof UninterpretedFuncTerm || args[0] instanceof TermVariable)) {
091: throw new IllegalArgumentException(translationFailure
092: + op.name() + failureCauseNoFuncTerm + args[0]);
093: }
094:
095: // The second argument represents the index of the accessed element
096: if (!(args[1] instanceof Term))
097: throw new IllegalArgumentException(translationFailure
098: + op.name() + failureCause + args[1]);
099:
100: convArgs = new Term[] { (Term) args[0], (Term) args[1] };
101:
102: // The integer array case:
103: if (elementSort.extendsTrans(integerSort)) {
104: logger
105: .info("Found integer array, creating uninterpreted function");
106: uiSig = Signature.intSignature(2, true);
107: String funcName = arrayOpPrefix + arrayOpUifSuffix
108: + arrayOpIntSuffix;
109: ttVisitor.createTypePredUif(elementSort, funcName, 2);
110: return new UninterpretedFuncTerm(funcName, convArgs, uiSig);
111: }
112:
113: // The object array case:
114: if (elementSort instanceof ObjectSort) {
115: logger
116: .info("Found object array, creating uninterpreted function");
117: uiSig = Signature.intSignature(2, true);
118: String funcName = arrayOpPrefix + arrayOpUifSuffix
119: + elementSort;
120: ttVisitor.createTypePredUif(elementSort, funcName, 2);
121: return new UninterpretedFuncTerm(funcName, convArgs, uiSig);
122: }
123:
124: // The boolean array case:
125: if (elementSort == booleanSort) {
126: logger
127: .info("Found boolean array, creating uninterpreted predicate");
128: uiSig = Signature.intSignature(2, false);
129: return new UninterpretedPredFormula(arrayOpPrefix
130: + arrayOpUipSuffix, convArgs, uiSig);
131: }
132:
133: // The given array is of an untranslatable sort!
134: logger
135: .info("Found unsupported array operator, exiting with exception!");
136: throw new UnsupportedOperationException(unsupportedArrayOp
137: + op.name() + " Sort: " + elementSort);
138: }
139: }
|