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 an if-then-else (ite) construct for terms as defined in the SMT-Lib
023: * specification, and specialized in the (QF_)AUFLIA sublogic. Thereby an ite-construct
024: * consists of a formula 'iteFormula' and two terms t1 and t2, and evaluates to one of
025: * this terms in dependence of the truth value of the formula.
026: * <p>
027: * IteTerms are immutable; their attribute values cannot be changed after they are created.
028: *
029: * @author akuwertz
030: * @version 1.4, 12/05/2005 (Adjustments to changes in superclass; further comments)
031: */
032:
033: public final class IteTerm extends Term {
034:
035: /* Additional fields */
036:
037: /** The <tt>Formula</tt> of this Term */
038: private final Formula iteFormula;
039:
040: /** A int to cache the hash code for this <tt>IteTerm</tt> */
041: private int cachedHashCode;
042:
043: // String constants for failures during Term creation
044: private static final String creationFailureT1Null = "Term t1 is null!";
045: private static final String creationFailureT2Null = "Term t2 is null!";
046: private static final String creationFailureFormula1Null = "Formula is null!";
047:
048: /* Constructor */
049:
050: /** Creates an new <tt>IteTerm</tt>.
051: * <p>
052: * An <tt>IteTerm</tt> consists of one <tt>Formula</tt> and two <tt>Term</tt>s. It is
053: * semantically equivalent to its first or second <tt>Term</tt> argument in dependence of
054: * the truth value of its <tt>Formula</tt>.
055: *
056: * @param t1 the <tt>Term</tt> into which this <tt>IteTerm</tt> results if its <tt>Formula</tt>
057: * is evaluated to true
058: * @param t2 the <tt>Term</tt> into which this <tt>IteTerm</tt> results if its <tt>Formula</tt>
059: * is evaluated to false
060: * @param iteForm the <tt>Formula</tt> to be evaluated
061: * @throws NullPointerException if one of the specified arguments is <tt>null</tt>
062: */
063: public IteTerm(Term t1, Term t2, Formula iteForm) {
064: super (DecisionProcedureSmtAufliaOp.ITE, new Term[] { t1, t2 },
065: iteForm != null ? iteForm.getUIF() : null,
066: iteForm != null ? iteForm.getUIPredicates() : null);
067: if (t1 == null)
068: throw new NullPointerException(creationFailureT1Null);
069: if (t2 == null)
070: throw new NullPointerException(creationFailureT2Null);
071: if (iteForm == null)
072: throw new NullPointerException(creationFailureFormula1Null);
073: iteFormula = iteForm;
074: }
075:
076: // Public method implementations
077:
078: /* (non-Javadoc)
079: * @see de.uka.ilkd.key.proof.decproc.smtlib.Term#containsTerm(de.uka.ilkd.key.proof.decproc.smtlib.Term)
080: */
081: public boolean containsTerm(Term t) {
082: if (super .containsTerm(t))
083: return true;
084: return iteFormula.containsTerm(t);
085: }
086:
087: /** Returns true if this <tt>IteTerm</tt> contains the specified <tt>Term</tt> t as a subterm
088: * of one of its <tt>Term</tt> arguments, i.e. if t is contained in t1 or t2. In contrast to
089: * <tt>containsTerm</tt>, the iteFormula is not checked for containment of t.
090: *
091: * @param t the <tt>Term</tt> to be checked for containment in this <tt>IteTerm</tt>
092: * @return true if t is contained in of one the subterms of this <tt>IteTernm</tt>
093: */
094: public boolean containsTermAsSubterm(Term t) {
095: Term[] this FuncArgs = getFuncArgs();
096: for (int i = 0; i < this FuncArgs.length; i++) {
097: if (this FuncArgs[i].containsTerm(t))
098: return true;
099: }
100: return false;
101: }
102:
103: /** Returns true if this <tt>IteTerm</tt> contains the specified <tt>Formula</tt> f
104: * in its ite-formula
105: *
106: * @param f the <tt>Formula</tt> to be checked for containment in this <tt>IteTerm</tt>
107: * @return true if this <tt>IteTerm</tt> contains the <tt>Formula</tt> f.
108: */
109: public boolean containsFormulaIteTerm(Formula f) {
110: if (super .containsFormulaIteTerm(f))
111: return true;
112: return iteFormula.containsFormula(f);
113: }
114:
115: /* (non-Javadoc)
116: * @see de.uka.ilkd.key.proof.decproc.smtlib.Term#equals(de.uka.ilkd.key.proof.decproc.smtlib.Term)
117: */
118: public boolean equals(Object o) {
119: if (this == o)
120: return true;
121: if (super .equals(o)) {
122: if (o instanceof IteTerm) {
123: IteTerm t = (IteTerm) o;
124: return iteFormula.equals(t.getIteFormula());
125: }
126: }
127: return false;
128: }
129:
130: /* (non-Javadoc)
131: * @see de.uka.ilkd.key.proof.decproc.smtlib.Term#hashCode()
132: */
133: public int hashCode() {
134: if (cachedHashCode == 0) {
135: cachedHashCode = 37 * super .hashCode()
136: + iteFormula.hashCode();
137: }
138: return cachedHashCode;
139: }
140:
141: /* (non-Javadoc)
142: * @see de.uka.ilkd.key.proof.decproc.smtlib.Term#toString()
143: */
144: public String toString() {
145: String representation = "(" + getFunction();
146: representation += " " + iteFormula.toString() + " ";
147: representation += getFuncArgs()[0].toString() + " "
148: + getFuncArgs()[1].toString();
149: representation += ")";
150: return representation;
151: }
152:
153: /** Returns the Formula of this <tt>IteTerm</tt>.
154: *
155: * @return the Formula of this <tt>IteTerm</tt>
156: */
157: public Formula getIteFormula() {
158: return iteFormula;
159: }
160:
161: /** Returns the <tt>Term</tt> t1 of this <tt>IteTerm</tt>
162: *
163: * @return the <tt>Term</tt> t1 of this <tt>IteTerm</tt>
164: */
165: public Term getTermT1() {
166: return getFuncArgs()[0];
167: }
168:
169: /** Returns the <tt>Term</tt> t2 of this <tt>IteTerm</tt>
170: *
171: * @return the <tt>Term</tt> t2 of this <tt>IteTerm</tt>
172: */
173: public Term getTermT2() {
174: return getFuncArgs()[1];
175: }
176:
177: /* (non-Javadoc)
178: * @see de.uka.ilkd.key.proof.decproc.smtlib.Term#replaceTermVar(de.uka.ilkd.key.proof.decproc.smtlib.TermVariable, de.uka.ilkd.key.proof.decproc.smtlib.Term)
179: */
180: public Term replaceTermVar(TermVariable termVar, Term replacement) {
181: if (!containsTerm(termVar))
182: return this ;
183: Term[] this FuncArgs = getFuncArgs();
184: return new IteTerm(this FuncArgs[0].replaceTermVar(termVar,
185: replacement), this FuncArgs[1].replaceTermVar(termVar,
186: replacement), iteFormula.replaceTermVar(termVar,
187: replacement));
188: }
189:
190: /** Replaces all occurrences of a specified <tt>FormulaVariable</tt> by a specified
191: * <tt>Formula</tt> in the iteFormula of this <tt>IteTerm</tt>.
192: * Thereby this <tt>IteTerm</tt> and the returned replaced <tt>Term</tt> share the
193: * same objects in their fields, except for those objects which contained the
194: * specified <tt>FormulaVariable</tt>
195: *
196: * @param formVar the <tt>FormulaVariable</tt> to be replaced
197: * @param replacement the <tt>Formula</tt> used to replace <tt>formVar</tt>
198: * @return the <tt>Formula</tt> obtained by replacing every (free) occurence of <tt>formVar</tt>
199: * by <tt>replacement</tt> in the iteFormula of this <tt>IteTerm</tt>
200: */
201: public Term replaceFormVarIteTerm(FormulaVariable formVar,
202: Formula replacement) {
203: if (!containsFormulaIteTerm(formVar))
204: return this ;
205: Term[] this FuncArgs = getFuncArgs();
206: return new IteTerm(this FuncArgs[0].replaceFormVarIteTerm(
207: formVar, replacement), this FuncArgs[1]
208: .replaceFormVarIteTerm(formVar, replacement),
209: iteFormula.replaceFormVar(formVar, replacement));
210: }
211: }
|