de.uka.ilkd.key.logic.op

Class TermSV

java.lang.Object

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

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

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

de.uka.ilkd.key.logic.op.TermSV

All Implemented Interfaces:

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

public final class TermSV
extends AbstractSV

A schema variable that is used as placeholder for terms.

Constructor Summary

Constructors

Constructor and Description
TermSV(Name name, Sort sort, boolean isRigid, boolean isStrict)

Method Summary

Modifier and Type	Method and Description
java.lang.String	proofToString() Creates a parseable string representation of the declaration of the schema variable.
java.lang.String	toString()

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

isStrict, toString

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

Constructor Detail

TermSV

TermSV(Name name,
       Sort sort,
       boolean isRigid,
       boolean isStrict)

Parameters:

name - the name of the schema variable

sort - the sort of the schema variable

isRigid - true iff this schema variable may only match rigid terms

isStrict - boolean indicating if the schema variable is declared as strict forcing exact type match

Method Detail

toString

public java.lang.String toString()

Overrides:

toString in class AbstractOperator

proofToString

public java.lang.String proofToString()

Description copied from interface: SchemaVariable

Creates a parseable string representation of the declaration of the schema variable.