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.HashMap;
021: import java.util.HashSet;
022: import java.util.Set;
023:
024: import de.uka.ilkd.key.proof.decproc.DecisionProcedureSmtAufliaOp;
025:
026: /** Represents a signature for the uninterpreted terms and formulae of the SMT-Lib specification
027: * and the QF_AUFLIA sublogic.
028: * <p>
029: * A signature thereby is a <tt>String</tt> array, with each <tt>String</tt> representing the
030: * required sort for the corresponding argument and the result sort of an uninterpreted
031: * function respectively.
032: * <p>
033: * A <tt>Signature</tt> is immutable, i.e. after creation its attribute values cannot be altered
034: * any more . Due to this immutability, it is possible to cache the created signature objects
035: * internally to reduce memory footprint
036: *
037: * @author akuwertz
038: * @version 1.2, 12/05/2005 (Replaced exception by standard exceptions; added further comments)
039: */
040:
041: public final class Signature {
042:
043: /* Additional fields */
044:
045: /** The array of signature symbols of this <tt>Signature</tt> */
046: private final String[] signature;
047: /** The set of uninterpreted sort symbols of this <tt>Signature</tt> */
048: private final Set uiSorts;
049: /** The cached hash code of this <tt>Signature</tt> */
050: private final int hashCode;
051: /** Cached <tt>Signature</tt> object representing a one symbol signature */
052: private static Signature oneIntSig, oneArrSig;
053: /** Cache for <tt>Signature</tt> objects which only consist of integer symbols */
054: private static final HashMap intSigs = new HashMap();
055:
056: /* String constants for failures during Signature creation */
057: private static final String creationFailureSigNull = "Signature symbol array is null!";
058: private static final String creationFailureSigContNull = "Signature symbol array contains a nullpointer at position !";
059: private static final String creationFailureArityNegative = "Arity must not be negative!";
060:
061: /* Constructors */
062:
063: /** Creates a new <tt>Signature</tt>, which consists of the specified <tt>String</tt>s
064: *
065: * @param sig the array of signature symbols for this <tt>Signature</tt>
066: * @throws NullPointerException if <tt>sig</tt> is or contains any nullpointer
067: */
068: public Signature(String[] sig) {
069: if (sig == null)
070: throw new NullPointerException(creationFailureSigNull);
071: signature = (String[]) sig.clone();
072: uiSorts = findUiSorts(); // Also checks for null pointer
073: int result = 17;
074: for (int i = 0; i < sig.length; i++) {
075: result = 37 * result + sig[i].hashCode();
076: }
077: hashCode = result;
078: }
079:
080: /* Public method implementation */
081:
082: /** A factory method that returns a <tt>Signature</tt> instance which consists only of
083: * symbols representing integers in QF_AUFLIA.
084: * <p>
085: * Because <tt>Signature</tt>s can be assigned to functions and predicates, there is a
086: * parameter 'hasReturnType' indicating if the return type of the assigned object should
087: * be contained in this <tt>Signature</tt> (This is the case for uninterpreted function,
088: * but not for uninterpreted predicates ).
089: * <p>
090: * The <tt>Signature</tt> objects returned by this method are cached internally. Therefore
091: * on successive calls with same or equivalent arguments this method provides same objects.
092: * Arguments are considered equivalent if they result in <tt>Signatures</tt> of the same length.
093: * This cache is provided to reduce memory footprint. It can be cleared by calling the
094: * <tt>clearSignatureCache</tt> method.
095: *
096: *
097: * @param arity the arity of the function/predicate symbol which the <tt>Signature</tt>
098: * is to be assigned to
099: * @param hasReturnType Specifies if an integer symbol should be added at the end of the
100: * returned <tt>Signature</tt>, representing the return type of its
101: * assigned function
102: * @return a <tt>Signature</tt> consisting of the specified number of integer symbols
103: *
104: * @throws IllegalArgumentException if <tt>arity</tt> is negative
105: *
106: * @see de.uka.ilkd.key.proof.decproc.smtlib.Signature#clearSignatureCache()
107: */
108: public static Signature intSignature(int arity,
109: boolean hasReturnType) {
110: if (arity < 0)
111: throw new IllegalArgumentException(
112: creationFailureArityNegative);
113: // If there is a return type, the signature consists of arity + 1 'ints'
114: int count = hasReturnType ? arity + 1 : arity;
115: Integer index = new Integer(count);
116: if (intSigs.get(index) == null) {
117: String[] ints = new String[count];
118: for (int i = 0; i < count; i++) {
119: ints[i] = DecisionProcedureSmtAufliaOp.INT;
120: }
121: intSigs.put(index, new Signature(ints));
122: }
123: return (Signature) intSigs.get(index);
124: }
125:
126: /** A factory method that returns a <tt>Signature</tt> instance which consists of only one
127: * symbol representing an array or an integer in QF_AUFLIA.
128: * <p>
129: * The objects returned by this method are cached internally. Therefore successive calls with
130: * the same value for <tt>switcher</tt> return the same objects.<br>
131: * This cache is provided to reduce memory footprint.
132: *
133: * @param switcher a boolean used to decide if the signature symbol should be the array (true)
134: * or the integer symbol (false)
135: * @return a <tt>Signature</tt> consisting of only one symbol
136: */
137: public static Signature constSignature(boolean switcher) {
138: if (switcher) {
139: if (oneArrSig == null) {
140: oneArrSig = new Signature(
141: new String[] { DecisionProcedureSmtAufliaOp.ARRAY });
142: }
143: return oneArrSig;
144: }
145: if (oneIntSig == null) {
146: oneIntSig = new Signature(
147: new String[] { DecisionProcedureSmtAufliaOp.INT });
148: }
149: return oneIntSig;
150: }
151:
152: /** Returns an array containing the signature symbols of this <tt>Signature</tt> as shallow copy
153: *
154: * @return the array of signature symbols for this <tt>Signature</tt>
155: */
156: public String[] getSymbols() {
157: return (String[]) signature.clone();
158: }
159:
160: /** Returns the length of this <tt>Signature</tt>, i.e. the the number of signature symbols
161: * contained in this <tt>Signature</tt>.
162: *
163: * @return the length of this <tt>Signature</tt>
164: */
165: public int getLength() {
166: return signature.length;
167: }
168:
169: /** Return an array of all uninterpreted sort symbols contained in this <tt>Signature</tt>
170: * as shallow copy
171: *
172: * @return the array of all uninterpreted sort symbols of this <tt>Signature</tt>
173: */
174: public Set getUiSorts() {
175: return new HashSet(uiSorts);
176: }
177:
178: /** Compares this <tt>Signature</tt> to the specified <tt>Object</tt>.
179: * <p>
180: * <tt>o</tt> is equal to this <tt>Signature</tt> if it is an instance of <tt>Signature</tt>
181: * and if the <tt>String</tt> array containing the signature symbols of this <tt>Signature</tt>
182: * is equal to that of <tt>o</tt>
183: *
184: * @return true iff the specified <tt>Object</tt> is equals to this <tt>Signature</tt>
185: */
186: public boolean equals(Object o) {
187: if (o == this )
188: return true;
189: if (o instanceof Signature) {
190: Signature sig = (Signature) o;
191: if (signature.length == sig.getLength()) {
192: String[] sigSig = sig.getSymbols();
193: for (int i = 0; i < signature.length; i++) {
194: if (!signature[i].equals(sigSig[i]))
195: return false;
196: }
197: return true;
198: }
199:
200: }
201: return false;
202: }
203:
204: /** Returns an int value representing the hash code of this <tt>Signature</tt>.
205: * <p>
206: * The hash code for a <tt>Signature</tt> is calculated during its creation by combining
207: * the hash codes of its signature symbols to a new one
208: *
209: * @return the hash Code of this <tt>Signature</tt>
210: */
211: public int hashCode() {
212: return hashCode;
213: }
214:
215: /** Returns a string representation of this <tt>Signature</tt>.
216: * <p>
217: * The returned <tt>String</tt> consists of the signature symbols, separated by spaces
218: *
219: * @return the string representation of this <tt>Signature</tt>
220: */
221: public String toString() {
222: if (signature.length == 0)
223: return "";
224: String out = signature[0];
225: for (int i = 1; i < signature.length; i++) {
226: out += " " + signature[i];
227: }
228: return out;
229: }
230:
231: /** Clears the cache for <tt>Signature</tt> objects created with the <tt>intSignature</tt>
232: * method
233: *
234: * @see de.uka.ilkd.key.proof.decproc.smtlib.Signature#intSignature(int, boolean)
235: */
236: public static void clearSignatureCache() {
237: intSigs.clear();
238: }
239:
240: // Internal methods
241:
242: /** Finds all uninterpreted sort symbols contained in this <tt>Signature</tt>, and returns
243: * them as a <tt>Set</tt>
244: *
245: * @return a <tt>Set</tt> of all uninterpreted sort symbols contained in this <tt>Signature</tt>
246: */
247: private Set findUiSorts() {
248: Set foundUiSorts = new HashSet();
249: String toTest;
250: for (int i = 0; i < signature.length; i++) {
251: toTest = signature[i];
252: if (toTest == null)
253: throw new NullPointerException(
254: creationFailureSigContNull + i);
255: if (toTest != DecisionProcedureSmtAufliaOp.INT
256: & toTest != DecisionProcedureSmtAufliaOp.ARRAY) {
257: foundUiSorts.add(toTest);
258: }
259: }
260: return foundUiSorts;
261: }
262: }
|