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.Junctor;
016: import de.uka.ilkd.key.logic.op.Operator;
017: import de.uka.ilkd.key.logic.op.Op;
018: import de.uka.ilkd.key.proof.decproc.DecisionProcedureSmtAufliaOp;
019: import de.uka.ilkd.key.proof.decproc.smtlib.ConnectiveFormula;
020: import de.uka.ilkd.key.proof.decproc.smtlib.Formula;
021: import de.uka.ilkd.key.proof.decproc.smtlib.TruthValueFormula;
022:
023: /** This class represents the translation rule for <tt>Junctor</tt>s.
024: * <p>
025: * The following <tt>Junctor</tt> instances are translated currently:<ul>
026: * <li>NOT</li> <li>AND</li>
027: * <li>OR</li> <li>IMP</li>
028: * <li>TRUE</li> <li>FALSE</li></ul>
029: * <p>
030: * Each of the first four <tt>Junctor</tt>s mentioned above is translated into a corresponding
031: * SMT-LIB <tt>ConnectiveFormula</tt>. The last two are translated into a corresponding
032: * <tt>TruthValueFormula</tt>
033: *
034: * @author akuwertz
035: * @version 1.1, 02/15/2006 (Added logger support)
036: */
037:
038: public class TranslateJunctor implements IOperatorTranslation {
039:
040: /* Additional fields */
041:
042: /** A <tt>Logger</tt> for logging and debugging operator translation */
043: private static final Logger logger = Logger
044: .getLogger(TranslateJunctor.class.getName());
045: // Logger is created hierarchical to inherit configuration and behaviour from parent
046:
047: /* String constants for error messages */
048: private static final String translationFailure = "Translation of junctor failed due to illegal arguments on visitor stack:\n";
049: private static final String failureCauseNoFormula = " expected an argument of class (SMT-LIB) Formula and found the object:\n";
050: private static final String unsupportedJunctor = "Translation of junctor failed because this junctor is not supported by this class: ";
051:
052: /* Public method implementation*/
053:
054: /* (non-Javadoc)
055: * @see de.uka.ilkd.key.proof.decproc.translation.IOperatorTranslation#isApplicable(de.uka.ilkd.key.logic.op.Operator)
056: */
057: public boolean isApplicable(Operator op) {
058: return op instanceof Junctor;
059: }
060:
061: /* (non-Javadoc)
062: * @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)
063: */
064: public Object translate(Operator op,
065: TermTranslationVisitor ttVisitor) {
066:
067: if (op == Op.TRUE) {
068: logger
069: .info("Found 'TRUE' junctor, creating 'true' formula");
070: return TruthValueFormula.getInstance(true);
071: }
072: if (op == Op.FALSE) {
073: logger
074: .info("Found 'FALSE' junctor, creating 'false' formula");
075: return TruthValueFormula.getInstance(false);
076: }
077:
078: // Temporal variables for operators of positive arity
079: Object[] args;
080: Formula[] convArgs;
081:
082: if (op == Op.NOT) {
083: logger
084: .info("Found 'NOT' junctor, starting operator translation...");
085: logger.debug("Popping 1 argument formula from stack");
086: args = ttVisitor.getTranslatedArguments(1);
087: if (args[0] instanceof Formula) {
088: convArgs = new Formula[] { (Formula) args[0] };
089: logger.info("Creating 'NOT' formula");
090: return new ConnectiveFormula(
091: DecisionProcedureSmtAufliaOp.NOT, convArgs);
092: }
093: throw new IllegalArgumentException(translationFailure
094: + op.name() + failureCauseNoFormula + args[0]);
095: }
096:
097: // Operators of arity 2
098: if (op == Op.AND || op == Op.OR || op == Op.IMP) {
099: logger.debug("Popping 2 argument formulae from stack");
100: args = ttVisitor.getTranslatedArguments(2);
101: if (args[0] instanceof Formula
102: && args[1] instanceof Formula) {
103: convArgs = new Formula[] { (Formula) args[0],
104: (Formula) args[1] };
105: if (op == Op.AND) {
106: logger
107: .info("Found 'AND' junctor, creating 'AND' formula");
108: return new ConnectiveFormula(
109: DecisionProcedureSmtAufliaOp.AND, convArgs);
110: }
111: if (op == Op.OR) {
112: logger
113: .info("Found 'OR' junctor, creating 'OR' formula");
114: return new ConnectiveFormula(
115: DecisionProcedureSmtAufliaOp.OR, convArgs);
116: }
117: logger
118: .info("Found 'IMP' junctor, creating 'IMP' formula");
119: return new ConnectiveFormula(
120: DecisionProcedureSmtAufliaOp.IMP, convArgs);
121: }
122: String errorMsg = translationFailure + op.name()
123: + failureCauseNoFormula;
124: errorMsg += args[0] instanceof Formula ? args[1] : args[0];
125: throw new IllegalArgumentException(errorMsg);
126: }
127:
128: // Unsupported junctor
129: logger
130: .info("Found unsupported junctor, exiting with exception!");
131: throw new UnsupportedOperationException(unsupportedJunctor
132: + op.name());
133: }
134: }
|