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.IfThenElse;
016: import de.uka.ilkd.key.logic.op.Operator;
017: import de.uka.ilkd.key.proof.decproc.DecisionProcedureSmtAufliaOp;
018: import de.uka.ilkd.key.proof.decproc.smtlib.ConnectiveFormula;
019: import de.uka.ilkd.key.proof.decproc.smtlib.Formula;
020: import de.uka.ilkd.key.proof.decproc.smtlib.IteTerm;
021: import de.uka.ilkd.key.proof.decproc.smtlib.Term;
022:
023: /** This class represents the translation rule for the general <tt>IfThenElse</tt> operator.
024: * <p>
025: * An <tt>IfThenElse</tt> operator is translated into an SMT-LIB <tt>ConnectiveFormula</tt>,
026: * if it represents a choice between two <tt>Term</tt>s of <tt>Sort</tt> <tt>FORMULA</tt>. If it
027: * represents a choice between two <tt>Term</tt>s of integer <tt>Sort</tt>, it is translated into
028: * an SMT-LIB <tt>IteTerm</tt>.
029: *
030: * @author akuwertz
031: * @version 1.1, 02/16/2006 (Added logger support)
032: */
033:
034: public class TranslateIfThenElse implements IOperatorTranslation {
035:
036: /* Additional fields */
037:
038: /** A <tt>Logger</tt> for logging and debugging operator translation */
039: private static final Logger logger = Logger
040: .getLogger(TranslateIfThenElse.class.getName());
041: // Logger is created hierarchical to inherit configuration and behaviour from parent
042:
043: /* String constants for error messages */
044: private static final String translationFailure = "Translation of IfThenElse operator failed due to illegal arguments on visitor stack!";
045: private static final String failureCauseNoTerm = " Expected an argument of class Term (SMT-LIB) and found the object:\n";
046: private static final String failureCauseNoFormula = " Expected an argument of class Formula (SMT-LIB) and found the object:\n";
047:
048: /* Public method implementation*/
049:
050: /* (non-Javadoc)
051: * @see de.uka.ilkd.key.proof.decproc.translation.IOperatorTranslation#isApplicable(de.uka.ilkd.key.logic.op.Operator)
052: */
053: public boolean isApplicable(Operator op) {
054: return op instanceof IfThenElse;
055: }
056:
057: /* (non-Javadoc)
058: * @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)
059: */
060: public Object translate(Operator op,
061: TermTranslationVisitor ttVisitor) {
062: logger.debug("Popping 3 arguments from stack");
063: Object[] args = ttVisitor.getTranslatedArguments(3);
064: if (args[0] instanceof Formula) {
065: Formula condFormula = (Formula) args[0];
066: String errorMsg = translationFailure;
067: // Further translation depends on the class of the already translated arguments
068: if (args[1] instanceof Formula
069: && args[2] instanceof Formula) {
070: logger
071: .info("Found ifThenElse operator on formulae, creating 'ifthenelse' "
072: + "formula");
073: Formula[] convArgs = { condFormula, (Formula) args[1],
074: (Formula) args[2] };
075: return new ConnectiveFormula(
076: DecisionProcedureSmtAufliaOp.IFTHENELSE,
077: convArgs);
078: }
079: if (args[1] instanceof Term && args[2] instanceof Term) {
080: logger
081: .info("Found ifThenElse operator on terms, creating IteTerm");
082: return new IteTerm((Term) args[1], (Term) args[2],
083: condFormula);
084: }
085:
086: // Throw an appropriate error message:
087: // If one argument is of class Formula, throw an formula error
088: if (args[1] instanceof Formula
089: || args[2] instanceof Formula) {
090: errorMsg += failureCauseNoFormula
091: + (args[1] instanceof Formula ? args[2]
092: : args[1]);
093: throw new IllegalArgumentException(errorMsg);
094: }
095: // Else throw a Term error
096: errorMsg += failureCauseNoTerm
097: + (args[1] instanceof Term ? args[2] : args[1]);
098: throw new IllegalArgumentException(errorMsg);
099: }
100:
101: // First argument was not of class Formula
102: logger
103: .info("Found unsupported ifThenElse operator, exiting with exception!");
104: throw new UnsupportedOperationException(translationFailure
105: + failureCauseNoFormula + args[0]);
106: }
107: }
|