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 de.uka.ilkd.key.java.Services;
014: import de.uka.ilkd.key.logic.*;
015: import de.uka.ilkd.key.proof.ProofSaver;
016:
017: /**
018: * Instantiation of an if-formula that is a formula of an existing
019: * sequent.
020: */
021:
022: public class IfFormulaInstSeq implements IfFormulaInstantiation {
023:
024: /**
025: * Sequent and formula
026: */
027: private final Sequent seq;
028: private final boolean antec; // formula is in antecedent?
029: private final ConstrainedFormula cf;
030:
031: public IfFormulaInstSeq(Sequent p_seq, boolean antec,
032: ConstrainedFormula p_cf) {
033: seq = p_seq;
034: this .antec = antec;
035: cf = p_cf;
036: }
037:
038: public IfFormulaInstSeq(Sequent seq, int formulaNr) {
039: this (seq, seq.numberInAntec(formulaNr), seq
040: .getFormulabyNr(formulaNr));
041: }
042:
043: /**
044: * @return the cf this is pointing to
045: */
046: public ConstrainedFormula getConstrainedFormula() {
047: return cf;
048: }
049:
050: /**
051: * Create a list with all formulas of a given semisequent
052: */
053: private static ListOfIfFormulaInstantiation createListHelp(
054: Sequent p_s, boolean antec) {
055:
056: ListOfIfFormulaInstantiation res = SLListOfIfFormulaInstantiation.EMPTY_LIST;
057: IteratorOfConstrainedFormula it;
058: if (antec)
059: it = p_s.antecedent().iterator();
060: else
061: it = p_s.succedent().iterator();
062: while (it.hasNext()) {
063: res = res.prepend(new IfFormulaInstSeq(p_s, antec, it
064: .next()));
065: }
066:
067: return res;
068:
069: }
070:
071: public static ListOfIfFormulaInstantiation createList(Sequent p_s,
072: boolean antec) {
073: final Semisequent ss = antec ? p_s.antecedent() : p_s
074: .succedent();
075:
076: synchronized (cache) {
077: if ((antec ? cache.aKey : cache.sKey) != ss) {
078: final ListOfIfFormulaInstantiation val = createListHelp(
079: p_s, antec);
080: if (antec) {
081: cache.aKey = ss;
082: cache.aVal = val;
083: } else {
084: cache.sKey = ss;
085: cache.sVal = val;
086: }
087: }
088:
089: return antec ? cache.aVal : cache.sVal;
090: }
091: }
092:
093: public String toString() {
094: return toString(null);
095: }
096:
097: public String toString(Services services) {
098: return ProofSaver.printAnything(cf.formula(), services)
099: + (cf.constraint().isBottom() ? "" : "<<"
100: + cf.constraint());
101: }
102:
103: public boolean equals(Object p_obj) {
104: if (!(p_obj instanceof IfFormulaInstSeq)) {
105: return false;
106: }
107: return seq == ((IfFormulaInstSeq) p_obj).seq
108: && cf == ((IfFormulaInstSeq) p_obj).cf
109: && antec == ((IfFormulaInstSeq) p_obj).antec;
110: }
111:
112: public int hashCode() {
113: int result = 17;
114: result = 37 * result + seq.hashCode();
115: result = 37 * result + cf.hashCode();
116: result = 37 * result + (antec ? 0 : 1);
117: return result;
118: }
119:
120: public boolean inAntec() {
121: return antec;
122: }
123:
124: private PosInOccurrence pioCache = null;
125:
126: public PosInOccurrence toPosInOccurrence() {
127: if (pioCache == null)
128: pioCache = new PosInOccurrence(getConstrainedFormula(),
129: PosInTerm.TOP_LEVEL, inAntec());
130: return pioCache;
131: }
132:
133: // a simple cache for the results of the method <code>createList</code>
134: private static final class Cache {
135: public Semisequent aKey = null;
136: public ListOfIfFormulaInstantiation aVal = null;
137:
138: public Semisequent sKey = null;
139: public ListOfIfFormulaInstantiation sVal = null;
140: }
141:
142: private static final Cache cache = new Cache();
143: }
|