| java.lang.Object
 de.uka.ilkd.key.proof.decproc.smtlib.Term
de.uka.ilkd.key.proof.decproc.smtlib.UninterpretedFuncTerm
| UninterpretedFuncTerm | | final public class UninterpretedFuncTerm extends Term (Code) | | Represents an uninterpreted function term as defined in the SMT-Lib specification,
and specialized in the (QF_)AUFLIA sublogic.
Each uninterpreted function is identified by its function name, which is an arbitrary legal
identifier String. An identifier is legal in (QF_)AUFLIA if it begins with a letter and
consists only of letters, digits and the characters '.' , '_' and ''' (single quotation mark).
UninterpretedFuncTerms are immutable; their attribute values cannot be changed after they
are created.
author:
akuwertz
version:
1.5, 12/04/2005 (Adjustments to changes in superclass; added further comments) |
| Constructor Summary | |
| public | UninterpretedFuncTerm(String fName, Term[] fArgs, Signature sig)
Creates a new UninterpretedFuncTerm, representing an uninterpreted function.
Every uninterpreted function is associated with a signature. |
| UninterpretedFuncTerm | | public UninterpretedFuncTerm(String fName, Term[] fArgs, Signature sig)(Code) | | Creates a new UninterpretedFuncTerm, representing an uninterpreted function.
Every uninterpreted function is associated with a signature. It contains one more sort symbol
than the function contains arguments; the last sort symbol represents the return type of this
UninterpretedFuncTerm
To create an uninterpreted constant, fArgs can be either null or an empty
array; choosing null reduces the memory footprint through shared objects
Parameters:
fName - the name of the uninterpreted function
Parameters:
fArgs - the array of function arguments
Parameters:
sig - the signature of this uninterpreted function
throws:
NullPointerException - if fName or sig is nullor if fArgs contains a null pointer
throws:
IllegalArgumentException - if fName is no legal identifier in (QF_)AUFLIA orif it equals an interpreted symbol or if the given signaturedoes not match the function argument count |
| getSignature | | public Signature getSignature()(Code) | | Returns the signature of this UninterpretedFuncTerm
the signature of this UninterpretedFuncTerm |
| hashCode | | public int hashCode()(Code) | | Returns an int value representing the hash code of this UninterpretedFuncTerm.
This hash code is calculated by combining the Term hash code of this
UninterpretedFuncTerm with the hash code of its Signature
the hash code of this UninterpretedFuncTerm |
| Fields inherited from de.uka.ilkd.key.proof.decproc.smtlib.Term | final protected static Vector marker(Code)(Java Doc)
|
|
|