de.uka.ilkd.key.logic.op

Interface TermTransformer

All Superinterfaces:

Named, Operator, SortedOperator, SVSubstitute

All Known Implementing Classes:

AbstractTermTransformer, AddCast, ArrayBaseInstanceOf, ConstantValue, DivideLCRMonomials, DivideMonomials, EnumConstantValue, ExpandQueriesMetaConstruct, IntroAtPreDefsOp, MemberPVToField, MetaAdd, MetaArithBitMaskOp, MetaBinaryAnd, MetaBinaryOr, MetaBinaryXOr, MetaDiv, MetaEqual, MetaGeq, MetaGreater, MetaLeq, MetaLess, MetaMul, MetaPow, MetaShift, MetaShiftLeft, MetaShiftRight, MetaSub

public interface TermTransformer
extends SortedOperator

TermTransformer perform complex term transformation which cannot be (efficiently or at all) described by taclets.

Method Summary

Modifier and Type	Method and Description
Term	transform(Term term, SVInstantiations svInst, Services services) initiates term transformation of term.

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

Method Detail

transform

Term transform(Term term,
               SVInstantiations svInst,
               Services services)

initiates term transformation of term. Note the top level operator of of parameter term has to be this term transformer.