| java.lang.Object
 de.uka.ilkd.key.logic.TermFactory
| TermFactory | | public class TermFactory (Code) | | The TermFactory is the only way to create terms using constructos of
class Term or any of its subclasses. It is the
only class that implements and may exploit knowledge about sub
classes of
Term all other classes of the system only know
about terms what the
Term class offers them.
This class is used to encapsulate knowledge about the internal term structures.
See
de.uka.ilkd.key.logic.TermBuilder for more convienient methods to create
terms.
|
| Inner Class :static class CacheKey | |
| Method Summary | |
| public Term | createAnonymousUpdateTerm(AnonymousUpdate op, Term sub)
| | public Term | createAnonymousUpdateTerm(Name name, Term target)
| | public Term | createArrayTerm(ArrayOp op, Term t, Term index)
| | public Term | createArrayTerm(ArrayOp op, Term t, Term[] index)
| | public Term | createArrayTerm(ArrayOp arrayOp, Term[] subs)
| | public Term | createAttributeTerm(AttributeOp op, Term term)
| | public Term | createAttributeTerm(AttributeOp attrOp, Term[] subs)
| | public Term | createAttributeTerm(ProgramVariable var, Term term)
| | public Term | createAttributeTerm(SchemaVariable var, Term term)
| | public Term | createBoxTerm(JavaBlock javaBlock, Term subTerm)
| | public Term | createCastTerm(AbstractSort sort, Term with)
| | public Term | createDiamondTerm(JavaBlock javaBlock, Term subTerm)
| | public Term | createEqualityTerm(Equality op, Term[] subTerms)
creates a EqualityTerm with a given equality operator. | | public Term | createEqualityTerm(Equality op, Term t1, Term t2)
creates an EqualityTerm with a given equality operator. | | public Term | createEqualityTerm(Term t1, Term t2)
| | public Term | createEqualityTerm(Term[] terms)
| | public Term | createFunctionTerm(TermSymbol op)
| | public Term | createFunctionTerm(TermSymbol op, Term s1)
| | public Term | createFunctionTerm(TermSymbol op, Term s1, Term s2)
| | public Term | createFunctionTerm(TermSymbol op, Term[] subTerms)
| | public Term | createFunctionWithBoundVarsTerm(TermSymbol op, PairOfTermArrayAndBoundVarsArray subs)
| | public Term | createFunctionWithBoundVarsTerm(TermSymbol op, Term[] subTerms, ArrayOfQuantifiableVariable[] boundVars)
| | public Term | createIfExThenElseTerm(ArrayOfQuantifiableVariable exVars, Term condF, Term thenT, Term elseT)
| | public Term | createIfThenElseTerm(Term condF, Term thenT, Term elseT)
| | public Term | createJunctorTerm(Equality op, Term t1, Term t2)
some methods to handle the equality for formulas (equiv - operator) ... | | public Term | createJunctorTerm(Equality op, Term[] subTerms)
| | public Term | createJunctorTerm(Junctor op)
| | public Term | createJunctorTerm(Junctor op, Term t1)
| | public Term | createJunctorTerm(Junctor op, Term t1, Term t2)
| | public Term | createJunctorTerm(Junctor op, Term[] subTerms)
| | public Term | createJunctorTermAndSimplify(Equality op, Term t1, Term t2)
| | public Term | createJunctorTermAndSimplify(Junctor op, Term t1)
some methods for the creation of junctor terms with automatically performed simplification
like ( b /\ true ) == (b) ... | | public Term | createJunctorTermAndSimplify(Junctor op, Term t1, Term t2)
some methods for the creation of junctor terms with automatically performed simplification
like ( b /\ true ) == (b) ... | | public Term | createMetaTerm(MetaOperator op, Term[] subTerms)
creates a OpTerm with a meta operator as top operator. | | public Term | createNormalizedQuanUpdateTerm(QuanUpdateOperator op, Term[] subs, ArrayOfQuantifiableVariable[] boundVarsPerSub)
| | public Term | createProgramTerm(Operator op, JavaBlock javaBlock, Term subTerm)
| | public Term | createProgramTerm(Operator op, JavaBlock javaBlock, Term[] subTerms)
| | public Term | createQuanUpdateTerm(QuanUpdateOperator op, Term[] subs, ArrayOfQuantifiableVariable[] boundVarsPerSub)
| | public Term | createQuanUpdateTerm(ArrayOfQuantifiableVariable[] boundVars, Term[] guards, Term[] locs, Term[] values, Term target)
creates a normalized update term
{locs[0]:=values[0],...,locs[n]:=values[n]}target where
n is the length of the location array. | | public Term | createQuanUpdateTermUnordered(QuanUpdateOperator op, Term[] subs, ArrayOfQuantifiableVariable[] boundVars)
| | public Term | createQuantifierTerm(Quantifier quant, ArrayOfQuantifiableVariable varsBoundHere, Term subTerm)
| | public Term | createQuantifierTerm(Quantifier quant, QuantifiableVariable var, Term subTerm)
| | public Term | createQuantifierTerm(Quantifier quant, QuantifiableVariable[] varsBoundHere, Term subTerm)
| | public Term | createShadowArrayTerm(ShadowArrayOp op, Term t, Term index, Term shadownum)
| | public Term | createShadowArrayTerm(ShadowArrayOp op, Term t, Term[] index, Term shadownum)
creates a term representing a shadowed access on a multi
dimensional array. | | public Term | createShadowAttributeTerm(ProgramVariable var, Term term, Term shadownum)
| | public Term | createShadowAttributeTerm(SchemaVariable var, Term term, Term shadownum)
| | public Term | createShadowAttributeTerm(ShadowAttributeOp op, Term term, Term shadownum)
| | public Term | createSubstitutionTerm(SubstOp op, QuantifiableVariable substVar, Term substTerm, Term origTerm)
| | public Term | createSubstitutionTerm(SubstOp op, QuantifiableVariable substVar, Term[] subs)
| | public Term | createTerm(Operator op, Term[] subTerms, ArrayOfQuantifiableVariable vars, JavaBlock javaBlock)
| | public Term | createTerm(Operator op, Term[] subTerms, ArrayOfQuantifiableVariable[] bv, JavaBlock javaBlock)
| | public Term | createTerm(Operator op, Term[] subTerms, QuantifiableVariable[] vars, JavaBlock javaBlock)
creates a term using the other methods of this class depending on the
given operator. | | public Term | createUpdateTerm(ListOfUpdatePair pairs, Term target)
| | public Term | createUpdateTerm(Term loc, Term value, Term target)
| | public Term | createUpdateTerm(Term[] locs, Term[] values, Term target)
creates an update term
{locs[0]:=values[0],...,locs[n]:=values[n]}target
where n is the length of the location array. | | public Term | createUpdateTerm(UpdatePair pair, Term target)
| | public Term | createVariableTerm(LogicVariable v)
creates a term consisting of the given variable. | | public Term | createVariableTerm(ProgramVariable v)
| | public Term | createVariableTerm(SchemaVariable v)
|
| createAnonymousUpdateTerm | | public Term createAnonymousUpdateTerm(AnonymousUpdate op, Term sub)(Code) | | creates an anonymous update applied to the given target term
Parameters:
op - the AnonymousUpdate operator
Parameters:
subs - the array of Term containing the |
| createAnonymousUpdateTerm | | public Term createAnonymousUpdateTerm(Name name, Term target)(Code) | | creates an anonymous update applied to the given target term
Parameters:
name -
Parameters:
target - |
| createArrayTerm | | public Term createArrayTerm(ArrayOp op, Term t, Term[] index)(Code) | | creates a term representing an array access on the
index-th component of t
Parameters:
op - the ArrayOp used to access an array of type oft
Parameters:
t - the Term representing the array to be accessed
Parameters:
index - the Term describing the index of the arraycomponent to be accessed |
| createArrayTerm | | public Term createArrayTerm(ArrayOp arrayOp, Term[] subs)(Code) | |
Parameters:
arrayOp - the shadowed or normal version of the arrayaccess operator
Parameters:
subs - array of subterms the term representing an array access |
| createAttributeTerm | | public Term createAttributeTerm(AttributeOp attrOp, Term[] subs)(Code) | | creates a term representing an attribute access
Parameters:
attrOp - the AttributeOp representing the attribute to be accessed
Parameters:
subs - an array of Term containing the subterms (usually of length 1 but may have length 2 for shadowed accesses) the term subs[0].attr (or subs[0]^(subs[1]).attr)) |
| createAttributeTerm | | public Term createAttributeTerm(ProgramVariable var, Term term)(Code) | | creates an attribute term that references to a field of a class
Parameters:
var - the variable the attribute term references to
Parameters:
term - the Term describing the class/object of which theattribute value has to be determined the attribute term "term.var" |
| createAttributeTerm | | public Term createAttributeTerm(SchemaVariable var, Term term)(Code) | | creates an attribute term that references to a field of a class
Parameters:
var - the variable the attribute term references to
Parameters:
term - the Term describing the class/object of which theattribute value has to be determined the attribute term "term.var" |
| createEqualityTerm | | public Term createEqualityTerm(Equality op, Term[] subTerms)(Code) | | creates a EqualityTerm with a given equality operator. USE THIS WITH
CARE! THERE IS NO CHECK THAT THE EQUALITY OPERATOR MATCHES THE TERMS.
|
| createEqualityTerm | | public Term createEqualityTerm(Equality op, Term t1, Term t2)(Code) | | creates an EqualityTerm with a given equality operator. USE THIS WITH
CARE! THERE IS NO CHECK THAT THE EQUALITY OPERATOR MATCHES THE TERMS.
|
| createEqualityTerm | | public Term createEqualityTerm(Term[] terms)(Code) | | create an EqualityTerm with the correct equality symbol for
the sorts involved, according to
Sort.getEqualitySymbol |
| createFunctionTerm | | public Term createFunctionTerm(TermSymbol op, Term[] subTerms)(Code) | | creates a term representing a function or predicate
Parameters:
op - a TermSymbol which is the top level operator of thefunction term to be created
Parameters:
subTerms - array of Term containing the sub terms,usually the function's or predicate's arguments a term with op as top level symbol andthe terms in subTerms as arguments (directsubterms) |
| createFunctionWithBoundVarsTerm | | public Term createFunctionWithBoundVarsTerm(TermSymbol op, PairOfTermArrayAndBoundVarsArray subs)(Code) | | creates a term representing an OCL expression with a
collection operation as top operator that
takes an OclExpression as argument (not "iterate")
Parameters:
op - the OCL collection operation
Parameters:
varBoundHere - the iterator variable
Parameters:
subs - subs[0] is the collection and subs[1] is the expression in which the iterator variable is bound |
| createFunctionWithBoundVarsTerm | | public Term createFunctionWithBoundVarsTerm(TermSymbol op, Term[] subTerms, ArrayOfQuantifiableVariable[] boundVars)(Code) | | |
| createIfExThenElseTerm | | public Term createIfExThenElseTerm(ArrayOfQuantifiableVariable exVars, Term condF, Term thenT, Term elseT)(Code) | | Create an 'ifEx-then-else' term (or formula)
|
| createIfThenElseTerm | | public Term createIfThenElseTerm(Term condF, Term thenT, Term elseT)(Code) | | Create an 'if-then-else' term (or formula)
|
| createJunctorTerm | | public Term createJunctorTerm(Equality op, Term t1, Term t2)(Code) | | some methods to handle the equality for formulas (equiv - operator) ...
|
| createJunctorTerm | | public Term createJunctorTerm(Junctor op, Term[] subTerms)(Code) | | creates a JunctorTerm with top operator op, some subterms
Parameters:
op - Operator at the top of the termstructure that startshere
Parameters:
subTerms - an array containing subTerms (an array with length 0 ifthere are no more subterms |
| createJunctorTermAndSimplify | | public Term createJunctorTermAndSimplify(Junctor op, Term t1)(Code) | | some methods for the creation of junctor terms with automatically performed simplification
like ( b /\ true ) == (b) ...
Currently only the AND, OR, IMP Operators will be simplified (if possible)
|
| createJunctorTermAndSimplify | | public Term createJunctorTermAndSimplify(Junctor op, Term t1, Term t2)(Code) | | some methods for the creation of junctor terms with automatically performed simplification
like ( b /\ true ) == (b) ...
Currently only the AND, OR, IMP Operators will be simplified (if possible)
|
| createMetaTerm | | public Term createMetaTerm(MetaOperator op, Term[] subTerms)(Code) | | creates a OpTerm with a meta operator as top operator. These
terms are only used in the replacewith areas of taclets. And are
replaced by the SyntacticalReplaceVisitor
Parameters:
op - Operator at the top of the termstructure that startshere
Parameters:
subTerms - an array containing subTerms (an array with length 0 ifthere are no more subterms |
| createNormalizedQuanUpdateTerm | | public Term createNormalizedQuanUpdateTerm(QuanUpdateOperator op, Term[] subs, ArrayOfQuantifiableVariable[] boundVarsPerSub)(Code) | | creates a normalized simultaneous update term
Parameters:
op - the UpdateOperator
Parameters:
subs - the subterm of the simultaneous update term to be created the normalized simultaneous update term |
| createQuanUpdateTerm | | public Term createQuanUpdateTerm(QuanUpdateOperator op, Term[] subs, ArrayOfQuantifiableVariable[] boundVarsPerSub)(Code) | | creates a simultaneous update-term
Parameters:
subs - the sub-terms |
| createQuanUpdateTerm | | public Term createQuanUpdateTerm(ArrayOfQuantifiableVariable[] boundVars, Term[] guards, Term[] locs, Term[] values, Term target)(Code) | | creates a normalized update term
{locs[0]:=values[0],...,locs[n]:=values[n]}target where
n is the length of the location array.
Parameters:
locs - an array of Term describing the updates locations
Parameters:
values - an array of Term describing the values to which the locationsare updated
Parameters:
target - the Term on which the update is applied to the update term as described above |
| createQuanUpdateTermUnordered | | public Term createQuanUpdateTermUnordered(QuanUpdateOperator op, Term[] subs, ArrayOfQuantifiableVariable[] boundVars)(Code) | | creates an update term which is not in normalform order (usually usage of
this method is discouraged)
creates an update term which is not in normalform order |
| createQuantifierTerm | | public Term createQuantifierTerm(Quantifier quant, ArrayOfQuantifiableVariable varsBoundHere, Term subTerm)(Code) | | creates a quantifier term
Parameters:
quant - the Quantifier (all, exist) which binds thevariables in varsBoundHere
Parameters:
varsBoundHere - an array of QuantifiableVariablecontaining all variables bound by the quantifier
Parameters:
subTerm - the Term where the variables are bound the quantified term |
| createQuantifierTerm | | public Term createQuantifierTerm(Quantifier quant, QuantifiableVariable var, Term subTerm)(Code) | | creates a quantifier term
Parameters:
op - Operator representing theQuantifier (all, exist) of this term
Parameters:
varsBoundHere - a QuantifiableVariable representing the only boundvariable of this quantifier. |
| createQuantifierTerm | | public Term createQuantifierTerm(Quantifier quant, QuantifiableVariable[] varsBoundHere, Term subTerm)(Code) | | creates a quantifier term
Parameters:
op - Operator representing theQuantifier (all, exist) of this term
Parameters:
varsBoundHere - anarray of QuantifiableVariable containing all variables bound by thequantifier |
| createShadowArrayTerm | | public Term createShadowArrayTerm(ShadowArrayOp op, Term t, Term index, Term shadownum)(Code) | | creates a term representing a shadowed array access on the
index-th component of t
Parameters:
op - the ShadowArrayOp used to access "shadowed memoryareas"
Parameters:
t - the Term representing the array whoseindex component is accessed
Parameters:
index - the Term describing the index of the arraycomponent to be accessed
Parameters:
shadownum - the Term describing the nested scope ofshadowed access |
| createShadowArrayTerm | | public Term createShadowArrayTerm(ShadowArrayOp op, Term t, Term[] index, Term shadownum)(Code) | | creates a term representing a shadowed access on a multi
dimensional array. The exact component is specified by the
array of indices.
Parameters:
op - the ShadowArrayOp used to access "shadowed memoryareas"
Parameters:
t - the Term representing the array whoseindex component is accessed
Parameters:
index - an array of Term specifying the array component tobe accessed
Parameters:
shadownum - the Term describing the nested scope ofshadowed access |
| createSubstitutionTerm | | public Term createSubstitutionTerm(SubstOp op, QuantifiableVariable substVar, Term substTerm, Term origTerm)(Code) | | creates a substitution term
Parameters:
substVar - the QuantifiableVariable to be substituted
Parameters:
substTerm - the Term that replaces substVar
Parameters:
origTerm - the Term that is substituted |
| createSubstitutionTerm | | public Term createSubstitutionTerm(SubstOp op, QuantifiableVariable substVar, Term[] subs)(Code) | | creates a substitution term
Parameters:
op - the replacement variable
Parameters:
substVar - the QuantifiableVariable to be substituted
Parameters:
subs - an array of Term where subs[0] is the term thatreplaces the variable substVar in subs[1] |
| createTerm | | public Term createTerm(Operator op, Term[] subTerms, QuantifiableVariable[] vars, JavaBlock javaBlock)(Code) | | creates a term using the other methods of this class depending on the
given operator. If the kind of term is known before (without using
if-else cascades on the kind of operator) the other methods in this
factory should be preferred. Depending on the needed parameters for
the terms that should be created some of the parameters of this method
might be ignored.
Parameters:
op - the top level operator for the new term.
Parameters:
subTerms - the subterms for the new term. The first n elementsare taken if op is a Junctor or TermSymbol and n is the arityof op. Only the first entry is taken if op is a Quantifier ora Diamond. The first (representing the replacing termfor a variable) and the second (representing the term behind thesubstitution operator) entries are taken if op is a SubstOp.
Parameters:
vars - the variables that are bound to a subterm. Not consideredif op is a Junctor, TermSymbol or Diamond. If op is aSubstOp only the first element is taken and the variable is bound tothe second subterm. In all other cases all variables are taken andbound to the first subterm.
Parameters:
javaBlock - representing a java code block. Only taken if op is aDiamond. the created Term |
| createUpdateTerm | | public Term createUpdateTerm(ListOfUpdatePair pairs, Term target)(Code) | | creates an update term like
{pair0}..{pairN}target
|
| createUpdateTerm | | public Term createUpdateTerm(Term loc, Term value, Term target)(Code) | | creates the update term {loc:=value}target
Parameters:
loc - the Term representing the location to be updated
Parameters:
value - the Term representing the value the location is updated to
Parameters:
target - the Term on which the update is applied the update term described above |
| createUpdateTerm | | public Term createUpdateTerm(Term[] locs, Term[] values, Term target)(Code) | | creates an update term
{locs[0]:=values[0],...,locs[n]:=values[n]}target
where n is the length of the location array.
Parameters:
locs - an array of Term describing the updates locations
Parameters:
values - an array of Term describing the values to which the locations are updated
Parameters:
target - the Term on which the update is applied to the update term as described above |
| createVariableTerm | | public Term createVariableTerm(LogicVariable v)(Code) | | creates a term consisting of the given variable.
Parameters:
v - the variable |
| createVariableTerm | | public Term createVariableTerm(ProgramVariable v)(Code) | | creates a variable term representing the given programvariable
Parameters:
v - the ProgramVariable to be represented variable v as term |
| createVariableTerm | | public Term createVariableTerm(SchemaVariable v)(Code) | | creates a term with schemavariable v as top level operator
Parameters:
v - the SchemaVariable to be represented the term v |
|
|