| java.lang.Object
 de.uka.ilkd.key.logic.op.Op
de.uka.ilkd.key.logic.op.AbstractMetaOperator
All known Subclasses: de.uka.ilkd.key.rule.metaconstruct.arith.MetaJavaIntXor, de.uka.ilkd.key.rule.metaconstruct.arith.MetaMul, de.uka.ilkd.key.rule.metaconstruct.CreateInReachableStatePO, de.uka.ilkd.key.rule.metaconstruct.arith.MetaGeq, de.uka.ilkd.key.rule.metaconstruct.arith.MetaSub, de.uka.ilkd.key.rule.metaconstruct.arith.MetaJavaLongAnd, de.uka.ilkd.key.rule.metaconstruct.MetaField, de.uka.ilkd.key.rule.metaconstruct.MetaAllSubtypes, de.uka.ilkd.key.rule.metaconstruct.MetaTransient, de.uka.ilkd.key.rule.metaconstruct.MetaEquivalentUpdates, de.uka.ilkd.key.rule.metaconstruct.ArrayBaseInstanceOf, de.uka.ilkd.key.rule.metaconstruct.arith.MetaDiv, de.uka.ilkd.key.rule.metaconstruct.arith.MetaJavaIntAnd, de.uka.ilkd.key.rule.metaconstruct.arith.MetaJavaLongUnsignedShiftRight, de.uka.ilkd.key.rule.metaconstruct.ConstantValue, de.uka.ilkd.key.rule.metaconstruct.LocationDependentFunction, de.uka.ilkd.key.rule.metaconstruct.arith.DivideMonomials, de.uka.ilkd.key.rule.metaconstruct.ExpandDynamicType, de.uka.ilkd.key.rule.metaconstruct.arith.MetaJavaLongShiftRight, de.uka.ilkd.key.rule.metaconstruct.arith.DivideLCRMonomials, de.uka.ilkd.key.rule.metaconstruct.Universes, de.uka.ilkd.key.rule.metaconstruct.arith.MetaLess, de.uka.ilkd.key.rule.metaconstruct.arith.MetaJavaLongOr, de.uka.ilkd.key.rule.metaconstruct.ResolveQuery, de.uka.ilkd.key.rule.metaconstruct.arith.MetaJavaLongXor, de.uka.ilkd.key.rule.metaconstruct.MetaShadow, de.uka.ilkd.key.rule.metaconstruct.IntroNewAnonUpdateOp, de.uka.ilkd.key.rule.metaconstruct.arith.MetaJavaIntShiftLeft, de.uka.ilkd.key.rule.metaconstruct.ArrayStoreStaticAnalyse, de.uka.ilkd.key.rule.metaconstruct.arith.MetaJavaIntShiftRight, de.uka.ilkd.key.rule.metaconstruct.arith.MetaJavaIntOr, de.uka.ilkd.key.rule.metaconstruct.WhileInvRule, de.uka.ilkd.key.rule.metaconstruct.arith.MetaGreater, de.uka.ilkd.key.rule.metaconstruct.arith.MetaJavaLongShiftLeft, de.uka.ilkd.key.rule.metaconstruct.arith.MetaEqual, de.uka.ilkd.key.rule.metaconstruct.arith.MetaAdd, de.uka.ilkd.key.rule.metaconstruct.arith.MetaLeq, de.uka.ilkd.key.rule.metaconstruct.AtPreEquations, de.uka.ilkd.key.rule.metaconstruct.arith.MetaJavaIntUnsignedShiftRight,
| AbstractMetaOperator | | abstract public class AbstractMetaOperator extends Op implements MetaOperator(Code) | | this class implements the interface for
MetaOperators. MetaOperators are used to do complex term
transformation when applying a taclet. Often these transformation
caanot be described with the taclet scheme (or trying to do so would
result in a huge number of rules)
|
| AbstractMetaOperator | | public AbstractMetaOperator(Name name, int arity)(Code) | | |
| arity | | public int arity()(Code) | | arity of the Operator as int |
| convertToDecimalString | | public static String convertToDecimalString(Term term, Services services)(Code) | | String representing a logical integer literal in decimal representation |
| sort | | public Sort sort(Term[] term)(Code) | | determines the sort of the
Term if it would be created using this
Operator as top level operator and the given terms as sub terms. The
assumption that the constructed term would be allowed is not checked.
Parameters:
term - an array of Term containing the subterms of a (potential)term with this operator as top level operator sort of the term with this operator as top level operator of thegiven substerms |
| validTopLevel | | public boolean validTopLevel(Term term)(Code) | | 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. The
assumption that the top level operator and the term are equal
is NOT checked.
true iff the top level structure ofthe @link Term is valid. |
|
|