public abstract class AbstractTermTransformer extends AbstractSortedOperator implements TermTransformer
Modifier | Constructor and Description |
---|---|
protected |
AbstractTermTransformer(Name name,
int arity) |
protected |
AbstractTermTransformer(Name name,
int arity,
Sort sort) |
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.
|
static java.lang.String |
convertToDecimalString(Term term,
Services services) |
boolean |
isRigid()
Tells whether the operator is rigid.
|
Name |
name()
returns the name of this element
|
static TermTransformer |
name2metaop(java.lang.String s) |
java.lang.String |
toString() |
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() |
additionalValidTopLevel, argSort, argSorts, sort, sort
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
transform
argSort, argSorts, sort
arity, bindVarsAt, isRigid, sort, validTopLevel, validTopLevelException
public static final Sort METASORT
public static final java.util.Map<java.lang.String,AbstractTermTransformer> NAME_TO_META_OP
public static final AbstractTermTransformer META_SHIFTRIGHT
public static final AbstractTermTransformer META_SHIFTLEFT
public static final AbstractTermTransformer META_AND
public static final AbstractTermTransformer META_OR
public static final AbstractTermTransformer META_XOR
public static final AbstractTermTransformer META_ADD
public static final AbstractTermTransformer META_SUB
public static final AbstractTermTransformer META_MUL
public static final AbstractTermTransformer META_DIV
public static final AbstractTermTransformer META_POW
public static final AbstractTermTransformer META_LESS
public static final AbstractTermTransformer META_GREATER
public static final AbstractTermTransformer META_LEQ
public static final AbstractTermTransformer META_GEQ
public static final AbstractTermTransformer META_EQ
public static final AbstractTermTransformer ARRAY_BASE_INSTANCE_OF
public static final AbstractTermTransformer CONSTANT_VALUE
public static final AbstractTermTransformer ENUM_CONSTANT_VALUE
public static final AbstractTermTransformer DIVIDE_MONOMIALS
public static final AbstractTermTransformer DIVIDE_LCR_MONOMIALS
public static final AbstractTermTransformer INTRODUCE_ATPRE_DEFINITIONS
public static final AbstractTermTransformer CREATE_LOCAL_ANON_UPDATE
public static final AbstractTermTransformer CREATE_HEAP_ANON_UPDATE
public static final AbstractTermTransformer CREATE_BEFORE_LOOP_UPDATE
public static final AbstractTermTransformer CREATE_FRAME_COND
public static final AbstractTermTransformer CREATE_WELLFORMED_COND
public static final AbstractTermTransformer MEMBER_PV_TO_FIELD
public static final AbstractTermTransformer ADD_CAST
public static final AbstractTermTransformer EXPAND_QUERIES
public static final AbstractTermTransformer OBSERVER_EQUALITY
protected AbstractTermTransformer(Name name, int arity)
public static TermTransformer name2metaop(java.lang.String s)
public static java.lang.String convertToDecimalString(Term term, 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.