de.uka.ilkd.key.logic.op

Class Function

java.lang.Object

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

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

de.uka.ilkd.key.logic.op.Function

All Implemented Interfaces:

Named, Operator, SortedOperator, SVSubstitute, Sorted

Direct Known Subclasses:

ObserverFunction, SortDependingFunction, Transformer

public class Function
extends AbstractSortedOperator

Objects of this class represent function and predicate symbols. Note that program variables are a separate syntactic category, and not a type of function.

Field Summary

Fields

Modifier and Type	Field and Description
private boolean	skolemConstant
private boolean	unique

Constructor Summary

Constructors

Constructor and Description
Function(Name name, Sort sort)
Function(Name name, Sort sort, boolean isSkolemConstant)
Function(Name name, Sort sort, boolean isSkolemConstant, Sort... argSorts)
Function(Name name, Sort sort, ImmutableArray<Sort> argSorts)
Function(Name name, Sort sort, ImmutableArray<Sort> argSorts, boolean isRigid)
Function(Name name, Sort sort, ImmutableArray<Sort> argSorts, ImmutableArray<java.lang.Boolean> whereToBind, boolean unique)
Function(Name name, Sort sort, ImmutableArray<Sort> argSorts, ImmutableArray<java.lang.Boolean> whereToBind, boolean unique, boolean isSkolemConstant)
Function(Name name, Sort sort, ImmutableArray<Sort> argSorts, ImmutableArray<java.lang.Boolean> whereToBind, boolean unique, boolean isRigid, boolean isSkolemConstant)
Function(Name name, Sort sort, Sort... argSorts)
Function(Name name, Sort sort, Sort[] argSorts, java.lang.Boolean[] whereToBind, boolean unique)
Function(Name name, Sort sort, Sort[] argSorts, java.lang.Boolean[] whereToBind, boolean unique, boolean isSkolemConstant)

Method Summary

Modifier and Type	Method and Description
boolean	isSkolemConstant()
boolean	isUnique() Indicates whether the function or predicate symbol has the "uniqueness" property.
java.lang.String	proofToString() Returns a parsable string representation of the declaration of this function or predicate symbol.
Function	rename(Name newName)
java.lang.String	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.Operator

arity, bindVarsAt, isRigid, validTopLevel

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

name

Field Detail

unique

private final boolean unique

skolemConstant

private final boolean skolemConstant

Constructor Detail

Function

Function(Name name,
         Sort sort,
         ImmutableArray<Sort> argSorts,
         ImmutableArray<java.lang.Boolean> whereToBind,
         boolean unique,
         boolean isRigid,
         boolean isSkolemConstant)

Function

public Function(Name name,
                Sort sort,
                ImmutableArray<Sort> argSorts,
                ImmutableArray<java.lang.Boolean> whereToBind,
                boolean unique)

Function

public Function(Name name,
                Sort sort,
                ImmutableArray<Sort> argSorts,
                ImmutableArray<java.lang.Boolean> whereToBind,
                boolean unique,
                boolean isSkolemConstant)

Function

public Function(Name name,
                Sort sort,
                Sort[] argSorts,
                java.lang.Boolean[] whereToBind,
                boolean unique)

Function

public Function(Name name,
                Sort sort,
                Sort[] argSorts,
                java.lang.Boolean[] whereToBind,
                boolean unique,
                boolean isSkolemConstant)

Function

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

Function

public Function(Name name,
                Sort sort,
                ImmutableArray<Sort> argSorts)

Function

public Function(Name name,
                Sort sort,
                Sort... argSorts)

Function

public Function(Name name,
                Sort sort,
                boolean isSkolemConstant,
                Sort... argSorts)

Function

public Function(Name name,
                Sort sort)

Function

public Function(Name name,
                Sort sort,
                boolean isSkolemConstant)

Method Detail

isUnique

public final boolean isUnique()

Indicates whether the function or predicate symbol has the "uniqueness" property. For two unique symbols f1: A1 -> B1, f2: A2 -> B2 by definition we have (1) f1(x) != f1(y) for all x, y in A1 with x != y (i.e., injectivity), and (2) f1(x) != f2(y) for all x in A1, y in A2.

isSkolemConstant

public final boolean isSkolemConstant()

toString

public final java.lang.String toString()

Overrides:

toString in class AbstractOperator

proofToString

public final java.lang.String proofToString()

Returns a parsable string representation of the declaration of this function or predicate symbol.

rename

public Function rename(Name newName)