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:
015: import de.uka.ilkd.key.logic.op.Equality;
016: import de.uka.ilkd.key.logic.op.Operator;
017: import de.uka.ilkd.key.logic.op.Op;
018: import de.uka.ilkd.key.logic.sort.ObjectSort;
019: import de.uka.ilkd.key.logic.sort.Sort;
020: import de.uka.ilkd.key.proof.decproc.DecisionProcedureSmtAufliaOp;
021: import de.uka.ilkd.key.proof.decproc.smtlib.ConnectiveFormula;
022: import de.uka.ilkd.key.proof.decproc.smtlib.Formula;
023: import de.uka.ilkd.key.proof.decproc.smtlib.Term;
024: import de.uka.ilkd.key.proof.decproc.smtlib.PredicateFormula;
025:
026: /** This class represents the translation rule for an <tt>Equality</tt>.
027: * <p>
028: * Three different types of an <tt>Equality</tt> are currently translated:<br>
029: * If the target <tt>Sort</tt> of an <tt>Equality</tt> is <tt>FORMULA</tt>, it is translated
030: * into an SMT-LIB <tt>ConnectiveFormula</tt> as equivalence. The same happens for an <tt>Equality</tt>
031: * having a boolean target <tt>Sort</tt>.<br>
032: * If the target <tt>Sort</tt> is an integer or object <tt>Sort</tt>, it is translated into a
033: * <tt>PredicateFormula</tt> as equality
034: *
035: * @author akuwertz
036: * @version 1.2, 03/27/2006 (Added support for obejct sort)
037: */
038:
039: public class TranslateEquality implements IOperatorTranslation {
040:
041: /* Additional fields */
042:
043: /** A <tt>Logger</tt> for logging and debugging operator translation */
044: private static final Logger logger = Logger
045: .getLogger(TranslateEquality.class.getName());
046: // Logger is created hierarchical to inherit configuration and behaviour from parent
047:
048: /* String constants for error messages */
049: private static final String translationFailure = "Translation of Equality operator failed due to illegal arguments on visitor stack:\n";
050: private static final String failureCauseNoTerm = " expected an argument of class Term (SMT-LIB) and found the object:\n";
051: private static final String failureCauseNoFormula = " expected an argument of class Formula (SMT-LIB) and found the object:\n";
052: private static final String unsupportedEquality = "Translation of Equality failed!";
053: private static final String unsupportedSort = "\nCause: the sort of this equality is not supported: ";
054: private static final String unsupportedOperator = "\nCause: this equality operator is not supported!";
055: private static final String diffArgSorts = "\nCause: the arguments are of different sorts: ";
056:
057: /* Public method implementation*/
058:
059: /* (non-Javadoc)
060: * @see de.uka.ilkd.key.proof.decproc.translation.IOperatorTranslation#isApplicable(de.uka.ilkd.key.logic.op.Operator)
061: */
062: public boolean isApplicable(Operator op) {
063: return op instanceof Equality;
064: }
065:
066: /* (non-Javadoc)
067: * @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)
068: */
069: public Object translate(Operator op,
070: TermTranslationVisitor ttVisitor) {
071:
072: logger.debug("Popping 2 arguments from stack");
073: Object[] args = ttVisitor.getTranslatedArguments(2);
074:
075: if (op == Op.EQV) {
076: logger
077: .info("Found 'EQV' equality, starting operator translation...");
078:
079: // The FORMULA case: f1 <-> f2 will be translated into a ConnectiveFormula
080: if (args[0] instanceof Formula
081: && args[1] instanceof Formula) {
082: Formula[] convArgs = { (Formula) args[0],
083: (Formula) args[1] };
084: logger.info("Creating 'EQV' formula");
085: return new ConnectiveFormula(
086: DecisionProcedureSmtAufliaOp.EQV, convArgs);
087: }
088: String errorMsg = translationFailure + op.name()
089: + failureCauseNoFormula
090: + (args[0] instanceof Formula ? args[1] : args[0]);
091: throw new IllegalArgumentException(errorMsg);
092:
093: }
094:
095: if (op == Op.EQUALS) {
096: logger
097: .info("Found 'EQUALS' equality, starting operator translation...");
098:
099: // EQUALS represents the general equality, applicable on arbitrary KeY Terms
100: Sort subSortFirst = ttVisitor.getCurrentTerm().sub(0)
101: .sort();
102: Sort subSortSecond = ttVisitor.getCurrentTerm().sub(1)
103: .sort();
104: Sort integerSort = ttVisitor.getServices()
105: .getTypeConverter().getIntegerLDT().targetSort();
106: Sort booleanSort = ttVisitor.getServices()
107: .getTypeConverter().getBooleanLDT().targetSort();
108:
109: // First treat equality on integers
110: if (subSortFirst.extendsTrans(integerSort)
111: && subSortSecond.extendsTrans(integerSort)) {
112: if (args[0] instanceof Term && args[1] instanceof Term) {
113: Term[] convArgs = { (Term) args[0], (Term) args[1] };
114: logger
115: .info("Treating as integer equality, creating 'EQUALS' formula");
116: return new PredicateFormula(
117: DecisionProcedureSmtAufliaOp.EQUALS,
118: convArgs);
119: }
120: String errorMsg = translationFailure + op.name()
121: + failureCauseNoTerm
122: + (args[0] instanceof Term ? args[1] : args[0]);
123: throw new IllegalArgumentException(errorMsg);
124: }
125:
126: // Next treat equality on booleans: Create a new equivalence!
127: if (subSortFirst == booleanSort
128: && subSortSecond == booleanSort) {
129: if (args[0] instanceof Formula
130: && args[1] instanceof Formula) {
131: Formula[] convArgs = { (Formula) args[0],
132: (Formula) args[1] };
133: logger
134: .info("Treating as boolean equality, creating 'EQV' formula");
135: return new ConnectiveFormula(
136: DecisionProcedureSmtAufliaOp.EQV, convArgs);
137: }
138: String errorMsg = translationFailure
139: + op.name()
140: + failureCauseNoFormula
141: + (args[0] instanceof Formula ? args[1]
142: : args[0]);
143: throw new IllegalArgumentException(errorMsg);
144: }
145:
146: // Finally the equality on objects
147: if (isCompatibleObject(subSortFirst, subSortSecond)) {
148: if (args[0] instanceof Term && args[1] instanceof Term) {
149: Term[] convArgs = { (Term) args[0], (Term) args[1] };
150: logger
151: .info("Treating as object equality, creating 'EQUALS' formula");
152: return new PredicateFormula(
153: DecisionProcedureSmtAufliaOp.EQUALS,
154: convArgs);
155: }
156: String errorMsg = translationFailure + op.name()
157: + failureCauseNoTerm
158: + (args[0] instanceof Term ? args[1] : args[0]);
159: throw new IllegalArgumentException(errorMsg);
160: }
161:
162: logger
163: .info("Found unsupported equality, exiting with exception!");
164: // Arguments are of different sorts!
165: if (subSortFirst.extendsTrans(integerSort)
166: || subSortFirst == booleanSort
167: || subSortFirst instanceof ObjectSort) {
168: throw new UnsupportedOperationException(
169: unsupportedEquality + diffArgSorts
170: + subSortFirst + " <-> "
171: + subSortSecond);
172: }
173:
174: // Given equality is of an untranslatable sort!
175: throw new UnsupportedOperationException(unsupportedEquality
176: + op.name() + unsupportedSort + subSortFirst);
177: }
178:
179: // Other equality operators are not supported
180: logger
181: .info("Found unsupported equality operator, exiting with exception!");
182: throw new UnsupportedOperationException(unsupportedEquality
183: + op.name() + unsupportedOperator);
184: }
185:
186: /** Checks whether the <tt>Sort</tt>s of two objects are compatible to be used in an equality
187: * @param sortFirst the sort of the first object
188: * @param sortSecond the sort of the second object
189: * @return true iff both <tt>Sort</tt>s are instances of <tt>ObjectSort</tt> and if one
190: * <tt>Sort</tt> is a subsort of the other <tt>Sort</tt>
191: */
192: private boolean isCompatibleObject(Sort sortFirst, Sort sortSecond) {
193: return sortFirst instanceof ObjectSort
194: && sortSecond instanceof ObjectSort;
195: // TODO Further checks necessary?
196: }
197: }
|