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.*;
016: import de.uka.ilkd.key.proof.decproc.DecisionProcedureSmtAufliaOp;
017: import de.uka.ilkd.key.proof.decproc.smtlib.ConnectiveFormula;
018: import de.uka.ilkd.key.proof.decproc.smtlib.Formula;
019: import de.uka.ilkd.key.proof.decproc.smtlib.QuantifierFormula;
020: import de.uka.ilkd.key.proof.decproc.smtlib.TermVariable;
021:
022: /** This class represents the translation rule for <tt>Quantifier</tt>s.<br>
023: * They are supported only in AUFLIA, not in QF_AUFLIA.
024: * <p>
025: * A <tt>Quantifier</tt> is translated into a <tt>QuantifierFormula</tt>, if it is an ALL or
026: * an EXISTS quantifier. Thereby, its bound variables will also be translated
027: *
028: * @author akuwertz
029: * @version 1.2, 11/09/2006 (Added type predicates for quantified variables)
030: */
031:
032: public class TranslateQuantifier implements IOperatorTranslation {
033:
034: /* Additional fields */
035:
036: /** A <tt>Logger</tt> for logging and debugging operator translation */
037: private static final Logger logger = Logger
038: .getLogger(TranslateQuantifier.class.getName());
039: // Logger is created hierarchical to inherit configuration and behaviour from parent
040:
041: /* String constants for error messages */
042: private static final String translationFailure = "Translation of quantifier failed due to illegal arguments on visitor stack:\n";
043: private static final String failureCauseNoFormula = " expected an argument of class Formula (SMT-LIB) and found the object:\n";
044: private static final String unsupportedQuantifier = "Translation of quantifier failed!";
045: private static final String unsupportedOperator = "\nCause: this quantifier operator is not supported!";
046: private static final String unsupportedVar = "\nCause: the quantified variable cound not be translated: ";
047: private static final String varTransFailed = "\nThe following exception was thrown during variable translation: \n";
048:
049: /* Public methods */
050:
051: /* (non-Javadoc)
052: * @see de.uka.ilkd.key.proof.decproc.translation.IOperatorTranslation#isApplicable(de.uka.ilkd.key.logic.op.Operator)
053: */
054: public boolean isApplicable(Operator op) {
055: return op instanceof Quantifier;
056: }
057:
058: /* (non-Javadoc)
059: * @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)
060: */
061: public Object translate(Operator op,
062: TermTranslationVisitor ttVisitor) {
063:
064: if (op == Op.ALL || op == Op.EX) {
065: String opName = op == Op.ALL ? DecisionProcedureSmtAufliaOp.FORALL
066: : DecisionProcedureSmtAufliaOp.EXISTS;
067: logger.info("Found '" + opName
068: + "' quantifier, starting operator translation...");
069: logger.debug("Popping one argument term from stack");
070:
071: Object arg = ttVisitor.getTranslatedArguments(1)[0];
072: Formula form;
073: if (arg instanceof Formula)
074: form = (Formula) arg;
075: else
076: throw new IllegalArgumentException(translationFailure
077: + opName + failureCauseNoFormula + arg);
078:
079: ArrayOfQuantifiableVariable boundVars = ttVisitor
080: .getCurrentTerm().varsBoundHere(0);
081: logger
082: .info("Found "
083: + boundVars.size()
084: + " quantifiable variables, trying to create new term variables...");
085: TermVariable[] quantVars = new TermVariable[boundVars
086: .size()];
087: Formula[] typePreds = new Formula[boundVars.size()];
088: for (int i = 0; i < quantVars.length; i++) {
089: QuantifiableVariable var = boundVars
090: .getQuantifiableVariable(i);
091: // Give the quantifiable variable to the ttVisitor!
092: try {
093: quantVars[i] = ttVisitor
094: .translateLvManually((LogicVariable) var);
095: // ClassCastExceptions will also be catched!
096: } catch (RuntimeException e) {
097: // Pass on the exception after adding some quantifier specific information
098: throw new UnsupportedOperationException(
099: unsupportedQuantifier + op.name()
100: + unsupportedVar + var
101: + varTransFailed + e);
102: }
103: // Create type predicate for quantifiable variable
104: typePreds[i] = ttVisitor.createTypePredLv(var.sort(),
105: quantVars[i]);
106: }
107: logger.info("Creating new quantifier formula!");
108: // Integrate type predicates and quantified formula
109: Formula preconditions = typePreds[0];
110: Formula[] helper;
111: for (int i = 1; i < typePreds.length; i++) { // typePreds.length > 0!
112: helper = new Formula[] { preconditions, typePreds[i] };
113: preconditions = new ConnectiveFormula(
114: DecisionProcedureSmtAufliaOp.AND, helper);
115: }
116: helper = new Formula[] { preconditions, form };
117: if (op == Op.ALL) {
118: form = new ConnectiveFormula(
119: DecisionProcedureSmtAufliaOp.IMP, helper);
120: } else { // op == Op.EX
121: form = new ConnectiveFormula(
122: DecisionProcedureSmtAufliaOp.AND, helper);
123: }
124: return new QuantifierFormula(opName, quantVars, form);
125: }
126:
127: // Other quantifier operators are not supported
128: logger
129: .info("Found unsupported quantifier operator, exiting with exception!");
130: throw new UnsupportedOperationException(unsupportedQuantifier
131: + ((Quantifier) op).name() + unsupportedOperator);
132: }
133:
134: }
|