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.AttributeOp;
016: import de.uka.ilkd.key.logic.op.IProgramVariable;
017: import de.uka.ilkd.key.logic.op.Operator;
018: import de.uka.ilkd.key.logic.op.ProgramVariable;
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.SmtAufliaTranslation;
022: import de.uka.ilkd.key.proof.decproc.smtlib.*;
023:
024: /** This class represents the translation rule for <tt>AttributeOp</tt>s.
025: * <p>
026: * Thereby the attribute represented by the <tt>AttributeOp</tt> has to be a
027: * <tt>ProgramVariable</tt>. If this attribute is of <tt>Sort</tt> INT or OBJECT, it will be
028: * translated into an SMT-LIB <tt>UninterpretedFuncTerm</tt>. If it is of <tt>Sort</tt> FORMULA,
029: * it will be translated into an SMT-LIB <tt>UninterpretedPredFormula</tt>.
030: * <p>
031: * The name of the uninterpreted function or predicate respectively is created out of the name of
032: * the attribute and an id unique to the <tt>AttributeOp</tt> to be translated. It further consists
033: * of a prefix indicating that it is a translation of an <tt>AttributeOp</tt> and a suffix that
034: * allows to quickly distinguish functions from predicates
035: *
036: * @author akuwertz
037: * @version 1.5, 12/13/2006 (Minor fixes for AUFLIA support)
038: */
039:
040: public class TranslateAttributeOp implements IOperatorTranslation {
041:
042: /* Additional fields */
043:
044: /** A cache for already translated <tt>AttributeOp</tt> instances */
045: private final HashMap translatedAttrOps = new HashMap();
046:
047: /** A prefix used in the names of the uninterpreted functions and predicates respectively to
048: * indicate that they represent a translations of an <tt>AttributeOp</tt> */
049: private static final String attrOpPrefix = "AttrOp_";
050:
051: /** A suffix used in the name of the created uninterpreted function to indicate that it
052: * represents the translation of an integer attribute */
053: private static final String attrOpIntSuffix = "_int";
054: /** A suffix used in the name of the created uninterpreted function to indicate that it
055: * represents the translation of an object attribute */
056: private static final String attrOpObjectSuffix = "_object";
057:
058: /** A suffix used in the name of the created uninterpreted function to mark it as function */
059: private static final String attrOpUifSuffix = "_UIF";
060: /** A suffix used in the name of the created uninterpreted predicate to mark it as predicate */
061: private static final String attrOpUipSuffix = "_UIP";
062:
063: /** A <tt>Logger</tt> for logging and debugging operator translation */
064: private static final Logger logger = Logger
065: .getLogger(TranslateAttributeOp.class.getName());
066: // Logger is created hierarchical to inherit configuration and behaviour from parent
067:
068: /* String constants for error messages */
069: private static final String translationFailure = "Translation of attribute operator failed due to illegal arguments on visitor stack:\n";
070: private static final String failureCause = " expected an argument of class UninterpretedFuncTerm (SMT-LIB) and found the object:\n";
071: private static final String unsupportedAttributOp = "Translation of attribute op failed because its Sort could not be handled by this class: ";
072: private static final String unsupportedAttributeType = "Translation of attribute op failed because the type of its attribute could not be handled:\nS";
073:
074: /* Public method implementation */
075:
076: /* (non-Javadoc)
077: * @see de.uka.ilkd.key.proof.decproc.translation.IOperatorTranslation#isApplicable(de.uka.ilkd.key.logic.op.Operator)
078: */
079: public boolean isApplicable(Operator op) {
080: return op instanceof AttributeOp;
081: }
082:
083: /* (non-Javadoc)
084: * @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)
085: */
086: public Object translate(Operator op,
087: TermTranslationVisitor ttVisitor) {
088:
089: logger.debug("Popping 1 argument from stack");
090: Object[] args = ttVisitor.getTranslatedArguments(1);
091: Term[] convArgs;
092:
093: // Check if attribute is a ProgramVariable
094: IProgramVariable attribute = ((AttributeOp) op).attribute();
095: Sort attrOpSort;
096: if (attribute instanceof ProgramVariable) {
097: logger.debug("Operator is a program variable!");
098: attrOpSort = ((ProgramVariable) attribute).sort();
099: } else
100: throw new IllegalArgumentException(unsupportedAttributeType
101: + op.name() + " has type: " + attribute.getClass());
102:
103: Sort integerSort = ttVisitor.getServices().getTypeConverter()
104: .getIntegerLDT().targetSort();
105: Sort booleanSort = ttVisitor.getServices().getTypeConverter()
106: .getBooleanLDT().targetSort();
107: Signature uiSig;
108: String generatedFuncName;
109:
110: if (attrOpSort.extendsTrans(integerSort)
111: || attrOpSort == booleanSort
112: || attrOpSort instanceof ObjectSort) {
113: if (args[0] instanceof UninterpretedFuncTerm
114: || args[0] instanceof TermVariable) {
115:
116: // Add a unique ID to the name of the uninterpreted function/predicate
117: if (!translatedAttrOps.containsKey(op)) {
118: generatedFuncName = attrOpPrefix
119: + SmtAufliaTranslation
120: .legaliseIdentifier(attribute
121: .name().toString()) + "_"
122: + translatedAttrOps.size();
123: logger
124: .debug("Generated unique ID for attribute operator");
125: translatedAttrOps.put(op, generatedFuncName);
126: }
127: generatedFuncName = (String) translatedAttrOps.get(op);
128: logger.info("Found attribute operator: "
129: + generatedFuncName);
130: convArgs = new Term[] { (Term) args[0] };
131:
132: if (attrOpSort.extendsTrans(integerSort)
133: || attrOpSort instanceof ObjectSort) {
134: // Attribute operators of integer or object sort are translated into
135: // uninterpreted functions
136: generatedFuncName += attrOpUifSuffix;
137: if (attrOpSort.extendsTrans(integerSort)) {
138: generatedFuncName += attrOpIntSuffix;
139: logger
140: .info("Found integer attribute, creating uninterpreted function");
141: } else {
142: generatedFuncName += attrOpObjectSuffix;
143: logger
144: .info("Found object attribute, creating uninterpreted function");
145: }
146: uiSig = Signature.intSignature(1, true);
147: logger.debug("Function was given the name: "
148: + generatedFuncName);
149: ttVisitor.createTypePredUif(attrOpSort,
150: generatedFuncName, 1);
151: return new UninterpretedFuncTerm(generatedFuncName,
152: convArgs, uiSig);
153: }
154:
155: // Translate attribute operator into an uninterpreted predicate
156: generatedFuncName += attrOpUipSuffix;
157: uiSig = Signature.intSignature(1, false);
158: logger
159: .info("Found boolean attribute, creating uninterpreted predicate");
160: logger.debug("Predicate was given the name: "
161: + generatedFuncName);
162: return new UninterpretedPredFormula(generatedFuncName,
163: convArgs, uiSig);
164: }
165:
166: // Argument term popped from stack has wrong type!
167: throw new IllegalArgumentException(translationFailure
168: + op.name() + failureCause + args[0]);
169: }
170:
171: // The given attribute operator is of an untranslatable sort!
172: logger
173: .info("Found unsupported attribute operator, exiting with exception!");
174: throw new UnsupportedOperationException(unsupportedAttributOp
175: + op.name() + " Sort: " + attrOpSort);
176: }
177: }
|