public final class IntroAtPreDefsOp extends AbstractTermTransformer
ADD_CAST, ARRAY_BASE_INSTANCE_OF, CONSTANT_VALUE, CREATE_BEFORE_LOOP_UPDATE, CREATE_FRAME_COND, CREATE_HEAP_ANON_UPDATE, CREATE_LOCAL_ANON_UPDATE, CREATE_WELLFORMED_COND, DIVIDE_LCR_MONOMIALS, DIVIDE_MONOMIALS, ENUM_CONSTANT_VALUE, EXPAND_QUERIES, INTRODUCE_ATPRE_DEFINITIONS, MEMBER_PV_TO_FIELD, META_ADD, META_AND, META_DIV, META_EQ, META_GEQ, META_GREATER, META_LEQ, META_LESS, META_MUL, META_OR, META_POW, META_SHIFTLEFT, META_SHIFTRIGHT, META_SUB, META_XOR, METASORT, NAME_TO_META_OP, OBSERVER_EQUALITY
Constructor and Description |
---|
IntroAtPreDefsOp() |
Modifier and Type | Method and Description |
---|---|
int |
arity()
the arity of this operator
|
boolean |
bindVarsAt(int n)
Tells whether the operator binds variables at the n-th subterm.
|
boolean |
isRigid()
Tells whether the operator is rigid.
|
Name |
name()
returns the name of this element
|
java.lang.String |
toString() |
Term |
transform(Term term,
SVInstantiations svInst,
Services services)
initiates term transformation of term.
|
void |
updateBlockAndLoopContracts(ImmutableSet<? extends JavaStatement> statements,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
java.util.Map<LocationVariable,LocationVariable> atPreHeapVars,
Services services)
Replace the placeholder variables
(see
AuxiliaryContract.getPlaceholderVariables() )
of all block contracts for blocks in blocks by
atPreVars and atPreHeapVars |
void |
updateBlockAndLoopContracts(ImmutableSet<StatementBlock> blocks,
ImmutableSet<LoopStatement> loops,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
java.util.Map<LocationVariable,LocationVariable> atPreHeapVars,
Services services)
Replace the placeholder variables
(see
AuxiliaryContract.getPlaceholderVariables() )
of all block contracts for blocks in blocks by
atPreVars and atPreHeapVars |
void |
validTopLevelException(Term term)
Checks whether the top level structure of the given @link Term
is syntactically valid, given the assumption that the top level
operator of the term is the same as this Operator.
|
protected ImmutableArray<java.lang.Boolean> |
whereToBind() |
convertToDecimalString, name2metaop
additionalValidTopLevel, argSort, argSorts, sort, sort
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
argSort, argSorts, sort
arity, bindVarsAt, isRigid, sort, validTopLevel, validTopLevelException
public Term transform(Term term, SVInstantiations svInst, Services services)
TermTransformer
public void updateBlockAndLoopContracts(ImmutableSet<StatementBlock> blocks, ImmutableSet<LoopStatement> loops, java.util.Map<LocationVariable,LocationVariable> atPreVars, java.util.Map<LocationVariable,LocationVariable> atPreHeapVars, Services services)
AuxiliaryContract.getPlaceholderVariables()
)
of all block contracts for blocks in blocks
by
atPreVars
and atPreHeapVars
blocks
- the blocks whose contracts to update.loops
- the loops whose contracts to update.atPreVars
- all remembrance variables.atPreHeapVars
- all remembrance heaps.services
- services.public void updateBlockAndLoopContracts(ImmutableSet<? extends JavaStatement> statements, java.util.Map<LocationVariable,LocationVariable> atPreVars, java.util.Map<LocationVariable,LocationVariable> atPreHeapVars, Services services)
AuxiliaryContract.getPlaceholderVariables()
)
of all block contracts for blocks in blocks
by
atPreVars
and atPreHeapVars
statements
- the blocks and loops whose contracts to update.atPreVars
- all remembrance variables.atPreHeapVars
- all remembrance heaps.services
- services.protected final ImmutableArray<java.lang.Boolean> whereToBind()
public final Name name()
Named
public final int arity()
Operator
public final boolean bindVarsAt(int n)
Operator
bindVarsAt
in interface Operator
public final boolean isRigid()
Operator
public void validTopLevelException(Term term) throws TermCreationException
Operator
validTopLevelException
in interface Operator
TermCreationException
- if a construction error was recognisepublic java.lang.String toString()
toString
in class java.lang.Object
Copyright © 2003-2019 The KeY-Project.