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.util.HashMap;
014: import org.apache.log4j.Logger;
015: import de.uka.ilkd.key.logic.op.Operator;
016: import de.uka.ilkd.key.logic.op.ProgramVariable;
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.SmtAufliaTranslation;
020: import de.uka.ilkd.key.proof.decproc.smtlib.Signature;
021: import de.uka.ilkd.key.proof.decproc.smtlib.UninterpretedFuncTerm;
022: import de.uka.ilkd.key.proof.decproc.smtlib.UninterpretedPredFormula;
023:
024: /** This class represents the translation rule for <tt>ProgramVariable</tt>s.
025: * <p>
026: * A <tt>ProgramVariable</tt> is translated into a constant. If it is of <tt>Sort</tt> INT or
027: * OBJECT, it will be translated into an SMT-LIB <tt>UninterpretedFuncTerm</tt>. If it is of
028: * <tt>Sort</tt> BOOLEAN, it will be translated into an SMT-LIB <tt>UninterpretedPredFormula</tt>
029: * <p>
030: * The name of the uninterpreted function or predicate respectively is created out of the variable
031: * name and an id unique to the <tt>ProgramVariable</tt>. It further consists of a prefix
032: * indicating that this is a translation of an <tt>ProgramVariable</tt> and a suffix that allows to
033: * quickly distinguish functions from predicates and integer functions from object functions
034: *
035: * @author akuwertz
036: * @version 1.3, 03/28/2006 (Minor fixes)
037: */
038:
039: public class TranslateProgramVariable implements IOperatorTranslation {
040:
041: /* Additional fields */
042:
043: /** A cache for already translated <tt>ProgramVariable</tt> instances */
044: private final HashMap translatedProgVars = new HashMap();
045:
046: /** A prefix used in the names of the uninterpreted functions and predicates respectively to
047: * indicate that they represent a translations of an <tt>ProgramVariable</tt> */
048: private static final String progVarPrefix = "ProgVar_";
049:
050: /** A suffix used in the name of the created uninterpreted function to indicate that it
051: * represents the translation of an integer <tt>ProgramVariable</tt> */
052: private static final String progVarIntSuffix = "_int";
053: /** A suffix used in the name of the created uninterpreted function to indicate that it
054: * represents the translation of an object <tt>ProgramVariable</tt> */
055: private static final String progVarObjectSuffix = "_object";
056:
057: /** A suffix used in the name of the created uninterpreted function to mark it as function */
058: private static final String progVarUifSuffix = "_UIF";
059: /** A suffix used in the name of the created uninterpreted predicate to mark it as predicate */
060: private static final String progVarUipSuffix = "_UIP";
061:
062: /** A <tt>Logger</tt> for logging and debugging operator translation */
063: private static final Logger logger = Logger
064: .getLogger(TranslateProgramVariable.class.getName());
065: // Logger is created hierarchical to inherit configuration and behaviour from parent
066:
067: /* String constants for error messages */
068: private static final String unsupportedProgVar = "Translation of program variable failed: ";
069: private static final String unsupportedProgVarFailure = "\nCaused by unsupported Sort: ";
070:
071: /* Public method implementation */
072:
073: /* (non-Javadoc)
074: * @see de.uka.ilkd.key.proof.decproc.translation.IOperatorTranslation#isApplicable(de.uka.ilkd.key.logic.op.Operator)
075: */
076: public boolean isApplicable(Operator op) {
077: return op instanceof ProgramVariable;
078: }
079:
080: /* (non-Javadoc)
081: * @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)
082: */
083: public Object translate(Operator op,
084: TermTranslationVisitor ttVisitor) {
085:
086: Sort integerSort = ttVisitor.getServices().getTypeConverter()
087: .getIntegerLDT().targetSort();
088: Sort booleanSort = ttVisitor.getServices().getTypeConverter()
089: .getBooleanLDT().targetSort();
090: Sort currentSort = ((ProgramVariable) op).sort();
091: Signature uiSig;
092: String generatedConstName;
093:
094: // If the program variable has already been translated, return cached translation
095: if (translatedProgVars.containsKey(op)) {
096: logger
097: .info("Found a previously translated program variable: "
098: + op.name());
099: logger
100: .info("Returning cached translation for this program variable");
101: return translatedProgVars.get(op);
102: }
103:
104: if (currentSort.extendsTrans(integerSort)
105: || currentSort == booleanSort
106: || currentSort instanceof ObjectSort) {
107: logger.info("Found program variable: " + op.name());
108: // Add a unique ID to the name of the uninterpreted function/predicate
109: generatedConstName = progVarPrefix
110: + SmtAufliaTranslation.legaliseIdentifier(op.name()
111: .toString()) + "_"
112: + translatedProgVars.size();
113: Object translation;
114:
115: if (currentSort.extendsTrans(integerSort)
116: || currentSort instanceof ObjectSort) {
117: // Program variables of integer or object sort are translated into uninterpreted
118: // function constants
119: generatedConstName += progVarUifSuffix;
120: if (currentSort.extendsTrans(integerSort)) {
121: generatedConstName += progVarIntSuffix;
122: logger
123: .info("Found integer sort for this program variable, creating "
124: + "uninterpreted function and caching it");
125: } else {
126: generatedConstName += progVarObjectSuffix;
127: logger
128: .info("Found object sort for this program variable, creating "
129: + "uninterpreted function and caching it");
130: }
131: logger.debug("Function was given the name: "
132: + generatedConstName);
133: uiSig = Signature.constSignature(false);
134: ttVisitor.createTypePredUif(currentSort,
135: generatedConstName, 0);
136: translation = new UninterpretedFuncTerm(
137: generatedConstName, null, uiSig);
138: translatedProgVars.put(op, translation);
139:
140: } else {
141: // Program variables of boolean sort are translated into uninterpreted predicates
142: generatedConstName += progVarUipSuffix;
143: uiSig = Signature.intSignature(0, false);
144: logger
145: .info("Found boolean sort for this program variable, creating "
146: + "uninterpreted predicate and caching it");
147: logger.debug("Predicate was given the name: "
148: + generatedConstName);
149: translation = new UninterpretedPredFormula(
150: generatedConstName, null, uiSig);
151: translatedProgVars.put(op, translation);
152: }
153:
154: return translation;
155: }
156:
157: // The given program variable is of an untranslatable sort!
158: logger
159: .info("Found unsupported program variable, exiting with exception!");
160: throw new UnsupportedOperationException(unsupportedProgVar
161: + op.name() + unsupportedProgVarFailure + currentSort);
162: }
163: }
|