de.uka.ilkd.key.logic.op

Class AbstractTermTransformer

java.lang.Object

de.uka.ilkd.key.logic.op.AbstractOperator

de.uka.ilkd.key.logic.op.AbstractSortedOperator

de.uka.ilkd.key.logic.op.AbstractTermTransformer

All Implemented Interfaces:

Named, Operator, SortedOperator, SVSubstitute, TermTransformer, Sorted

Direct Known Subclasses:

AddCast, ArrayBaseInstanceOf, ConstantValue, DivideLCRMonomials, DivideMonomials, EnumConstantValue, ExpandQueriesMetaConstruct, IntroAtPreDefsOp, MemberPVToField, MetaAdd, MetaArithBitMaskOp, MetaDiv, MetaEqual, MetaGeq, MetaGreater, MetaLeq, MetaLess, MetaMul, MetaPow, MetaShift, MetaSub

public abstract class AbstractTermTransformer
extends AbstractSortedOperator
implements TermTransformer

Abstract class factoring out commonalities of typical term transformer implementations. The available singletons of term transformers are kept here.

Field Summary

Fields

Modifier and Type	Field and Description
static AbstractTermTransformer	ADD_CAST
static AbstractTermTransformer	ARRAY_BASE_INSTANCE_OF
static AbstractTermTransformer	CONSTANT_VALUE
static AbstractTermTransformer	DIVIDE_LCR_MONOMIALS
static AbstractTermTransformer	DIVIDE_MONOMIALS
static AbstractTermTransformer	ENUM_CONSTANT_VALUE
static AbstractTermTransformer	EXPAND_QUERIES
static AbstractTermTransformer	INTRODUCE_ATPRE_DEFINITIONS
static AbstractTermTransformer	MEMBER_PV_TO_FIELD
static AbstractTermTransformer	META_ADD
static AbstractTermTransformer	META_AND
static AbstractTermTransformer	META_DIV
static AbstractTermTransformer	META_EQ
static AbstractTermTransformer	META_GEQ
static AbstractTermTransformer	META_GREATER
static AbstractTermTransformer	META_LEQ
static AbstractTermTransformer	META_LESS
static AbstractTermTransformer	META_MUL
static AbstractTermTransformer	META_OR
static AbstractTermTransformer	META_POW
static AbstractTermTransformer	META_SHIFTLEFT
static AbstractTermTransformer	META_SHIFTRIGHT
static AbstractTermTransformer	META_SUB
static AbstractTermTransformer	META_XOR
static Sort	METASORT
private static java.util.Map<java.lang.String,AbstractTermTransformer>	name2metaop

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	AbstractTermTransformer(Name name, int arity)
protected	AbstractTermTransformer(Name name, int arity, Sort sort)

Method Summary

Modifier and Type	Method and Description
static java.lang.String	convertToDecimalString(Term term, Services services)
private static Sort[]	createMetaSortArray(int arity)
static TermTransformer	name2metaop(java.lang.String s)

Methods inherited from class de.uka.ilkd.key.logic.op.AbstractSortedOperator

additionalValidTopLevel, additionalValidTopLevel2, argSort, argSorts, sort, sort

Methods inherited from class de.uka.ilkd.key.logic.op.AbstractOperator

arity, bindVarsAt, isRigid, name, toString, validTopLevel, whereToBind

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Methods inherited from interface de.uka.ilkd.key.logic.op.TermTransformer

transform

Methods inherited from interface de.uka.ilkd.key.logic.op.SortedOperator

argSort, argSorts, sort

Methods inherited from interface de.uka.ilkd.key.logic.op.Operator

arity, bindVarsAt, isRigid, sort, validTopLevel

Methods inherited from interface de.uka.ilkd.key.logic.Named

name

Field Detail

name2metaop

private static final java.util.Map<java.lang.String,AbstractTermTransformer> name2metaop

METASORT

public static final Sort METASORT

META_SHIFTRIGHT

public static final AbstractTermTransformer META_SHIFTRIGHT

META_SHIFTLEFT

public static final AbstractTermTransformer META_SHIFTLEFT

META_AND

public static final AbstractTermTransformer META_AND

META_OR

public static final AbstractTermTransformer META_OR

META_XOR

public static final AbstractTermTransformer META_XOR

META_ADD

public static final AbstractTermTransformer META_ADD

META_SUB

public static final AbstractTermTransformer META_SUB

META_MUL

public static final AbstractTermTransformer META_MUL

META_DIV

public static final AbstractTermTransformer META_DIV

META_POW

public static final AbstractTermTransformer META_POW

META_LESS

public static final AbstractTermTransformer META_LESS

META_GREATER

public static final AbstractTermTransformer META_GREATER

META_LEQ

public static final AbstractTermTransformer META_LEQ

META_GEQ

public static final AbstractTermTransformer META_GEQ

META_EQ

public static final AbstractTermTransformer META_EQ

ARRAY_BASE_INSTANCE_OF

public static final AbstractTermTransformer ARRAY_BASE_INSTANCE_OF

CONSTANT_VALUE

public static final AbstractTermTransformer CONSTANT_VALUE

ENUM_CONSTANT_VALUE

public static final AbstractTermTransformer ENUM_CONSTANT_VALUE

DIVIDE_MONOMIALS

public static final AbstractTermTransformer DIVIDE_MONOMIALS

DIVIDE_LCR_MONOMIALS

public static final AbstractTermTransformer DIVIDE_LCR_MONOMIALS

INTRODUCE_ATPRE_DEFINITIONS

public static final AbstractTermTransformer INTRODUCE_ATPRE_DEFINITIONS

MEMBER_PV_TO_FIELD

public static final AbstractTermTransformer MEMBER_PV_TO_FIELD

ADD_CAST

public static final AbstractTermTransformer ADD_CAST

EXPAND_QUERIES

public static final AbstractTermTransformer EXPAND_QUERIES

Constructor Detail

AbstractTermTransformer

protected AbstractTermTransformer(Name name,
                                  int arity,
                                  Sort sort)

AbstractTermTransformer

protected AbstractTermTransformer(Name name,
                                  int arity)

Method Detail

createMetaSortArray

private static Sort[] createMetaSortArray(int arity)

name2metaop

public static TermTransformer name2metaop(java.lang.String s)

convertToDecimalString

public static java.lang.String convertToDecimalString(Term term,
                                                      Services services)

Returns:

String representing a logical integer literal in decimal representation