de.uka.ilkd.key.logic.op

Class AbstractSV

java.lang.Object

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

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

de.uka.ilkd.key.logic.op.AbstractSV

All Implemented Interfaces:

Named, Operator, ParsableVariable, SchemaVariable, SortedOperator, SVSubstitute, Sorted

Direct Known Subclasses:

FormulaSV, ModalOperatorSV, ProgramSV, SkolemTermSV, TermLabelSV, TermSV, UpdateSV, VariableSV

public abstract class AbstractSV
extends AbstractSortedOperator
implements SchemaVariable

Abstract base class for schema variables.

Field Summary

Fields

Modifier and Type	Field and Description
private boolean	isStrict

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	AbstractSV(Name name, ImmutableArray<Sort> argSorts, Sort sort, boolean isRigid, boolean isStrict)
protected	AbstractSV(Name name, Sort[] argSorts, Sort sort, boolean isRigid, boolean isStrict)
protected	AbstractSV(Name name, Sort sort, boolean isRigid, boolean isStrict)

Method Summary

Modifier and Type	Method and Description
boolean	isStrict()
protected java.lang.String	toString(java.lang.String sortSpec)

Methods inherited from class de.uka.ilkd.key.logic.op.AbstractSortedOperator

additionalValidTopLevel, additionalValidTopLevel2, argSort, argSorts, sort, sort

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.SchemaVariable

proofToString

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

Field Detail

isStrict

private final boolean isStrict

Constructor Detail

AbstractSV

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

AbstractSV

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

AbstractSV

protected AbstractSV(Name name,
                     Sort sort,
                     boolean isRigid,
                     boolean isStrict)

Method Detail

toString

protected final java.lang.String toString(java.lang.String sortSpec)

isStrict

public final boolean isStrict()

Specified by:

isStrict in interface SchemaVariable

Returns:

true if the schemavariable has the strict modifier which forces the instantiation to have exactly the same sort as the schemavariable (or if the sv is of generic sort - the instantiation of the generic sort)