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 java.util.Iterator;
014:
015: import de.uka.ilkd.key.logic.Term;
016: import de.uka.ilkd.key.logic.op.Op;
017: import de.uka.ilkd.key.logic.op.QuantifiableVariable;
018: import de.uka.ilkd.key.logic.op.Quantifier;
019: import de.uka.ilkd.key.logic.sort.Sort;
020: import de.uka.ilkd.key.util.Debug;
021:
022: /**
023: * Immutable class for representing information about the quantification of a
024: * formula. The quantifier in <code>all x:int. phi</code> is represented by an
025: * object <code>new QuantifierPrefixEntry(x, true)</code>
026: */
027: public class QuantifierPrefixEntry {
028: private final boolean universal;
029: private final QuantifiableVariable variable;
030:
031: public QuantifierPrefixEntry(final QuantifiableVariable variable,
032: final boolean universal) {
033: this .variable = variable;
034: this .universal = universal;
035: }
036:
037: public boolean isUniversal() {
038: return universal;
039: }
040:
041: public QuantifiableVariable getVariable() {
042: return variable;
043: }
044:
045: /**
046: * @return an entry in which universal and existential quantifiers are
047: * switched
048: */
049: public QuantifierPrefixEntry invert() {
050: return new QuantifierPrefixEntry(getVariable(), !isUniversal());
051: }
052:
053: public static ListOfQuantifierPrefixEntry invert(
054: ListOfQuantifierPrefixEntry list) {
055: if (list.isEmpty())
056: return list;
057:
058: return invert(list.tail()).prepend(list.head().invert());
059: }
060:
061: /**
062: * @return an entry object that represents the top-level quantifier of the
063: * given formula
064: *
065: * @pre t.sort() == Sort.FORMULA && t.op() instanceof Quantifier
066: */
067: public static QuantifierPrefixEntry createFor(Term t) {
068: Debug.assertTrue(t.sort() == Sort.FORMULA
069: && t.op() instanceof Quantifier);
070:
071: return new QuantifierPrefixEntry(t.varsBoundHere(0)
072: .getQuantifiableVariable(0), t.op() == Op.ALL);
073: }
074:
075: /**
076: * Represent the quantifier prefix of a formula as a list of prefix entries
077: *
078: * @pre t.sort() == Sort.FORMULA
079: */
080: public static ListOfQuantifierPrefixEntry extractPrefix(Term t) {
081: Debug.assertTrue(t.sort() == Sort.FORMULA);
082:
083: ListOfQuantifierPrefixEntry res = SLListOfQuantifierPrefixEntry.EMPTY_LIST;
084: while (t.op() instanceof Quantifier) {
085: res = res.append(QuantifierPrefixEntry.createFor(t));
086: t = t.sub(0);
087: }
088:
089: return res;
090: }
091:
092: /**
093: * Convert a sequence of <code>QuantifiableVariable</code>s to a prefix list
094: */
095: public static ListOfQuantifierPrefixEntry toUniversalList(
096: Iterator it) {
097: ListOfQuantifierPrefixEntry res = SLListOfQuantifierPrefixEntry.EMPTY_LIST;
098: while (it.hasNext()) {
099: final QuantifiableVariable var = (QuantifiableVariable) it
100: .next();
101: res = res.append(new QuantifierPrefixEntry(var, true));
102: }
103: return res;
104: }
105: }
|