public class Transformer extends Function
Constructor and Description |
---|
Transformer(Name name,
Sort argSort) |
Transformer(Name name,
Sort sort,
ImmutableArray<Sort> argSorts) |
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 Transformer |
getTransformer(Name name,
Sort sort,
ImmutableArray<Sort> argSorts,
TermServices services)
Looks up the function namespace for a term transformer with the given
attributes, assuming it to be uniquely defined by its name.
|
static Transformer |
getTransformer(PosInOccurrence pio)
Examines a position for whether it is inside a term transformer.
|
static Transformer |
getTransformer(Transformer t,
TermServices services)
Takes a template for a term transformer and checks in the function
namespace, whether an equivalent already exists.
|
static boolean |
inTransformer(PosInOccurrence pio)
Examines a position for whether it is inside a term transformer.
|
boolean |
isRigid()
Tells whether the operator is rigid.
|
Name |
name()
returns the name of this element
|
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() |
isSkolemConstant, isUnique, proofToString, rename, toString
additionalValidTopLevel, argSort, argSorts, sort, sort
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
arity, bindVarsAt, isRigid, validTopLevel, validTopLevelException
public Transformer(Name name, Sort sort, ImmutableArray<Sort> argSorts)
public static Transformer getTransformer(Name name, Sort sort, ImmutableArray<Sort> argSorts, TermServices services)
name
- name of the term transformersort
- sort of the term transformerargSorts
- array of the transformer's argument sortsservices
- public static Transformer getTransformer(Transformer t, TermServices services)
t
- the template for a term transformerservices
- public static boolean inTransformer(PosInOccurrence pio)
pio
- A position in an occurrence of a termpublic static Transformer getTransformer(PosInOccurrence pio)
pio
- A position in an occurrence of a termprotected 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 recogniseCopyright © 2003-2019 The KeY-Project.