| java.lang.Object
 de.uka.ilkd.key.proof.decproc.smtlib.Term
All known Subclasses: de.uka.ilkd.key.proof.decproc.smtlib.UninterpretedFuncTerm, de.uka.ilkd.key.proof.decproc.smtlib.NumberConstantTerm, de.uka.ilkd.key.proof.decproc.smtlib.TermVariable, de.uka.ilkd.key.proof.decproc.smtlib.IteTerm, de.uka.ilkd.key.proof.decproc.smtlib.InterpretedFuncTerm,
| Term | | abstract public class Term (Code) | | Represents a term as defined in the SMT-Lib specification, and specialized in the
QF_AUFLIA sublogic. Thereby, a term represents a function in most cases. It is constructed
recursively out of other terms, which are known as its the function arguments, and a String
representing the function name.
This class is abstract because it is intended as a frame for realizing subclasses which
specialize in representing one class of functions in QF_AUFLIA (e.g. uninterpreted functions).
Term objects are intentionally immutable; their attribute values cannot be changed once they are
created.
This class also contains methods with protected access intended to be used by realizing
subclasses for convenience, as well as methods to access a list of all uninterpreted functions
and predicates contained in this term, which are provided for the simple integration of terms
into a formulae and benchmarks.
author:
akuwertz
version:
1.5, 12/04/2005 (Added further API comments)
See Also: QF_AUFLIA
See Also: SMT-LIB |
| Field Summary | |
| final protected static Vector | marker
A Vector serving as an unique marker object. |
| Method Summary | |
| public boolean | containsFormulaIteTerm(Formula f)
Returns true if this Term contains the Formula f. | | public boolean | containsTerm(Term t)
Returns true if this Term contains the Term t.
This implementation tries to determine containment by first checking if t equals
this Term. | | public boolean | equals(Object o)
Compares this Term to the specified Object.
This implementation tries to determine equality by first checking if o is an
instance of Term. | | final public Term[] | getFuncArgs()
| | final public String | getFunction()
| | final public Vector | getUIF()
| | final public Vector | getUIPredicatesIteTerm()
| | public int | hashCode()
Returns an int value representing the hash code of this Term. | | final protected static boolean | isLegalIdentifier(String identifier)
Determines if a given identifier represents a legal identifier symbol in QF_AUFLIA. | | abstract public Term | replaceFormVarIteTerm(FormulaVariable formVar, Formula replacement)
Replaces all occurrences of a specified FormulaVariable by a specified
Formula in a this Term. | | abstract public Term | replaceTermVar(TermVariable termVar, Term replacement)
Replaces all occurrences of a specified TermVariable by a specified Term
in a this Term. | | abstract public String | toString()
Returns a String representation of this Term, containing the String representation
of each of its arguments. |
| Term | | protected Term(String fName, Term[] fArgs, Vector addUifs, Vector addUips)(Code) | | Sole constructor. For invocation by constructors of realizing subclasses.
This explicit constructor sets the internal fields to the specified values or rather to
values computed out of the given ones. Thereby the function name and the function arguments
are set directly, whereby the Vector of uninterpreted functions and predicates
resprectively are computed out of the specified Vectors and the uninterpreted functions contained in
the function arguments (respectively predicates).
Therefor all function argument Terms are searched for uninterpreted functions
(respectively predicates) and the results are merged into a Vector, eleminating
duplicate entries.
To enable realizing subclasses to specify further uninterpreted functions or predicates
contained in this Term (which can not be computed from its function arguments), the
argument Vectors addUifs and addUips are provided. Their elements
are merged into the result Vectors as their first elements, preserving their given
order.
Therefore, they must not contain duplicate elements. If set to null they indicate
that there are no additional uninterpreted functions and predicates respectively.
The argument Vector addUifs inheres a additional function. It can serve as
an indicator to the constructor that the calling subclass instance wishes to be added to the
Vector of uninterpreted functions. If the specified Vector instance is the
Vector contained in the static field marker, the calling instance will be
added to the Vector of uninterpreted functions as its first element.
This implementation checks for null pointers in the specified arguments. As mentioned above,
null pointers are explicitly allowed in addUifs and addUips for
convenience.
No null pointers are allowed in the function name argument fName. If a null pointer
is found, all fields will be set to null without throwing any exceptions. This
is done to enable realizing subclasses to throw specific exceptions on their part. It
implicates that every subclass realizing this class must check fName for being a
null pointer, and, if so, throw an exception. Otherwise Term methods called on the
created subclass instance could fail with a NullPointerException.
The same holds for the Terms contained in the array of function arguments
fArgs. If the specified array contains any null pointers, the Term fields
will be set to null without throwing an exception. Realizing subclasses therefore
have to check or ensure that fArgs contains no null pointers; otherwise the
Term methods could fail with a NullPointerException.
In contrary to this, a null pointer is allowed for the array object itself. This is done for
convenience and has to same effects as an empty array would have.
Parameters:
fName - the function name of this Term
Parameters:
fArgs - the array of function arguments for this Term
Parameters:
addUifs - the Vector containing these Terms that should be merged into theVector of uninterpreted functions additionally. It may be null andmust not contain any duplicates.
Parameters:
addUips - the Vector containing these Formulae that should be merged into theVector of uninterpreted predicates additionally. It may be null andmust not contain any duplicates.
See Also: de.uka.ilkd.key.proof.decproc.smtlib.Term.marker |
| containsFormulaIteTerm | | public boolean containsFormulaIteTerm(Formula f)(Code) | | Returns true if this Term contains the Formula f.
This implementation tries to determine containment by calling containsFormulaIteTerm
recursively on the function argument Terms of this Term and returns true,
if one of the function arguments contains t.
This method was included to support ite-constructs.
Parameters:
f - the Formula to be checked for containment in this Term true if this Term contains f |
| containsTerm | | public boolean containsTerm(Term t)(Code) | | Returns true if this Term contains the Term t.
This implementation tries to determine containment by first checking if t equals
this Term. If not, it calls containsTerm recursively on the function
argument Terms of this Term and returns true, if one of the function
arguments contains t
Parameters:
t - the Term to be checked for containment in this Term true if this Term contains t; otherwise false |
| equals | | public boolean equals(Object o)(Code) | | Compares this Term to the specified Object.
This implementation tries to determine equality by first checking if o is an
instance of Term. If so, it checks if the function name of o is equal to
the function name of this Term. If true, it checks if all function argument
Terms contained in this Term are equal to those contained in o,
and in same order. If so, true is returned.
Overriding methods are recommended to check for object equality in addition; this is not
done in this implementation.
Parameters:
o - the Object to compare with true if this Term is the same as the Object o; otherwise false. |
| getFuncArgs | | final public Term[] getFuncArgs()(Code) | | Returns a shallow copy of the function argument array of this Term
the array of function arguments of this Term |
| getFunction | | final public String getFunction()(Code) | | Returns the function name of this Term
the function name of this Term |
| getUIF | | final public Vector getUIF()(Code) | | Returns a Vector of all uninterpreted functions contained in this Term,
as a shallow copy
a Vector of all uninterpreted functions contained in this Term |
| getUIPredicatesIteTerm | | final public Vector getUIPredicatesIteTerm()(Code) | | Returns a Vector of all uninterpreted predicates contained in this Term,
as a shallow copy
an Vector of all uninterpreted predicates contained in this Term |
| hashCode | | public int hashCode()(Code) | | Returns an int value representing the hash code of this Term.
The hash code for a Term is calculated during its creation. This is done by
combining the hash code of its function name with the hash codes of its function
arguments, if available, to a new hash code. The order of function arguments matters for
this implementation
the hashCode of this Term |
| isLegalIdentifier | | final protected static boolean isLegalIdentifier(String identifier)(Code) | | Determines if a given identifier represents a legal identifier symbol in QF_AUFLIA.
An identifier is legal if it begins with a letter and consists only of letters, digits and
the characters '.' , '_' and ''' (single quotation mark)
Parameters:
identifier - the String to be checked true if the specified String represents a legal identifier symbol; otherwise false
throws:
NullPointerException - if identifier is null |
| replaceFormVarIteTerm | | abstract public Term replaceFormVarIteTerm(FormulaVariable formVar, Formula replacement)(Code) | | Replaces all occurrences of a specified FormulaVariable by a specified
Formula in a this Term.
Thereby this Term and the returned replaced Term share the same objects
in their fields, except for those objects which contained the specified
FormulaVariable.
This implicates that if formVar is not contained in this Term,
this Term is returned without changes.
This method was included to support ite-constructs
Parameters:
formVar - the FormulaVariable to be replaced
Parameters:
replacement - the Formula used to replace formVar the Term obtained by replacing every (free) occurence of formVar byreplacement in this Term |
| replaceTermVar | | abstract public Term replaceTermVar(TermVariable termVar, Term replacement)(Code) | | Replaces all occurrences of a specified TermVariable by a specified Term
in a this Term.
Thereby this Term and the returned replaced Term share the same objects
in their fields, except for those objects which contained the specified
TermVariable.
This implicates that if termVar is not contained in this Term,
this Term is returned without changes.
Parameters:
termVar - the TermVariable to be replaced
Parameters:
replacement - the Term used to replace termVar the Term obtained by replacing every (free) occurence of termVar by replacement in this Term |
| toString | | abstract public String toString()(Code) | | Returns a String representation of this Term, containing the String representation
of each of its arguments.
The returning String is formatted and can be parsed according to the SMT-Lib
grammar specification (chapter seven, "Concrete Syntax")
See Also:
* The SMT-LIB Standard: Version 1.1 a String representation of this Term |
|
|