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.mgt;
012:
013: import de.uka.ilkd.key.logic.ClashFreeSubst;
014: import de.uka.ilkd.key.logic.Term;
015: import de.uka.ilkd.key.logic.TermFactory;
016: import de.uka.ilkd.key.logic.op.*;
017: import de.uka.ilkd.key.logic.sort.Sort;
018: import de.uka.ilkd.key.proof.MethodSpecTransformation;
019: import de.uka.ilkd.key.util.Debug;
020:
021: /**
022: * Pre-processor for <code>MethodSpecTransformation</code>.
023: * Pull out quantifiers from a formula, only leaving over subformulas of the
024: * shape <code>all x. f@pre(...) = t</code> (such subformulas are removed by
025: * <code>MethodSpecTransformation</code>).
026: */
027: public class QuantifierEliminator {
028:
029: private final static TermFactory tf = TermFactory.DEFAULT;
030:
031: private ListOfQuantifierPrefixEntry quantifiers;
032: private Term quantifierFreeFormula;
033:
034: private QuantifierEliminator subFormulas[];
035: private final Term formula;
036:
037: private ListOfQuantifierPrefixEntry createQuantifierList() {
038: ListOfQuantifierPrefixEntry list = SLListOfQuantifierPrefixEntry.EMPTY_LIST;
039: for (int i = 0; i != formula.arity(); ++i)
040: list = list.prepend(subFormulas[i].getQuantifiers());
041: return list;
042: }
043:
044: private Term createQuantifierFreeFormula() {
045: final Term[] subs = new Term[formula.arity()];
046: for (int i = 0; i != formula.arity(); ++i)
047: subs[i] = subFormulas[i].getQuantifierFreeFormula();
048:
049: return tf.createTerm(op(), subs, formula.varsBoundHere(0),
050: formula.javaBlock());
051: }
052:
053: public static QuantifierEliminator create(Term f) {
054: if (f.op() == Op.EQV) {
055: // handle equivalences by rewriting them using simpler junctors
056: // could be made more efficiently: check whether there are really
057: // bound variables within the formula
058: final Term s0 = f.sub(0);
059: final Term s1 = f.sub(1);
060: final Term ns0 = tf.createJunctorTerm(Op.NOT, s0);
061: final Term ns1 = tf.createJunctorTerm(Op.NOT, s1);
062: final Term simplerF = tf.createJunctorTerm(Op.OR, tf
063: .createJunctorTerm(Op.AND, s0, s1), tf
064: .createJunctorTerm(Op.AND, ns0, ns1));
065: return create(simplerF);
066: }
067:
068: return new QuantifierEliminator(f);
069: }
070:
071: private QuantifierEliminator(Term f) {
072: formula = f;
073:
074: if (formula.sort() != Sort.FORMULA) {
075: // it is assumed that no variables are bound within terms
076: quantifiers = SLListOfQuantifierPrefixEntry.EMPTY_LIST;
077: quantifierFreeFormula = formula;
078: return;
079: }
080:
081: subFormulas = new QuantifierEliminator[formula.arity()];
082: for (int i = 0; i != formula.arity(); ++i)
083: subFormulas[i] = QuantifierEliminator
084: .create(formula.sub(i));
085:
086: handleDifferentOps();
087:
088: // make some memory reclaimable
089: subFormulas = null;
090: }
091:
092: private void handleDifferentOps() {
093: if (opIs(Op.ALL) || opIs(Op.EX)) {
094: handleQuantifier();
095: } else if (opIs(Op.NOT)) {
096: quantifiers = QuantifierPrefixEntry.invert(subFormulas[0]
097: .getQuantifiers());
098: quantifierFreeFormula = createQuantifierFreeFormula();
099: } else if (opIs(Op.AND) || opIs(Op.OR) || opIs(Op.DIA)
100: || opIs(Op.BOX) || opIs(Op.TRUE) || opIs(Op.FALSE)
101: || op() instanceof Function || opIs(Op.EQUALS)) {
102: quantifiers = createQuantifierList();
103: quantifierFreeFormula = createQuantifierFreeFormula();
104: } else if (opIs(Op.IMP)) {
105: final ListOfQuantifierPrefixEntry firstList = QuantifierPrefixEntry
106: .invert(subFormulas[0].getQuantifiers());
107: quantifiers = firstList.prepend(subFormulas[1]
108: .getQuantifiers());
109: quantifierFreeFormula = createQuantifierFreeFormula();
110: } else {
111: Debug
112: .fail("QuantifierEliminator: Don't know what to do with "
113: + formula);
114: }
115: }
116:
117: private boolean opIs(Op op) {
118: return op() == op;
119: }
120:
121: private Operator op() {
122: return formula.op();
123: }
124:
125: private void handleQuantifier() {
126: if (MethodSpecTransformation.isAtPreDefinition(formula)) {
127: quantifiers = SLListOfQuantifierPrefixEntry.EMPTY_LIST;
128: quantifierFreeFormula = formula;
129: return;
130: }
131:
132: final QuantifiableVariable oriVar = formula.varsBoundHere(0)
133: .getQuantifiableVariable(0);
134: // defensively create a new variable
135: final LogicVariable newVar = new LogicVariable(oriVar.name(),
136: oriVar.sort());
137: final ClashFreeSubst subst = new ClashFreeSubst(oriVar, tf
138: .createVariableTerm(newVar));
139: quantifierFreeFormula = subst.apply(subFormulas[0]
140: .getQuantifierFreeFormula());
141:
142: final QuantifierPrefixEntry entry = new QuantifierPrefixEntry(
143: newVar, opIs(Op.ALL));
144: quantifiers = subFormulas[0].getQuantifiers().prepend(entry);
145: }
146:
147: /**
148: * @return Returns the quantifierFreeFormula.
149: */
150: public Term getQuantifierFreeFormula() {
151: return quantifierFreeFormula;
152: }
153:
154: /**
155: * @return Returns the quantifiers.
156: */
157: public ListOfQuantifierPrefixEntry getQuantifiers() {
158: return quantifiers;
159: }
160: }
|