| java.lang.Object
 de.uka.ilkd.key.proof.decproc.smtlib.Term
de.uka.ilkd.key.proof.decproc.smtlib.InterpretedFuncTerm
| InterpretedFuncTerm | | final public class InterpretedFuncTerm extends Term (Code) | | Represents an interpreted function as defined in the SMT-Lib specification,
and specialized in the (QF_)AUFLIA sublogic. In (QF_)AUFLIA, only + , - , unary
minus, * , 'select' (array) and 'store' (array) are interpreted functions.
InterpretedFuncTerms are immutable; their attribute values cannot be changed after they
are created.
author:
akuwertz
version:
1.4, 12/04/2005 (Adjustments to changes in superclass; added further comments) |
| Constructor Summary | |
| public | InterpretedFuncTerm(String fName, Term[] fArgs)
Creates a new InterpretedFuncTerm, representing an interpreted function as
defined in (QF_)AUFLIA.
Which interpreted function is to be represented, is specified solely by the function name.
Therefore, only certain String values are accepted as interpreted functions in
(QF_)AUFLIA; they are defined as static fields in DecisionProcedureSmtAufliaOp. |
| InterpretedFuncTerm | | public InterpretedFuncTerm(String fName, Term[] fArgs)(Code) | | Creates a new InterpretedFuncTerm, representing an interpreted function as
defined in (QF_)AUFLIA.
Which interpreted function is to be represented, is specified solely by the function name.
Therefore, only certain String values are accepted as interpreted functions in
(QF_)AUFLIA; they are defined as static fields in DecisionProcedureSmtAufliaOp.
Namely, this are PLUS, MINUS, UMINUS, MULT, SELECT and STORE.
In (QF_)AUFLIA, there are two interpreted sorts, INT and ARRAY. For the mentioned interpreted
functions the following signatures hold:
UMINUS: INT->INT
MINUS: INT->INT->INT
PLUS: INT->INT->INT
MULT: INT->INT->INT
SELECT: ARRAY->INT->INT
STORE: ARRAY->INT->INT->ARRAY
For convenience, the PLUS function allows also more than two arguments. The MULT function
requests of one its arguments to be a natural number constant.
The sort of a Term depends on its class:
A NumberConstantTermis of sort Int, a Termvariables of arbitrary sort.
For an InterpretedFuncTerm or an UninterpretedFuncTerm the sort is
determined by their signature. An IteTerm is of same sort as its argument
Terms.
If any of these conditions does not hold for the InterpretedFuncTerm to created,
an IllegalArgumentException is thrown.
Parameters:
fName - the name of the interpreted function to be represented
Parameters:
fArgs - the array of function arguments;
throws:
NullPointerException - if fName or fArgs is null or iffArgs contains a null pointer
throws:
IllegalArgumentException - if fName is no interpreted function symbol inQF_AULIA or if the number of function arguments doesn'tmatch the function arity or if the sort of a function argument doesn't match the expected sort
See Also: de.uka.ilkd.key.logic.op.DecisionProcedureSmtAufliaOp
See Also: |
| equals | | public boolean equals(Object o)(Code) | | Compares this InterpretedFuncTerm to the specified Object.
This InterpretedFuncTerm is considered equal to o if o is an
instance of InterpretedFuncTerm and has the same function arguments as this
InterpretedFuncTerm.
If the represented function is commutative, i.e. if this InterpretedFuncTerm
represents one of the functions 'PLUS' or 'MULT', the order of function arguments does
not matter for equality. For all other interpreted functions in (QF_)AUFLIA, the order of
arguments matters for equality.
Parameters:
o - the Object to compare with true if this InterpretedFuncTerm is the same as the Object o;otherwise false. |
| hashCode | | public int hashCode()(Code) | | |
| Fields inherited from de.uka.ilkd.key.proof.decproc.smtlib.Term | final protected static Vector marker(Code)(Java Doc)
|
|
|