de.uka.ilkd.key.logic.op

Class AbstractSortedOperator

java.lang.Object

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

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

All Implemented Interfaces:

Named, Operator, SortedOperator, SVSubstitute, Sorted

Direct Known Subclasses:

AbstractSV, AbstractTermTransformer, ElementaryUpdate, Equality, Function, Junctor, LogicVariable, Metavariable, Modality, ProgramVariable, Quantifier, UpdateJunctor

public abstract class AbstractSortedOperator
extends AbstractOperator
implements SortedOperator, Sorted

Abstract sorted operator class offering some common functionality.

Field Summary

Fields

Modifier and Type	Field and Description
private ImmutableArray<Sort>	argSorts
private static ImmutableArray<Sort>	EMPTY_SORT_LIST
private Sort	sort

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	AbstractSortedOperator(Name name, ImmutableArray<Sort> argSorts, Sort sort, boolean isRigid)
protected	AbstractSortedOperator(Name name, ImmutableArray<Sort> argSorts, Sort sort, ImmutableArray<java.lang.Boolean> whereToBind, boolean isRigid)
protected	AbstractSortedOperator(Name name, Sort[] argSorts, Sort sort, boolean isRigid)
protected	AbstractSortedOperator(Name name, Sort[] argSorts, Sort sort, java.lang.Boolean[] whereToBind, boolean isRigid)
protected	AbstractSortedOperator(Name name, Sort sort, boolean isRigid)

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.
protected boolean	additionalValidTopLevel2(Term term) Allows subclasses to impose custom demands on what constitutes a valid term using the operator represented by the subclass.
Sort	argSort(int i)
ImmutableArray<Sort>	argSorts()
private boolean	possibleSub(int at, Term possibleSub) checks if a given Term could be subterm (at the at'th subterm position) of a term with this function at its top level.
Sort	sort()
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

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

arity, bindVarsAt, isRigid, validTopLevel

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

name

Field Detail

EMPTY_SORT_LIST

private static final ImmutableArray<Sort> EMPTY_SORT_LIST

sort

private final Sort sort

argSorts

private final ImmutableArray<Sort> argSorts

Constructor Detail

AbstractSortedOperator

protected AbstractSortedOperator(Name name,
                                 ImmutableArray<Sort> argSorts,
                                 Sort sort,
                                 ImmutableArray<java.lang.Boolean> whereToBind,
                                 boolean isRigid)

AbstractSortedOperator

protected AbstractSortedOperator(Name name,
                                 Sort[] argSorts,
                                 Sort sort,
                                 java.lang.Boolean[] whereToBind,
                                 boolean isRigid)

AbstractSortedOperator

protected AbstractSortedOperator(Name name,
                                 ImmutableArray<Sort> argSorts,
                                 Sort sort,
                                 boolean isRigid)

AbstractSortedOperator

protected AbstractSortedOperator(Name name,
                                 Sort[] argSorts,
                                 Sort sort,
                                 boolean isRigid)

AbstractSortedOperator

protected AbstractSortedOperator(Name name,
                                 Sort sort,
                                 boolean isRigid)

Method Detail

sort

public final 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.

Specified by:

sort in interface Operator

Parameters:

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

Returns:

sort of the term with this operator as top level operator of the given substerms

possibleSub

private boolean possibleSub(int at,
                            Term possibleSub)

checks if a given Term could be subterm (at the at'th subterm position) of a term with this function at its top level. The validity of the given subterm is NOT checked.

Parameters:

at - theposition of the term where this method should check the validity.

possibleSub - the subterm to be ckecked.

Returns:

true iff the given term can be subterm at the indicated position

additionalValidTopLevel2

protected boolean additionalValidTopLevel2(Term term)

Allows subclasses to impose custom demands on what constitutes a valid term using the operator represented by the subclass. The default implementation here does not impose any such demands.

additionalValidTopLevel

protected final 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

argSort

public final Sort argSort(int i)

Specified by:

argSort in interface SortedOperator

argSorts

public final ImmutableArray<Sort> argSorts()

Specified by:

argSorts in interface SortedOperator

sort

public final Sort sort()

Specified by:

sort in interface SortedOperator

Specified by:

sort in interface Sorted