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 java.util.Vector;
021:
022: import de.uka.ilkd.key.proof.decproc.DecisionProcedureSmtAufliaOp;
023:
024: /** Represents an interpreted function as defined in the SMT-Lib specification,
025: * and specialized in the (QF_)AUFLIA sublogic. In (QF_)AUFLIA, only + , - , unary
026: * minus, * , 'select' (array) and 'store' (array) are interpreted functions.
027: * <p>
028: * InterpretedFuncTerms are immutable; their attribute values cannot be changed after they
029: * are created.
030: *
031: * @author akuwertz
032: * @version 1.4, 12/04/2005 (Adjustments to changes in superclass; added further comments)
033: */
034:
035: public final class InterpretedFuncTerm extends Term {
036:
037: /* Additional fields */
038:
039: /** A int used to cache the hash code of this <tt>InterpretedFuncTerm</tt> if it represents a
040: * commutative function */
041: private int cachedCommHashCode;
042:
043: /* String constants for failures during Term creation */
044: private static final String creationFailurefNameNull = "Function name is null!";
045: private static final String creationFailurefArgsNull = "Function argument array is null!";
046: private static final String creationFailurefArgsContNull = "Function argument array contains a null pointer at position ";
047: private static final String creationFailureArity = "Argument count does not match function arity!";
048: private static final String creationFailureArgType = "Argument types don't match function signature!";
049: private static final String creationFailureUninterpreted = "Operator is not an interpreted one!";
050: private static final String creationFailureArray = "First function argument must be of type 'array'!";
051: private static final String creationFailureInt = "Second and third function arguments must be of type 'int'!";
052: private static final String creationFailureIntArb = "Function arguments must be of type 'int'!";
053:
054: /* Constructor */
055:
056: /** Creates a new <tt>InterpretedFuncTerm</tt>, representing an interpreted function as
057: * defined in (QF_)AUFLIA.
058: * <p>
059: * Which interpreted function is to be represented, is specified solely by the function name.
060: * Therefore, only certain <tt>String</tt> values are accepted as interpreted functions in
061: * (QF_)AUFLIA; they are defined as static fields in <tt>DecisionProcedureSmtAufliaOp</tt>.
062: * Namely, this are PLUS, MINUS, UMINUS, MULT, SELECT and STORE.
063: * <p>
064: * In (QF_)AUFLIA, there are two interpreted sorts, INT and ARRAY. For the mentioned interpreted
065: * functions the following signatures hold:<br>
066: * UMINUS: INT->INT<br>
067: * MINUS: INT->INT->INT<br>
068: * PLUS: INT->INT->INT<br>
069: * MULT: INT->INT->INT<br>
070: * SELECT: ARRAY->INT->INT<br>
071: * STORE: ARRAY->INT->INT->ARRAY<br>
072: * For convenience, the PLUS function allows also more than two arguments. The MULT function
073: * requests of one its arguments to be a natural number constant.<br>
074: * The sort of a <tt>Term</tt> depends on its class:
075: * A <tt>NumberConstantTerm</tt>is of sort Int, a <tt>Termvariable</tt>s of arbitrary sort.
076: * For an <tt>InterpretedFuncTerm</tt> or an <tt>UninterpretedFuncTerm</tt> the sort is
077: * determined by their signature. An <tt>IteTerm</tt> is of same sort as its argument
078: * <tt>Term</tt>s.
079: * <p>
080: * If any of these conditions does not hold for the <tt>InterpretedFuncTerm</tt> to created,
081: * an <tt>IllegalArgumentException</tt> is thrown.
082: *
083: * @param fName the name of the interpreted function to be represented
084: * @param fArgs the array of function arguments;
085: * @throws NullPointerException if <tt>fName</tt> or <tt>fArgs </tt>is <tt>null</tt> or if
086: * <tt>fArgs</tt> contains a null pointer
087: * @throws IllegalArgumentException if <tt>fName</tt> is no interpreted function symbol in
088: * QF_AULIA or if the number of function arguments doesn't
089: * match the function arity or if the sort of a function
090: * argument doesn't match the expected sort
091: * @see de.uka.ilkd.key.logic.op.DecisionProcedureSmtAufliaOp
092: */
093: public InterpretedFuncTerm(String fName, Term[] fArgs) {
094: super (fName, fArgs, null, null);
095:
096: if (fName == null)
097: throw new NullPointerException(creationFailurefNameNull);
098: if (fArgs == null)
099: throw new NullPointerException(creationFailurefArgsNull);
100: for (int i = 0; i < fArgs.length; i++) {
101: if (fArgs[i] == null)
102: throw new NullPointerException(
103: creationFailurefArgsContNull + i);
104: }
105: // Find out if the function fName is interpreted, and if so, check the arguments
106: if (fName == DecisionProcedureSmtAufliaOp.PLUS) {
107: if (fArgs.length < 2)
108: throw new IllegalArgumentException(creationFailureArity);
109: for (int i = 0; i < fArgs.length; i++) {
110: if (!isIntSort(fArgs[i])) {
111: throw new IllegalArgumentException(
112: creationFailureIntArb);
113: }
114: }
115:
116: } else if (fName == DecisionProcedureSmtAufliaOp.MINUS) {
117: if (fArgs.length != 2)
118: throw new IllegalArgumentException(creationFailureArity);
119: if (!isIntSort(fArgs[0]))
120: throw new IllegalArgumentException(
121: creationFailureIntArb);
122: if (!isIntSort(fArgs[1]))
123: throw new IllegalArgumentException(
124: creationFailureIntArb);
125:
126: } else if (fName == DecisionProcedureSmtAufliaOp.UMINUS) {
127: if (fArgs.length != 1)
128: throw new IllegalArgumentException(creationFailureArity);
129: if (!isIntSort(fArgs[0]))
130: throw new IllegalArgumentException(
131: creationFailureIntArb);
132:
133: } else if (fName == DecisionProcedureSmtAufliaOp.MULT) {
134: if (fArgs.length != 2)
135: throw new IllegalArgumentException(creationFailureArity);
136: if (!(fArgs[0] instanceof NumberConstantTerm | fArgs[1] instanceof NumberConstantTerm))
137: throw new IllegalArgumentException(
138: creationFailureArgType);
139: if (!isIntSort(fArgs[0]))
140: throw new IllegalArgumentException(
141: creationFailureIntArb);
142: if (!isIntSort(fArgs[1]))
143: throw new IllegalArgumentException(
144: creationFailureIntArb);
145:
146: } else if (fName == DecisionProcedureSmtAufliaOp.SELECT) {
147: if (fArgs.length != 2)
148: throw new IllegalArgumentException(creationFailureArity);
149: if (!isArraySort(fArgs[0]))
150: throw new IllegalArgumentException(creationFailureArray);
151: if (!isIntSort(fArgs[1]))
152: throw new IllegalArgumentException(creationFailureInt);
153:
154: } else if (fName == DecisionProcedureSmtAufliaOp.STORE) {
155: if (fArgs.length != 3)
156: throw new IllegalArgumentException(creationFailureArity);
157: if (!isArraySort(fArgs[0]))
158: throw new IllegalArgumentException(creationFailureArray);
159: if (!isIntSort(fArgs[1]))
160: throw new IllegalArgumentException(creationFailureInt);
161: if (!isIntSort(fArgs[2]))
162: throw new IllegalArgumentException(creationFailureInt);
163:
164: // No interpreted function
165: } else
166: throw new IllegalArgumentException(
167: creationFailureUninterpreted);
168: }
169:
170: // Public method implementation
171:
172: /** Compares this <tt>InterpretedFuncTerm</tt> to the specified <tt>Object</tt>.
173: * <p>
174: * This <tt>InterpretedFuncTerm</tt> is considered equal to <tt>o</tt> if <tt>o</tt> is an
175: * instance of <tt>InterpretedFuncTerm</tt> and has the same function arguments as this
176: * <tt>InterpretedFuncTerm</tt>. <br>
177: * If the represented function is commutative, i.e. if this <tt>InterpretedFuncTerm</tt>
178: * represents one of the functions 'PLUS' or 'MULT', the order of function arguments does
179: * not matter for equality. For all other interpreted functions in (QF_)AUFLIA, the order of
180: * arguments matters for equality.
181: *
182: * @param o the <tt>Object</tt> to compare with
183: * @return true if this <tt>InterpretedFuncTerm</tt> is the same as the <tt>Object</tt> o;
184: * otherwise false.
185: */
186: public boolean equals(Object o) {
187: if (o == this )
188: return true;
189: if (o instanceof InterpretedFuncTerm) {
190: if (super .equals(o))
191: return true;
192: InterpretedFuncTerm t = (InterpretedFuncTerm) o;
193: String this Function = super .getFunction();
194: if (this Function.equals(t.getFunction())) {
195: if (this Function
196: .equals(DecisionProcedureSmtAufliaOp.PLUS)
197: | this Function
198: .equals(DecisionProcedureSmtAufliaOp.MULT)) {
199: // Two commutative functions are equal, if their set of arguments is the same
200: Vector this Args = toVector(super .getFuncArgs());
201: Vector tArgs = toVector(t.getFuncArgs());
202: if (this Args.containsAll(tArgs)
203: && tArgs.containsAll(this Args)) {
204: return true;
205: }
206: }
207: }
208: }
209: return false;
210: }
211:
212: /* (non-Javadoc)
213: * @see de.uka.ilkd.key.proof.decproc.smtlib.Term#hashCode()
214: */
215: public int hashCode() {
216: String this Function = getFunction();
217: // Non commutative functions
218: if (this Function.equals(DecisionProcedureSmtAufliaOp.MINUS)
219: | this Function
220: .equals(DecisionProcedureSmtAufliaOp.UMINUS)
221: | this Function
222: .equals(DecisionProcedureSmtAufliaOp.SELECT)
223: | this Function
224: .equals(DecisionProcedureSmtAufliaOp.STORE)) {
225: return super .hashCode();
226: }
227: // Commutative functions
228: if (cachedCommHashCode == 0) {
229: Term[] this FuncArgs = getFuncArgs();
230: int result = 17;
231: result = 37 * result + this Function.hashCode();
232: int[] hashCodes = new int[this FuncArgs.length];
233: for (int i = 0; i < this FuncArgs.length; i++) {
234: hashCodes[i] = this FuncArgs[i].hashCode();
235: }
236: // Use the sum and the product of calculated argument hashes
237: int sum = 0;
238: int product = 1;
239: for (int i = 0; i < hashCodes.length; i++) {
240: sum += hashCodes[i];
241: product *= hashCodes[i];
242: }
243: result = 37 * result + sum;
244: result = 37 * result + product;
245: cachedCommHashCode = result;
246: }
247: return cachedCommHashCode;
248: }
249:
250: /* (non-Javadoc)
251: * @see de.uka.ilkd.key.proof.decproc.smtlib.Term#toString()
252: */
253: public String toString() {
254: String representation = "(" + getFunction();
255: Term[] this FuncArgs = getFuncArgs();
256: for (int i = 0; i < this FuncArgs.length; i++) {
257: representation += " " + this FuncArgs[i].toString();
258: }
259: representation += ")";
260: return representation;
261: }
262:
263: /* (non-Javadoc)
264: * @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)
265: */
266: public Term replaceTermVar(TermVariable termVar, Term replacement) {
267: if (!containsTerm(termVar))
268: return this ;
269: Term[] newSubterms = getFuncArgs();
270: for (int i = 0; i < newSubterms.length; i++) {
271: newSubterms[i] = newSubterms[i].replaceTermVar(termVar,
272: replacement);
273: }
274: return new InterpretedFuncTerm(getFunction(), newSubterms);
275: }
276:
277: /* (non-Javadoc)
278: * @see de.uka.ilkd.key.proof.decproc.smtlib.Term#replaceFormVarIteTerm(de.uka.ilkd.key.proof.decproc.smtlib.FormulaVariable, de.uka.ilkd.key.proof.decproc.smtlib.Formula)
279: */
280: public Term replaceFormVarIteTerm(FormulaVariable formVar,
281: Formula replacement) {
282: if (!containsFormulaIteTerm(formVar))
283: return this ;
284: Term[] newFuncArgs = getFuncArgs();
285: for (int i = 0; i < newFuncArgs.length; i++) {
286: newFuncArgs[i] = newFuncArgs[i].replaceFormVarIteTerm(
287: formVar, replacement);
288: }
289: return new InterpretedFuncTerm(getFunction(), newFuncArgs);
290: }
291:
292: // Internal methods */
293:
294: /** Converts an array of <tt>Term</tt>s into a <tt>Vector</tt>, preserving element order
295: *
296: * @param terms The array which should be converted into a <tt>Vector</tt>
297: * @return a <tt>Vector</tt> containing all the <tt>Term</tt>s in the specified array,
298: * in the same order
299: */
300: private Vector toVector(Term[] terms) {
301: Vector termVector = new Vector(terms.length);
302: for (int i = 0; i < terms.length; i++) {
303: termVector.add(i, terms[i]);
304: }
305: return termVector;
306: }
307:
308: /** Checks if the specified <tt>Term</tt> is of sort 'array', which is interpreted in (QF_)AUFLIA
309: *
310: * @param t the <tt>Term</tt> to be checked for being of sort 'array'
311: * @return true iff the result of the function represented by this <tt>Term</tt> is of sort 'array'
312: */
313: private boolean isArraySort(Term t) {
314: // Uninterpreted functions can have the return type 'array'
315: if (t instanceof UninterpretedFuncTerm) {
316: UninterpretedFuncTerm uiTerm = (UninterpretedFuncTerm) t;
317: Signature uiSig = uiTerm.getSignature();
318: if (uiSig.getSymbols()[uiSig.getLength() - 1] == DecisionProcedureSmtAufliaOp.ARRAY) {
319: return true;
320: }
321: // As interpreted function only STORE returns an 'array'
322: } else if (t instanceof InterpretedFuncTerm) {
323: if (t.getFunction() == DecisionProcedureSmtAufliaOp.STORE)
324: return true;
325: // Both alternatives must be of type 'array'
326: } else if (t instanceof IteTerm) {
327: IteTerm ite = (IteTerm) t;
328: return (isArraySort(ite.getTermT1()) & isArraySort(ite
329: .getTermT2()));
330: // For a term variable, an arbitrary term could be set
331: } else if (t instanceof TermVariable)
332: return true;
333: return false;
334: }
335:
336: /** Checks if the specified <tt>Term</tt> is of sort 'int', which is interpreted in (QF_)AUFLIA
337: *
338: * @param t the <tt>Term</tt> to be checked for being of sort 'int'
339: * @return true iff the result of the function represented by this <tt>Term</tt> is of sort 'int'
340: */
341: private boolean isIntSort(Term t) {
342: // Uninterpreted functions can have the return type 'int'
343: if (t instanceof UninterpretedFuncTerm) {
344: UninterpretedFuncTerm uiTerm = (UninterpretedFuncTerm) t;
345: Signature uiSig = uiTerm.getSignature();
346: if (uiSig.getSymbols()[uiSig.getLength() - 1] == DecisionProcedureSmtAufliaOp.INT) {
347: return true;
348: }
349: return false;
350: // As interpreted function only STORE returns an 'array'
351: } else if (t instanceof InterpretedFuncTerm) {
352: if (t.getFunction() == DecisionProcedureSmtAufliaOp.STORE)
353: return false;
354: // Both alternatives must be of type 'int'
355: } else if (t instanceof IteTerm) {
356: IteTerm ite = (IteTerm) t;
357: return (isIntSort(ite.getTermT1()) & isIntSort(ite
358: .getTermT2()));
359: }
360: // Number constants are of type 'int', term variables can be
361: return true;
362: }
363: }
|