de.uka.ilkd.key.logic.op

Class SubstOp

java.lang.Object

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

de.uka.ilkd.key.logic.op.SubstOp

All Implemented Interfaces:

Named, Operator, SVSubstitute

Direct Known Subclasses:

WarySubstOp

public abstract class SubstOp
extends AbstractOperator

Standard first-order substitution operator, resolving clashes but not preventing (usually unsound) substitution of non-rigid terms across modal operators. Currently, only the subclass WarySubstOp is used and accessible through the key parser.

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	SubstOp(Name name)

Method Summary

Modifier and Type	Method and Description
protected boolean	additionalValidTopLevel(Term term) Allows subclasses to impose custom demands on what constitutes a valid term using the operator represented by the subclass.
abstract Term	apply(Term term, TermBuilder tb) Apply this substitution operator to term, which has this operator as top-level operator
Sort	sort(ImmutableArray<Term> terms) 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.

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

Constructor Detail

SubstOp

protected SubstOp(Name name)

Method Detail

sort

public Sort sort(ImmutableArray<Term> terms)

Description copied from interface: Operator

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:

terms - an array of Term containing the subterms of a (potential) term with this operator as top level operator

Returns:

sort of the second subterm or throws an IllegalArgumentException if the given term has no correct (2=) arity

additionalValidTopLevel

protected boolean additionalValidTopLevel(Term term)

Description copied from class: AbstractOperator

Allows subclasses to impose custom demands on what constitutes a valid term using the operator represented by the subclass.

Specified by:

additionalValidTopLevel in class AbstractOperator

Returns:

true iff the sort of the subterm 0 of the given term has the same sort as or a subsort of the variable to be substituted and the term's arity is 2 and the numer of variables bound there is 0 for the 0th subterm and 1 for the 1st subterm.

apply

public abstract Term apply(Term term,
                           TermBuilder tb)

Apply this substitution operator to term, which has this operator as top-level operator

Parameters:

term - the Term on which to apply the substitution

tb - the TermBuilder to use for term construction