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: package de.uka.ilkd.key.proof.decproc.translation;
009:
010: import java.util.HashMap;
011: import org.apache.log4j.Logger;
012: import de.uka.ilkd.key.logic.op.LogicVariable;
013: import de.uka.ilkd.key.logic.op.Operator;
014: import de.uka.ilkd.key.logic.sort.ObjectSort;
015: import de.uka.ilkd.key.logic.sort.Sort;
016: import de.uka.ilkd.key.proof.decproc.SmtAufliaTranslation;
017: import de.uka.ilkd.key.proof.decproc.smtlib.Signature;
018: import de.uka.ilkd.key.proof.decproc.smtlib.TermVariable;
019:
020: /** This class represents the translation rule for <tt>LogicVariable</tt>s.
021: * <p>
022: * A <tt>LogicVariable</tt> is translated into a <tt>TermVariable</tt>, if it is of <tt>Sort</tt> INT or
023: * OBJECT.
024: * <p>
025: * The name of this <tt>TermVariable</tt> is created out of the variable name and an id unique to
026: * the <tt>LogicVariable</tt>. It further consists of a prefix indicating that it is a
027: * translation of a <tt>LogicVariable</tt> and a suffix that indicating the <tt>Sort</tt> of
028: * the translated <tt>LogicVariable</tt>
029: *
030: * @author akuwertz
031: * @version 1.0, 10/04/2006
032: *
033: */
034: public class TranslateLogicVariable implements IOperatorTranslation {
035:
036: /* Additional fields */
037:
038: /** A cache for already translated <tt>LogicVariable</tt> instances */
039: private final HashMap translatedLogicVars = new HashMap();
040:
041: /** A prefix used in the names of the created <tt>TermVariables</tt> to
042: * indicate that they represent a translations of an <tt>LogicVariable</tt> */
043: private static final String logicVarPrefix = "LogVar_";
044:
045: /** A suffix used in the name of the created <tt>TermVariables</tt> to indicate that it
046: * represents the translation of an integer <tt>ProgramVariable</tt> */
047: private static final String logicVarIntSuffix = "_int";
048: /** A suffix used in the name of the created <tt>TermVariables</tt> to indicate that it
049: * represents the translation of an object <tt>LogicVariable</tt> */
050: private static final String logicVarObjectSuffix = "_object";
051:
052: /** A <tt>Logger</tt> for logging and debugging operator translation */
053: private static final Logger logger = Logger
054: .getLogger(TranslateLogicVariable.class.getName());
055: // Logger is created hierarchical to inherit configuration and behaviour from parent
056:
057: /* String constants for error messages */
058: private static final String unsupportedLogicVar = "Translation of logic variable failed: ";
059: private static final String unsupportedLogicVarFailure = "\nCaused by unsupported Sort: ";
060:
061: /* Public method implementation */
062:
063: /* (non-Javadoc)
064: * @see de.uka.ilkd.key.proof.decproc.translation.IOperatorTranslation#isApplicable(de.uka.ilkd.key.logic.op.Operator)
065: */
066: public boolean isApplicable(Operator op) {
067: return op instanceof LogicVariable;
068: }
069:
070: /* (non-Javadoc)
071: * @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)
072: */
073: public Object translate(Operator op,
074: TermTranslationVisitor ttVisitor) {
075:
076: Sort integerSort = ttVisitor.getServices().getTypeConverter()
077: .getIntegerLDT().targetSort();
078: Sort currentSort = ((LogicVariable) op).sort();
079: String generatedName;
080:
081: // If the logic variable has already been translated, return cached translation
082: if (translatedLogicVars.containsKey(op)) {
083: logger
084: .info("Found a previously translated logic variable: "
085: + op.name());
086: logger
087: .info("Returning cached translation for this logic variable");
088: return translatedLogicVars.get(op);
089: }
090:
091: if (currentSort.extendsTrans(integerSort)
092: || currentSort instanceof ObjectSort) {
093: logger.info("Found logic variable: " + op.name());
094: // Add a unique ID to the name of the term variable
095: generatedName = logicVarPrefix
096: + SmtAufliaTranslation.legaliseIdentifier(op.name()
097: .toString()) + "_"
098: + translatedLogicVars.size();
099: Object translation;
100: if (currentSort.extendsTrans(integerSort)) {
101: generatedName += logicVarIntSuffix;
102: logger
103: .info("Found integer sort for this logic variable, creating "
104: + "term variable and caching it");
105: } else {
106: generatedName += logicVarObjectSuffix;
107: logger
108: .info("Found object sort for this logic variable, creating "
109: + "term variable and caching it");
110: }
111: logger.debug("Term variable was given the name: "
112: + generatedName);
113: translation = new TermVariable(generatedName, Signature
114: .constSignature(false));
115: translatedLogicVars.put(op, translation);
116:
117: return translation;
118: }
119:
120: // The given logic variable is of an untranslatable sort!
121: logger
122: .info("Found unsupported logic variable, exiting with exception!");
123: throw new UnsupportedOperationException(unsupportedLogicVar
124: + op.name() + unsupportedLogicVarFailure + currentSort);
125: }
126:
127: }
|