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.rule;
012:
013: import java.util.HashSet;
014:
015: import de.uka.ilkd.key.logic.*;
016: import de.uka.ilkd.key.logic.op.QuantifiableVariable;
017:
018: /**
019: * The bound uniqueness checker ensures that schemavariables can be bound
020: * at most once in the <tt>\find</tt> and <tt>\assumes</tt> part of a taclet. The justification for this restriction is to
021: * prevent the user to write taclets that match only in very rare cases, e.g.
022: * <code>
023: * \assumes (==>\forall var; phi)
024: * \find (\forall var; phi ==>)
025: * </code>
026: * would nearly never match, as <tt>var</tt> would be required to match
027: * the same object.
028: */
029: public class BoundUniquenessChecker {
030:
031: private HashSet boundVars = new HashSet();
032: private ListOfTerm terms = SLListOfTerm.EMPTY_LIST;
033:
034: public BoundUniquenessChecker(Sequent seq) {
035: addAll(seq);
036: }
037:
038: public BoundUniquenessChecker(Term t, Sequent seq) {
039: addTerm(t);
040: addAll(seq);
041: }
042:
043: /**
044: * adds <tt>term</tt> to the list of terms to include in
045: * the uniqueness check
046: * @param term a Term
047: */
048: public void addTerm(Term term) {
049: terms = terms.prepend(term);
050: }
051:
052: /**
053: * adds all formulas in the sequent to the list of terms to
054: * include in the uniqueness check
055: * @param seq the Sequent with the formulas to add
056: */
057: public void addAll(Sequent seq) {
058: final IteratorOfConstrainedFormula it = seq.iterator();
059: while (it.hasNext()) {
060: terms = terms.prepend(it.next().formula());
061: }
062: }
063:
064: //recursive helper
065: private boolean correct(Term t) {
066: /* Note that a term can bound a variable in several
067: * subterms.
068: */
069: final HashSet localVars = new HashSet(10);
070:
071: for (int i = 0, ar = t.arity(); i < ar; i++) {
072: for (int j = 0, sz = t.varsBoundHere(i).size(); j < sz; j++) {
073: final QuantifiableVariable qv = t.varsBoundHere(i)
074: .getQuantifiableVariable(j);
075: if (boundVars.contains(qv)) {
076: return false;
077: } else {
078: localVars.add(qv);
079: }
080: }
081: }
082:
083: boundVars.addAll(localVars);
084:
085: for (int i = 0, ar = t.arity(); i < ar; ++i) {
086: if (!correct(t.sub(i))) {
087: return false;
088: }
089: }
090: return true;
091: }
092:
093: /**
094: * returns true if any variable is bound at most once in the
095: * given set of terms
096: */
097: public boolean correct() {
098: final IteratorOfTerm it = terms.iterator();
099: while (it.hasNext()) {
100: if (!correct(it.next())) {
101: return false;
102: }
103: }
104: return true;
105: }
106:
107: }
|