de.uka.ilkd.key.logic.op

Class AbstractOperator

java.lang.Object

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

All Implemented Interfaces:

Named, Operator, SVSubstitute

Direct Known Subclasses:

AbstractSortedOperator, IfExThenElse, IfThenElse, SubstOp, UpdateApplication

abstract class AbstractOperator
extends java.lang.Object
implements Operator

Abstract operator class offering some common functionality.

Field Summary

Fields

Modifier and Type	Field and Description
private int	arity
private boolean	isRigid
private Name	name
private ImmutableArray<java.lang.Boolean>	whereToBind

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	AbstractOperator(Name name, int arity, boolean isRigid)
protected	AbstractOperator(Name name, int arity, java.lang.Boolean[] whereToBind, boolean isRigid)
protected	AbstractOperator(Name name, int arity, ImmutableArray<java.lang.Boolean> whereToBind, boolean isRigid)

Method Summary

Modifier and Type	Method and Description
protected abstract boolean	additionalValidTopLevel(Term term) Allows subclasses to impose custom demands on what constitutes a valid term using the operator represented by the subclass.
int	arity() the arity of this operator
boolean	bindVarsAt(int n) Tells whether the operator binds variables at the n-th subterm.
boolean	isRigid() Tells whether the operator is rigid.
Name	name() returns the name of this element
java.lang.String	toString()
boolean	validTopLevel(Term term) 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.
protected ImmutableArray<java.lang.Boolean>	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.Operator

sort

Field Detail

name

private final Name name

arity

private final int arity

whereToBind

private final ImmutableArray<java.lang.Boolean> whereToBind

isRigid

private final boolean isRigid

Constructor Detail

AbstractOperator

protected AbstractOperator(Name name,
                           int arity,
                           ImmutableArray<java.lang.Boolean> whereToBind,
                           boolean isRigid)

AbstractOperator

protected AbstractOperator(Name name,
                           int arity,
                           java.lang.Boolean[] whereToBind,
                           boolean isRigid)

AbstractOperator

protected AbstractOperator(Name name,
                           int arity,
                           boolean isRigid)

Method Detail

whereToBind

protected final ImmutableArray<java.lang.Boolean> whereToBind()

name

public final Name name()

Description copied from interface: Named

returns the name of this element

Specified by:

name in interface Named

Returns:

the name of the element

arity

public final int arity()

Description copied from interface: Operator

the arity of this operator

Specified by:

arity in interface Operator

bindVarsAt

public final boolean bindVarsAt(int n)

Description copied from interface: Operator

Tells whether the operator binds variables at the n-th subterm.

Specified by:

bindVarsAt in interface Operator

isRigid

public final boolean isRigid()

Description copied from interface: Operator

Tells whether the operator is rigid.

Specified by:

isRigid in interface Operator

additionalValidTopLevel

protected abstract boolean additionalValidTopLevel(Term term)

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

validTopLevel

public boolean validTopLevel(Term term)

Description copied from interface: Operator

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.

Specified by:

validTopLevel in interface Operator

Returns:

true iff the top level structure of the Term is valid.

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object