| java.lang.Object
 de.uka.ilkd.key.logic.op.TermSymbol
de.uka.ilkd.key.logic.op.Function
All known Subclasses: de.uka.ilkd.key.logic.op.RigidFunction, de.uka.ilkd.key.logic.op.NonRigidFunctionLocation, de.uka.ilkd.key.logic.op.NonRigidFunction,
| Method Summary | |
| public ArrayOfSort | argSort()
| | public Sort | argSort(int n)
| | public int | arity()
| | public boolean | possibleSub(int at, Term possibleSub)
checks if a given Term could be subterm (at the atth subterm
position) of a term with this function at its top level. | | public boolean | possibleSubs(Term[] possibleSubs)
checks if given Terms could be subterms of a term with this
function at its top level. | | public String | proofToString()
| | public String | toString()
| | public boolean | validTopLevel(Term term)
checks if the given term is syntactically valid at its top
level assumed the top level operator were this, i.e. |
| Function | | public Function(Name name, Sort sort, Sort[] argSorts)(Code) | | creates a Function
Parameters:
name - String with name of the function
Parameters:
sort - the Sort of the function (result type)
Parameters:
argSorts - an array of Sort with the sorts of the function's arguments |
| Function | | public Function(Name name, Sort sort, ArrayOfSort argSorts)(Code) | | creates a Function
Parameters:
name - String with name of the function
Parameters:
sort - the Sort of the function (result type)
Parameters:
argSorts - ArrayOfSort of the function's arguments |
| argSort | | public ArrayOfSort argSort()(Code) | | array of allowed sorts of the function arguments |
| argSort | | public Sort argSort(int n)(Code) | | Sort of the n-th argument |
| arity | | public int arity()(Code) | | arity of the Function as int |
| possibleSub | | public boolean possibleSub(int at, Term possibleSub)(Code) | | checks if a given Term could be subterm (at the atth subterm
position) of a term with this function at its top level. The
validity of the given subterm is NOT checked.
Parameters:
at - theposition of the term where this method should check the validity.
Parameters:
possibleSub - the subterm to be ckecked. true iff the given term can be subterm at the indicatedposition |
| possibleSubs | | public boolean possibleSubs(Term[] possibleSubs)(Code) | | checks if given Terms could be subterms of a term with this
function at its top level. The check includes the comparison of
the required number of subterms and the number of given
terms. The validity of the given subterms is NOT checked.
Parameters:
possibleSubs - the subterms to be ckecked. true iff the given terms can be subterms and the number of giventerms and the required number of subterms are equal. |
| validTopLevel | | public boolean validTopLevel(Term term)(Code) | | checks if the given term is syntactically valid at its top
level assumed the top level operator were this, i.e. if the
direct subterms can be subterms of a term with this top level
operator, the method returns true. Furthermore, it is checked
that no variables are bound for none of the subterms.
Parameters:
term - the Term to be checked. true iff the given term has subterms that are suitablefor this function. |
|
|