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: //This file is part of KeY - Integrated Deductive Software Design
009: //Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
010: // Universitaet Koblenz-Landau, Germany
011: // Chalmers University of Technology, Sweden
012: //
013: //The KeY system is protected by the GNU General Public License.
014: //See LICENSE.TXT for details.
015: //
016: //
017:
018: package de.uka.ilkd.key.proof.decproc.smtlib;
019:
020: import de.uka.ilkd.key.proof.decproc.DecisionProcedureSmtAufliaOp;
021:
022: /** Represents a 'flet'-construct formula as defined in the SMT-Lib specification,
023: * and specialized in the (QF_)AUFLIA sublogic.
024: * <p>
025: * Thereby a 'flet'-construct consists of a formula f1, a formula variable fVar and an arbitrary
026: * formula f0, and is semantically equivalent to the Formula obtained by replacing every free
027: * occurence of formVar in f1 by the Formula f0.
028: * <p>
029: * FletFormula are immutable; their values cannot be changed after they are created
030: *
031: * @author akuwertz
032: * @version 1.4, 12/12/2005 (Adjustments to superclass V1.5; further comments)
033: */
034:
035: public class FletFormula extends Formula {
036:
037: /* Additional fields */
038:
039: /** The <tt>Formula</tt> to which this <tt>FletFormula</tt> is semantically equivant */
040: private final Formula replacedFormula;
041:
042: /* String constants for failures during Formula creation */
043: private static final String creationFailureFormVarNull = "The formula variable is null!";
044: private static final String creationFailureFormulaf0Null = "The replacement formula f0 is null!";
045: private static final String creationFailureFormulaf1Null = "The formula f1 is null!";
046: private static final String creationFailureVarNotCont = "The formula variable must be contained in the formula f1!";
047:
048: /* Constructor */
049:
050: /** Creates a new <tt>FletFormula</tt> using the 'flet'-construct.
051: *
052: * @param fVar the <tt>FormulaVariable</tt> occuring in <tt>f1</tt> which is to be semantically replaced
053: * @param f0 the <tt>Formula</tt> which will semantically replace fVar in <tt>f1</tt>
054: * @param f1 the <tt>Formula</tt> in which fVar will be semantically replaced by <tt>f0</tt>
055: * @throws NullPointerException if one of the arguments is <tt>null</tt>
056: * @throws IllegalArgumentException if <tt>fVar</tt> is not contained in <tt>f1</tt>
057: */
058: public FletFormula(FormulaVariable fVar, Formula f0, Formula f1) {
059: super (DecisionProcedureSmtAufliaOp.FLET, new Formula[] { fVar,
060: f0, f1 }, null);
061:
062: // Check if a Constructor argument is null
063: if (fVar == null)
064: throw new NullPointerException(creationFailureFormVarNull);
065: if (f0 == null)
066: throw new NullPointerException(creationFailureFormulaf0Null);
067: if (f1 == null)
068: throw new NullPointerException(creationFailureFormulaf1Null);
069:
070: // Check if fVar is contained in f1
071: if (!f1.containsFormula(fVar))
072: throw new IllegalArgumentException(
073: creationFailureVarNotCont);
074:
075: replacedFormula = f1.replaceFormVar(fVar, f0);
076: }
077:
078: // Public method implementation
079:
080: /** Returns true if this <tt>FletFormula</tt> contains the <tt>Formula</tt> <tt>f</tt>.
081: * <p>
082: * In a 'flet'-construct, the formula obtained by replacing every free occurence of its
083: * <tt>FormulaVariable</tt> <tt>fVar<tt> in its <tt>Formula</tt> <tt>f1</tt> by its
084: * <tt>Formula</tt> <tt>f0</tt>, is checked for containing the specified <tt>Formula</tt>
085: * <tt>f</tt>.
086: *
087: * @param f the <tt>Formula</tt> be checked for containment in this <tt>FletFormula</tt>
088: * @return true if this <tt>FletFormula</tt> contains <tt>f</tt>
089: */
090: public boolean containsFormula(Formula f) {
091: return replacedFormula.containsFormula(f);
092: }
093:
094: /** Returns true if this <tt>FletFormula</tt> contains the <tt>Term</tt> <tt>t</tt>.
095: * In a 'flet'-construct, the formula obtained by replacing every free occurence of its
096: * <tt>FormulaVariable</tt> <tt>fVar</tt> in its <tt>Formula</tt> <tt>f1</tt> by its
097: * <tt>Formula</tt> <tt>f0</tt>, is checked for containing the specified <tt>Term</tt>
098: * <tt>t</tt>.
099: *
100: * @param t the <tt>Term</tt> be checked for containment in this <tt>FletFormula</tt>
101: * @return true if this <tt>FletFormula</tt> contains <tt>t</tt>
102: */
103: public boolean containsTerm(Term t) {
104: return replacedFormula.containsTerm(t);
105: }
106:
107: /* (non-Javadoc)
108: * @see Formula#equals(java.lang.Object)
109: */
110: public boolean equals(Object o) {
111: if (o == this )
112: return true;
113: if (super .equals(o)) {
114: return (o instanceof LetFormula);
115: }
116: return false;
117: }
118:
119: /* (non-Javadoc)
120: * @see Formula#hashCode()
121: */
122: public int hashCode() {
123: return super .hashCode();
124: }
125:
126: /* (non-Javadoc)
127: * @see de.uka.ilkd.key.proof.decproc.smtlib.Formula#toString()
128: */
129: public String toString() {
130: String representation = "(" + getOp();
131: representation += " (" + getSubformulae()[0] + " "
132: + getSubformulae()[1] + ") ";
133: representation += getSubformulae()[2] + ")";
134: return representation;
135: }
136:
137: /** Returns the formula variable of this <tt>FletFormula</tt>
138: *
139: * @return the <tt>FormulaVariable</tt> fVar of this <tt>FletFormula</tt>
140: */
141: public FormulaVariable getFormVar() {
142: return (FormulaVariable) getSubformulae()[0];
143: }
144:
145: /** Returns the <tt>Formula</tt> <tt>f0</tt> of this <tt>FletFormula</tt>
146: *
147: * @return the <tt>Formula</tt> <tt>f0</tt> of this <tt>FletFormula</tt>
148: */
149: public Formula getFormulaF0() {
150: return getSubformulae()[1];
151: }
152:
153: /** Returns the <tt>Formula</tt> <tt>f1</tt> of this <tt>FletFormula</tt>
154: *
155: * @return the <tt>Formula</tt> <tt>f1</tt> of this <tt>FletFormula</tt>
156: */
157: public Formula getFormulaF1() {
158: return getSubformulae()[2];
159: }
160:
161: /* (non-Javadoc)
162: * @see Formula#replaceFormVar(FormulaVariable, Formula)
163: */
164: public Formula replaceFormVar(FormulaVariable fVar,
165: Formula replacement) {
166: if (!containsFormula(fVar))
167: return this ;
168: return new FletFormula(getFormVar(), getFormulaF0()
169: .replaceFormVar(fVar, replacement), fVar
170: .equals(getFormVar()) ? getFormulaF1() : getFormulaF1()
171: .replaceFormVar(fVar, replacement));
172: }
173:
174: /* (non-Javadoc)
175: * @see Formula#replaceTermVar(TermVariable, Term)
176: */
177: public Formula replaceTermVar(TermVariable termVar, Term replacement) {
178: if (!containsTerm(termVar))
179: return this ;
180: return new FletFormula(getFormVar(), getFormulaF0()
181: .replaceTermVar(termVar, replacement), getFormulaF1()
182: .replaceTermVar(termVar, replacement));
183: }
184:
185: /** Returns true if the specified <tt>Formula</tt> <tt>f</tt> equals the <tt>Formula</tt> obtained
186: * from this <tt>FletFormula</tt> by replacing free occurence of its <tt>FormulaVariable</tt>
187: * <tt>fVar</tt> in its <tt>Formula</tt> <tt>f1</tt> by its <tt>Formula</tt> <tt>f0</tt>.
188: *
189: * @param f the <tt>Formula</tt> to be compared with the replaced <tt>Formula</tt> of
190: * this <tt>FletFormula</tt>
191: * @return true if the specified <tt>Formula</tt> equals the replaced <tt>Formula</tt>
192: * of this <tt>FletFormula</tt>
193: */
194: public boolean equalsReplacedForm(Formula f) {
195: return replacedFormula.equals(f);
196: }
197:
198: /** Returns the hash code of the <tt>Formula</tt> obtained from this <tt>FletFormula</tt> by
199: * replacing free occurence of its <tt>FormulaVariable</tt> <tt>fVar</tt> in its <tt>Formula</tt>
200: * <tt>f1</tt> by its <tt>Formula</tt> <tt>f0</tt>.
201: *
202: * @return the hash code of the replaced <tt>Formula</tt> of this <tt>FletFormula</tt>
203: */
204: public int hashCodeReplacedForm() {
205: return replacedFormula.hashCode();
206: }
207: }
|