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 |
---|---|
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.
|
isSkolemConstant, isUnique, proofToString, rename, toString
additionalValidTopLevel, additionalValidTopLevel2, argSort, argSorts, sort, sort
arity, bindVarsAt, isRigid, name, validTopLevel, whereToBind
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
arity, bindVarsAt, isRigid, validTopLevel
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 term