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.HashSet;
021: import java.util.Vector;
022:
023: /**
024: * Represents a term as defined in the SMT-Lib specification, and specialized in the
025: * QF_AUFLIA sublogic. Thereby, a term represents a function in most cases. It is constructed
026: * recursively out of other terms, which are known as its the function arguments, and a String
027: * representing the function name.
028: * <p>
029: * This class is abstract because it is intended as a frame for realizing subclasses which
030: * specialize in representing one class of functions in QF_AUFLIA (e.g. uninterpreted functions).
031: * <p>
032: * Term objects are intentionally immutable; their attribute values cannot be changed once they are
033: * created.
034: * <p>
035: * This class also contains methods with protected access intended to be used by realizing
036: * subclasses for convenience, as well as methods to access a list of all uninterpreted functions
037: * and predicates contained in this term, which are provided for the simple integration of terms
038: * into a formulae and benchmarks.
039: *
040: * @author akuwertz
041: *
042: * @version 1.5, 12/04/2005 (Added further API comments)
043: *
044: * @see <a href="http://goedel.cs.uiowa.edu/smtlib/logics/QF_AUFLIA.smt">QF_AUFLIA</a>
045: * @see <a href="http://goedel.cs.uiowa.edu/smtlib">SMT-LIB</a>
046: */
047:
048: public abstract class Term {
049:
050: /** The function name of this <tt>Term</tt> */
051: private final String function;
052:
053: /** The array of function arguments of this <tt>Term</tt> */
054: private final Term[] funcArgs;
055:
056: /** A template <tt>Term</tt> array assigned to <tt>funcArgs</tt> if this <tt>Term</tt> has no
057: * function arguments. This shared object is intended to lower memory footprint */
058: private static final Term[] emptyTermArray = new Term[0];
059:
060: /** The <tt>Vector</tt> of all uninterpreted functions contained in this <tt>Term</tt> */
061: private final Vector uninterFuncs;
062:
063: /** The <tt>Vector</tt> of all uninterpreted predicates contained in this <tt>Term</tt>.
064: * This fields was included to support ite-constructs */
065: private final Vector uninterPredsIteTerm;
066:
067: /** A template <tt>Vector</tt> assigned to the <tt>Term</tt> attributes which store the
068: * uninterpreted functions and predicates of this <tt>Term</tt>, if these fields are empty.
069: * This shared object is intended to lower memory footprint */
070: private static final Vector emptyVector = new Vector();
071:
072: /** The cached hash code for this <tt>Term</tt> */
073: private final int hashCode;
074:
075: /** A <tt>Vector</tt> serving as an unique marker object. It is used by subclasses as an
076: * argument of the <tt>Term</tt> constructor to indicate to the constructor that a reference to
077: * the calling subclass instance must be contained in the uninterpreted functions field of the
078: * <tt>Term</tt> to be created
079: * @see de.uka.ilkd.key.proof.decproc.smtlib.Term#Term(String, de.uka.ilkd.key.proof.decproc.smtlib.Term[], java.util.Vector, java.util.Vector)
080: */
081: protected static final Vector marker = new Vector();
082:
083: /* Constructor */
084:
085: /** Sole constructor. For invocation by constructors of realizing subclasses.
086: * <p>
087: * This explicit constructor sets the internal fields to the specified values or rather to
088: * values computed out of the given ones. Thereby the function name and the function arguments
089: * are set directly, whereby the <tt>Vector</tt> of uninterpreted functions and predicates
090: * resprectively are computed out of the specified <tt>Vector</tt>s and the uninterpreted functions contained in
091: * the function arguments (respectively predicates).<br>
092: * Therefor all function argument <tt>Term</tt>s are searched for uninterpreted functions
093: * (respectively predicates) and the results are merged into a <tt>Vector</tt>, eleminating
094: * duplicate entries.<br>
095: * To enable realizing subclasses to specify further uninterpreted functions or predicates
096: * contained in this <tt>Term</tt> (which can not be computed from its function arguments), the
097: * argument <tt>Vector</tt>s <tt>addUifs</tt> and <tt>addUips</tt> are provided. Their elements
098: * are merged into the result <tt>Vector</tt>s as their first elements, preserving their given
099: * order.<br>
100: * Therefore, they must not contain duplicate elements. If set to <tt>null</tt> they indicate
101: * that there are no additional uninterpreted functions and predicates respectively.
102: * <p>
103: * The argument <tt>Vector</tt> <tt>addUifs</tt> inheres a additional function. It can serve as
104: * an indicator to the constructor that the calling subclass instance wishes to be added to the
105: * <tt>Vector</tt> of uninterpreted functions. If the specified <tt>Vector</tt> instance is the
106: * <tt>Vector</tt> contained in the static field <tt>marker</tt>, the calling instance will be
107: * added to the <tt>Vector</tt> of uninterpreted functions as its first element.
108: * <p>
109: * This implementation checks for null pointers in the specified arguments. As mentioned above,
110: * null pointers are explicitly allowed in <tt>addUifs</tt> and <tt>addUips</tt> for
111: * convenience.<br>
112: * No null pointers are allowed in the function name argument <tt>fName</tt>. If a null pointer
113: * is found, all fields will be set to <tt>null</tt> without throwing any exceptions. This
114: * is done to enable realizing subclasses to throw specific exceptions on their part. It
115: * implicates that every subclass realizing this class must check <tt>fName</tt> for being a
116: * null pointer, and, if so, throw an exception. Otherwise <tt>Term</tt> methods called on the
117: * created subclass instance could fail with a <tt>NullPointerException</tt>.<br>
118: * The same holds for the <tt>Term</tt>s contained in the array of function arguments
119: * <tt>fArgs</tt>. If the specified array contains any null pointers, the <tt>Term</tt> fields
120: * will be set to <tt>null</tt> without throwing an exception. Realizing subclasses therefore
121: * have to check or ensure that <tt>fArgs</tt> contains no null pointers; otherwise the
122: * <tt>Term</tt> methods could fail with a <tt>NullPointerException</tt>.<br>
123: * In contrary to this, a null pointer is allowed for the array object itself. This is done for
124: * convenience and has to same effects as an empty array would have.
125: *
126: * @param fName the function name of this <tt>Term</tt>
127: * @param fArgs the array of function arguments for this <tt>Term</tt>
128: * @param addUifs the Vector containing these <tt>Term</tt>s that should be merged into the
129: * <tt>Vector</tt> of uninterpreted functions additionally. It may be null and
130: * must not contain any duplicates.
131: * @param addUips the Vector containing these <tt>Formula</tt>e that should be merged into the
132: * <tt>Vector</tt> of uninterpreted predicates additionally. It may be null and
133: * must not contain any duplicates.
134: * @see de.uka.ilkd.key.proof.decproc.smtlib.Term#marker
135: */
136: protected Term(String fName, Term[] fArgs, Vector addUifs,
137: Vector addUips) {
138:
139: if (fName == null) {
140: function = null;
141: funcArgs = null;
142: uninterFuncs = uninterPredsIteTerm = null;
143: hashCode = 0;
144: // Handling of this null pointer situation has to be done by subclass
145: return;
146: }
147: function = fName;
148:
149: // Null pointer for fArgs is allowed for convenience
150: // Given array is cloned for immutability (exclusiveness)
151: if (fArgs == null || fArgs.length == 0)
152: funcArgs = emptyTermArray;
153: else
154: funcArgs = (Term[]) fArgs.clone();
155:
156: // Estimate capacity of new uif and uip Vectors to reduce reallocation effects to one
157: int estSizeUif = 0, estSizeUip = 0;
158: Vector[] uifHelper = new Vector[funcArgs.length];
159: Vector[] uipHelper = new Vector[funcArgs.length];
160:
161: try {
162: for (int i = 0; i < funcArgs.length; i++) {
163: uifHelper[i] = funcArgs[i].getUIF();
164: uipHelper[i] = funcArgs[i].getUIPredicatesIteTerm();
165: estSizeUif += uifHelper[i].size();
166: estSizeUip += uipHelper[i].size();
167: }
168: } catch (NullPointerException e) {
169: uninterFuncs = uninterPredsIteTerm = null;
170: hashCode = 0;
171: // Handling of this null pointer situation has to be done by subclass
172: return;
173: }
174:
175: // Compute Vector of uninterpreted functions contained in this Term
176: if ((addUifs == null || (addUifs.size() == 0 && addUifs != marker))
177: && estSizeUif == 0) {
178: // If no uninterpreted functions contained, use empty template Vector
179: uninterFuncs = emptyVector;
180: } else {
181: // Compute Vector lengths and Vector elements, i.e. uninterpreted functions
182: HashSet contFuncNames = new HashSet(estSizeUif + 1);
183: // Create new Vector of estimated capacity
184: if (addUifs == null)
185: addUifs = new Vector(estSizeUif);
186: /* If the specified Vector is the marker Vector, make sure uninterFuncs contains a
187: * refenrence to itself */
188: else if (addUifs == marker) {
189: addUifs = new Vector(estSizeUif + 1);
190: addUifs.add(this );
191: contFuncNames.add(function);
192: } else {
193: if (addUifs.size() != 0) {
194: if (addUifs.size() < estSizeUif) {
195: Vector temp = addUifs;
196: addUifs = new Vector(estSizeUif + temp.size());
197: addUifs.addAll(temp);
198: } else {
199: addUifs.ensureCapacity(estSizeUif
200: + addUifs.size());
201: }
202: for (int i = 0; i < addUifs.size(); i++) {
203: contFuncNames.add(((Term) addUifs.get(i))
204: .getFunction());
205: }
206: }
207: addUifs.ensureCapacity(estSizeUif);
208: }
209: Vector uifVector;
210: for (int i = 0; i < uifHelper.length; i++) {
211: uifVector = uifHelper[i];
212: for (int j = 0; j < uifVector.size(); j++) {
213: if (contFuncNames.add(((Term) uifVector.get(j))
214: .getFunction())) {
215: addUifs.add(uifVector.get(j));
216: }
217: }
218: }
219: addUifs.trimToSize();
220: uninterFuncs = addUifs;
221: }
222:
223: // Compute Vector of uninterpreted predicates contained in this Term
224: if ((addUips == null || addUips.size() == 0) && estSizeUip == 0) {
225: // If no uninterpreted predicates contained, use empty template Vector
226: uninterPredsIteTerm = emptyVector;
227: } else {
228: // Compute Vector lengths and create Vector of appropriate size and
229: // prepare the HashSet with the given ui predicate names
230: HashSet contPredNames = new HashSet(estSizeUip);
231: if (addUips == null)
232: addUips = new Vector(estSizeUip);
233: else if (addUips.size() != 0) {
234: if (addUips.size() < estSizeUip) {
235: Vector temp = addUips;
236: addUips = new Vector(estSizeUip + temp.size());
237: addUips.addAll(temp);
238: } else {
239: addUips.ensureCapacity(estSizeUip + addUips.size());
240: }
241: for (int i = 0; i < addUips.size(); i++) {
242: contPredNames.add(((Formula) addUips.get(i))
243: .getOp());
244: }
245: }
246: addUips.ensureCapacity(estSizeUip);
247: // Compute contained ui predicates
248: Vector uipVector;
249: for (int i = 0; i < uipHelper.length; i++) {
250: uipVector = uipHelper[i];
251: for (int j = 0; j < uipVector.size(); j++) {
252: if (contPredNames.add(((Formula) uipVector.get(j))
253: .getOp())) {
254: addUips.add(uipVector.get(j));
255: }
256: }
257: }
258: addUips.trimToSize();
259: uninterPredsIteTerm = addUips;
260: }
261:
262: // Calculate hash code for a Term
263: int result = 17;
264: result = 37 * result + function.hashCode();
265: for (int i = 0; i < funcArgs.length; i++) {
266: result = 37 * result + funcArgs[i].hashCode();
267: }
268: hashCode = result;
269: }
270:
271: /* Now the public methods */
272:
273: /** Returns the function name of this <tt>Term</tt>
274: *
275: * @return the function name of this <tt>Term</tt>
276: */
277: public final String getFunction() {
278: return function;
279: }
280:
281: /** Returns a shallow copy of the function argument array of this <tt>Term</tt>
282: *
283: * @return the array of function arguments of this <tt>Term</tt>
284: */
285: public final Term[] getFuncArgs() {
286: return (Term[]) funcArgs.clone();
287: }
288:
289: /** Returns a <tt>Vector</tt> of all uninterpreted functions contained in this <tt>Term</tt>,
290: * as a shallow copy
291: *
292: * @return a <tt>Vector</tt> of all uninterpreted functions contained in this <tt>Term</tt>
293: */
294: public final Vector getUIF() {
295: return (Vector) uninterFuncs.clone();
296: }
297:
298: /** Returns a <tt>Vector</tt> of all uninterpreted predicates contained in this <tt>Term</tt>,
299: * as a shallow copy
300: *
301: * @return an <TT>Vector</tt> of all uninterpreted predicates contained in this <tt>Term</tt>
302: */
303: public final Vector getUIPredicatesIteTerm() {
304: return (Vector) uninterPredsIteTerm.clone();
305: }
306:
307: /** Returns true if this <tt>Term</tt> contains the <tt>Term</tt> <tt>t</tt>.
308: * <p>
309: * This implementation tries to determine containment by first checking if t <tt>equals</tt>
310: * this <tt>Term</tt>. If not, it calls <tt>containsTerm</tt> recursively on the function
311: * argument <tt>Term</tt>s of this <tt>Term</tt> and returns true, if one of the function
312: * arguments contains <tt>t</tt>
313: *
314: * @param t the <tt>Term</tt> to be checked for containment in this <tt>Term</tt>
315: * @return true if this <tt>Term</tt> contains t; otherwise false
316: */
317: public boolean containsTerm(Term t) {
318: // t is contained if it is equal
319: if (equals(t))
320: return true;
321: // t could also be contained in function argument
322: for (int i = 0; i < funcArgs.length; i++) {
323: if (funcArgs[i].containsTerm(t))
324: return true;
325: }
326: return false;
327: }
328:
329: /** Returns true if this <tt>Term</tt> contains the <tt>Formula</tt> f.
330: * <p>
331: * This implementation tries to determine containment by calling <tt>containsFormulaIteTerm</tt>
332: * recursively on the function argument <tt>Term</tt>s of this <tt>Term</tt> and returns true,
333: * if one of the function arguments contains <tt>t</tt>.<br>
334: * This method was included to support ite-constructs.
335: *
336: * @param f the <tt>Formula</tt> to be checked for containment in this <tt>Term</tt>
337: * @return true if this <tt>Term</tt> contains f
338: */
339: public boolean containsFormulaIteTerm(Formula f) {
340: for (int i = 0; i < funcArgs.length; i++) {
341: if (funcArgs[i].containsFormulaIteTerm(f))
342: return true;
343: }
344: return false;
345: }
346:
347: /** Compares this <tt>Term</tt> to the specified <tt>Object</tt>.
348: * <p>
349: * This implementation tries to determine equality by first checking if <tt>o</tt> is an
350: * instance of <tt>Term</tt>. If so, it checks if the function name of <tt>o</tt> is equal to
351: * the function name of this <tt>Term</tt>. If true, it checks if all function argument
352: * <tt>Term</tt>s contained in this <tt>Term</tt> are equal to those contained in <tt>o</tt>,
353: * and in same order. If so, true is returned.
354: * <p>
355: * Overriding methods are recommended to check for object equality in addition; this is not
356: * done in this implementation.
357: *
358: * @param o the <tt>Object</tt> to compare with
359: * @return true if this <tt>Term</tt> is the same as the <tt>Object</tt> o; otherwise false.
360: */
361: public boolean equals(Object o) {
362: if (o instanceof Term) {
363: Term t = (Term) o;
364: if (function.equals(t.getFunction())) {
365: Term[] tFuncArgs = t.getFuncArgs();
366: if (funcArgs.length == tFuncArgs.length) {
367: for (int i = 0; i < funcArgs.length; i++) {
368: if (!funcArgs[i].equals(tFuncArgs[i]))
369: return false;
370: }
371: return true;
372: }
373: }
374: }
375: return false;
376: }
377:
378: /** Returns an int value representing the hash code of this <tt>Term</tt>.
379: * <p>
380: * The hash code for a <tt>Term</tt> is calculated during its creation. This is done by
381: * combining the hash code of its function name with the hash codes of its function
382: * arguments, if available, to a new hash code. The order of function arguments matters for
383: * this implementation
384: *
385: * @return the hashCode of this <tt>Term</tt>
386: */
387: public int hashCode() {
388: return hashCode;
389: }
390:
391: /** Returns a String representation of this <tt>Term</tt>, containing the String representation
392: * of each of its arguments.
393: * <p>
394: * The returning <tt>String</tt> is formatted and can be parsed according to the SMT-Lib
395: * grammar specification (chapter seven, "Concrete Syntax")
396: *
397: * @see <a href="http://combination.cs.uiowa.edu/smtlib/papers/format-v1.1-r05.04.12.pdf">
398: * The SMT-LIB Standard: Version 1.1</a>
399: *
400: * @return a String representation of this <tt>Term</tt>
401: */
402: public abstract String toString();
403:
404: /** Replaces all occurrences of a specified <tt>TermVariable</tt> by a specified <tt>Term</tt>
405: * in a this <tt>Term</tt>.
406: * <p>
407: * Thereby this <tt>Term</tt> and the returned replaced <tt>Term</tt> share the same objects
408: * in their fields, except for those objects which contained the specified
409: * <tt>TermVariable</tt>.<br>
410: * This implicates that if <tt>termVar</tt> is not contained in this <tt>Term</tt>,
411: * this <tt>Term</tt> is returned without changes.
412: *
413: * @param termVar the <tt>TermVariable</tt> to be replaced
414: * @param replacement the <tt>Term</tt> used to replace termVar
415: * @return the <tt>Term</tt> obtained by replacing every (free) occurence of termVar by
416: * replacement in this <tt>Term</tt>
417: */
418: public abstract Term replaceTermVar(TermVariable termVar,
419: Term replacement);
420:
421: /** Replaces all occurrences of a specified <tt>FormulaVariable</tt> by a specified
422: * <tt>Formula</tt> in a this <tt>Term</tt>.
423: * <p>
424: * Thereby this <tt>Term</tt> and the returned replaced <tt>Term</tt> share the same objects
425: * in their fields, except for those objects which contained the specified
426: * <tt>FormulaVariable</tt>.<br>
427: * This implicates that if <tt>formVar</tt> is not contained in this <tt>Term</tt>,
428: * this <tt>Term</tt> is returned without changes.
429: * <p>
430: * This method was included to support ite-constructs
431: *
432: * @param formVar the <tt>FormulaVariable</tt> to be replaced
433: * @param replacement the <tt>Formula</tt> used to replace formVar
434: * @return the <tt>Term</tt> obtained by replacing every (free) occurence of formVar by
435: * replacement in this <tt>Term</tt>
436: */
437: public abstract Term replaceFormVarIteTerm(FormulaVariable formVar,
438: Formula replacement);
439:
440: /* Internal (protected) methods */
441:
442: /** Determines if a given identifier represents a legal identifier symbol in QF_AUFLIA.
443: * <p>
444: * An identifier is legal if it begins with a letter and consists only of letters, digits and
445: * the characters '.' , '_' and ''' (single quotation mark)
446: *
447: * @param identifier the String to be checked
448: * @return true if the specified String represents a legal identifier symbol; otherwise false
449: *
450: * @throws NullPointerException if <tt>identifier</tt> is null
451: */
452: protected static final boolean isLegalIdentifier(String identifier) {
453: char first = identifier.charAt(0);
454: // First character must be a letter
455: if ((first >= 'A' && first <= 'Z')
456: || (first >= 'a' && first <= 'z')) {
457: char act;
458: // All other characters must be letters or digits or '.', '_' or "'"
459: for (int i = 1; i < identifier.length(); i++) {
460: act = identifier.charAt(i);
461: if (!((act >= 'A' && act <= 'Z')
462: || (act >= 'a' && act <= 'z')
463: || (act >= '0' && act <= '9') || (act == '.'
464: || act == '_' || act == '\'')))
465: return false;
466: }
467: return true;
468: }
469: return false;
470: }
471: }
|