| java.lang.Object
 de.uka.ilkd.key.proof.decproc.smtlib.Signature
| Signature | | final public class Signature (Code) | | Represents a signature for the uninterpreted terms and formulae of the SMT-Lib specification
and the QF_AUFLIA sublogic.
A signature thereby is a String array, with each String representing the
required sort for the corresponding argument and the result sort of an uninterpreted
function respectively.
A Signature is immutable, i.e. after creation its attribute values cannot be altered
any more . Due to this immutability, it is possible to cache the created signature objects
internally to reduce memory footprint
author:
akuwertz
version:
1.2, 12/05/2005 (Replaced exception by standard exceptions; added further comments) |
| Method Summary | |
| public static void | clearSignatureCache()
| | public static Signature | constSignature(boolean switcher)
A factory method that returns a Signature instance which consists of only one
symbol representing an array or an integer in QF_AUFLIA.
The objects returned by this method are cached internally. | | public boolean | equals(Object o)
Compares this Signature to the specified Object. | | public int | getLength()
Returns the length of this Signature, i.e. | | public String[] | getSymbols()
| | public Set | getUiSorts()
| | public int | hashCode()
Returns an int value representing the hash code of this Signature. | | public static Signature | intSignature(int arity, boolean hasReturnType)
A factory method that returns a Signature instance which consists only of
symbols representing integers in QF_AUFLIA. | | public String | toString()
Returns a string representation of this Signature. |
| Signature | | public Signature(String[] sig)(Code) | | Creates a new Signature, which consists of the specified Strings
Parameters:
sig - the array of signature symbols for this Signature
throws:
NullPointerException - if sig is or contains any nullpointer |
| constSignature | | public static Signature constSignature(boolean switcher)(Code) | | A factory method that returns a Signature instance which consists of only one
symbol representing an array or an integer in QF_AUFLIA.
The objects returned by this method are cached internally. Therefore successive calls with
the same value for switcher return the same objects.
This cache is provided to reduce memory footprint.
Parameters:
switcher - a boolean used to decide if the signature symbol should be the array (true)or the integer symbol (false) a Signature consisting of only one symbol |
| equals | | public boolean equals(Object o)(Code) | | Compares this Signature to the specified Object.
o is equal to this Signature if it is an instance of Signature
and if the String array containing the signature symbols of this Signature
is equal to that of o
true iff the specified Object is equals to this Signature |
| getLength | | public int getLength()(Code) | | Returns the length of this Signature, i.e. the the number of signature symbols
contained in this Signature.
the length of this Signature |
| getSymbols | | public String[] getSymbols()(Code) | | Returns an array containing the signature symbols of this Signature as shallow copy
the array of signature symbols for this Signature |
| getUiSorts | | public Set getUiSorts()(Code) | | Return an array of all uninterpreted sort symbols contained in this Signature
as shallow copy
the array of all uninterpreted sort symbols of this Signature |
| hashCode | | public int hashCode()(Code) | | Returns an int value representing the hash code of this Signature.
The hash code for a Signature is calculated during its creation by combining
the hash codes of its signature symbols to a new one
the hash Code of this Signature |
| intSignature | | public static Signature intSignature(int arity, boolean hasReturnType)(Code) | | A factory method that returns a Signature instance which consists only of
symbols representing integers in QF_AUFLIA.
Because Signatures can be assigned to functions and predicates, there is a
parameter 'hasReturnType' indicating if the return type of the assigned object should
be contained in this Signature (This is the case for uninterpreted function,
but not for uninterpreted predicates ).
The Signature objects returned by this method are cached internally. Therefore
on successive calls with same or equivalent arguments this method provides same objects.
Arguments are considered equivalent if they result in Signatures of the same length.
This cache is provided to reduce memory footprint. It can be cleared by calling the
clearSignatureCache method.
Parameters:
arity - the arity of the function/predicate symbol which the Signatureis to be assigned to
Parameters:
hasReturnType - Specifies if an integer symbol should be added at the end of thereturned Signature, representing the return type of itsassigned function a Signature consisting of the specified number of integer symbols
throws:
IllegalArgumentException - if arity is negative
See Also: de.uka.ilkd.key.proof.decproc.smtlib.Signature.clearSignatureCache
See Also: |
| toString | | public String toString()(Code) | | Returns a string representation of this Signature.
The returned String consists of the signature symbols, separated by spaces
the string representation of this Signature |
|
|