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