FunctionSymbol (SMTInterpol 2.1 Public API)

java.lang.Object
- de.uni_freiburg.informatik.ultimate.logic.FunctionSymbol

```
public class FunctionSymbol
extends java.lang.Object
```
Represents a function symbol. Each function symbol has a name, a sort and zero or more parameter sorts. A constant symbol is represented as a function symbols with zero parameters. For parametric functions we create a different FunctionSymbol for every instantiation.

Author:

hoenicke

Field Summary

Fields
Modifier and Type	Field and Description
`static int`	`ASSOCMASK`
`static int`	`CHAINABLE`
`static int`	`INTERNAL`
`static int`	`LEFTASSOC`
`static int`	`MODELVALUE`
`static int`	`PAIRWISE`
`static int`	`RETURNOVERLOAD`
`static int`	`RIGHTASSOC`

Method Summary

All Methods Instance Methods Concrete Methods Deprecated Methods
Modifier and Type	Method and Description
`java.lang.String`	`getApplicationString()` Get the string representation of this function symbol as it would be used to build an application term.
`Term`	`getDefinition()` Retrieve the definition of this function symbol.
`TermVariable[]`	`getDefinitionVars()` Retrieve the variables used in the definition of this function symbol.
`java.math.BigInteger[]`	`getIndices()`
`java.lang.String`	`getName()` Get the name of the function.
`int`	`getParameterCount()` Deprecated. use getParameterSorts().length
`Sort`	`getParameterSort(int i)` Deprecated. use getParameterSorts()[i].
`Sort[]`	`getParameterSorts()` Get the sort of the parameters for this function.
`Sort`	`getReturnSort()` Get the return sort of this function.
`de.uni_freiburg.informatik.ultimate.logic.Theory`	`getTheory()`
`int`	`hashCode()`
`boolean`	`isChainable()` Checks if this function symbol was declared as chainable.
`boolean`	`isIntern()` Check whether this function symbol is created by the solver.
`boolean`	`isInterpreted()` Check whether this function symbol is an internal symbol that has a fixed semantic.
`boolean`	`isLeftAssoc()` Checks if this function symbol was declared as left associative.
`boolean`	`isModelValue()`
`boolean`	`isPairwise()` Checks if this function symbol was declared as pairwise.
`boolean`	`isReturnOverload()` Checks if this function symbol was created with the SMTLIB syntax `(as name sort)` to give it a different result sort.
`boolean`	`isRightAssoc()` Checks if this function symbol was declared as right associative.
`java.lang.String`	`toString()` Returns a string representation of this object.
`boolean`	`typecheck(Sort[] params)` Check if this function symbol can be called on terms with the given sort.
`void`	`typecheck(Term[] params)` Check if this function symbol can be called on the given argument terms.

Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, notify, notifyAll, wait, wait, wait

- Field Detail
  - INTERNAL
```
public static final int INTERNAL
```
    See Also:
    
    Constant Field Values
  - LEFTASSOC
```
public static final int LEFTASSOC
```
    See Also:
    
    Constant Field Values
  - RIGHTASSOC
```
public static final int RIGHTASSOC
```
    See Also:
    
    Constant Field Values
  - CHAINABLE
```
public static final int CHAINABLE
```
    See Also:
    
    Constant Field Values
  - PAIRWISE
```
public static final int PAIRWISE
```
    See Also:
    
    Constant Field Values
  - ASSOCMASK
```
public static final int ASSOCMASK
```
    See Also:
    
    Constant Field Values
  - RETURNOVERLOAD
```
public static final int RETURNOVERLOAD
```
    See Also:
    
    Constant Field Values
  - MODELVALUE
```
public static final int MODELVALUE
```
    See Also:
    
    Constant Field Values
- Method Detail
  - hashCode
```
public int hashCode()
```
    Overrides:
    
    hashCode in class java.lang.Object
  - getName
```
public java.lang.String getName()
```
    Get the name of the function. This is the name as used in an SMTLIB script. It can also contain symbols not allowed by the SMTLIB standard. In that case the string representation uses | to quote the name. The name may not contain | symbols.
    
    Returns:
    
    the name of the function.
  - getIndices
```
public java.math.BigInteger[] getIndices()
```
  - isIntern
```
public boolean isIntern()
```
    Check whether this function symbol is created by the solver. Symbols created by the solver are assumed to be special symbols like +, -, or internal symbols only used by the solver.
    
    Returns:
    
    true if and only if the function symbol was flagged as internal.
  - isModelValue
```
public boolean isModelValue()
```
  - getTheory
```
public de.uni_freiburg.informatik.ultimate.logic.Theory getTheory()
```
  - getParameterCount
```
@Deprecated
public int getParameterCount()
```
    Deprecated. use getParameterSorts().length
    
    Returns:
    
    the number of parameters this function takes.
  - getParameterSort
```
@Deprecated
public Sort getParameterSort(int i)
```
    Deprecated. use getParameterSorts()[i].
    
    Parameters:
    
    i - the parameter number.
    
    Returns:
    
    the sort of the ith parameter.
  - getDefinitionVars
```
public TermVariable[] getDefinitionVars()
```
    Retrieve the variables used in the definition of this function symbol. A definition only exists if the function symbol is a macro created by the define-fun command or a :named annotation.
    
    Returns:
    
    The variables used in the definition of this function symbol or null if this function symbol is not a macro.
  - getDefinition
```
public Term getDefinition()
```
    Retrieve the definition of this function symbol. A definition only exists if the function symbol is a macro created by the define-fun command or a :named annotation.
    
    Returns:
    
    The definition of this function symbol or null if this function symbol is not a macro.
  - getReturnSort
```
public Sort getReturnSort()
```
    Get the return sort of this function.
    
    Returns:
    
    the return sort.
  - getParameterSorts
```
public Sort[] getParameterSorts()
```
    Get the sort of the parameters for this function.
    
    Returns:
    
    An array with the parameter sorts. Never write to this array!
  - typecheck
```
public void typecheck(Term[] params)
               throws SMTLIBException
```
    Check if this function symbol can be called on the given argument terms. This throws an exception if the type check fails.
    
    Parameters:
    
    params - the arguments for the function symbols.
    
    Throws:
    
    SMTLIBException
  - typecheck
```
public boolean typecheck(Sort[] params)
```
    Check if this function symbol can be called on terms with the given sort.
    
    Parameters:
    
    params - the sort of the arguments for the function symbols.
    
    Returns:
    
    true if the type check succeeds, false otherwise.
  - toString
```
public java.lang.String toString()
```
    Returns a string representation of this object. This is a SMTLIB like representation of the following form:
```
(name paramsort1 ... paramsortn returnsort)
```
    where name is the (possibly indexed and quoted) function name.
    Overrides:
    
    toString in class java.lang.Object
  - isChainable
```
public final boolean isChainable()
```
    Checks if this function symbol was declared as chainable. This should only be true for the internal equality function.
    
    Returns:
    
    true if the function symbol is chainable.
  - isPairwise
```
public final boolean isPairwise()
```
    Checks if this function symbol was declared as pairwise. This should only be true for the internal distinct function.
    
    Returns:
    
    true if the function symbol is pairwise.
  - isLeftAssoc
```
public final boolean isLeftAssoc()
```
    Checks if this function symbol was declared as left associative. This should only be true for internal function symbols.
    
    Returns:
    
    true if the function symbol is left associative.
  - isRightAssoc
```
public final boolean isRightAssoc()
```
    Checks if this function symbol was declared as right associative. This should only be true for internal function symbols.
    
    Returns:
    
    true if the function symbol is right associative.
  - isReturnOverload
```
public final boolean isReturnOverload()
```
    Checks if this function symbol was created with the SMTLIB syntax (as name sort) to give it a different result sort.
    
    Returns:
    
    true if the sort was explicitly given, false if it is implicit.
  - getApplicationString
```
public java.lang.String getApplicationString()
```
    Get the string representation of this function symbol as it would be used to build an application term.
    
    Returns:
    
    the string representation.
  - isInterpreted
```
public boolean isInterpreted()
```
    Check whether this function symbol is an internal symbol that has a fixed semantic.
    
    Returns:
    
    true if and only if the symbol is an internal symbol with a fixed semantic.

Class FunctionSymbol

Field Summary

Method Summary

Methods inherited from class java.lang.Object

Field Detail

INTERNAL

LEFTASSOC

RIGHTASSOC

CHAINABLE

PAIRWISE

ASSOCMASK

RETURNOVERLOAD

MODELVALUE

Method Detail

hashCode

getName

getIndices

isIntern

isModelValue

getTheory

getParameterCount

getParameterSort

getDefinitionVars

getDefinition

getReturnSort

getParameterSorts

typecheck

typecheck

toString

isChainable

isPairwise

isLeftAssoc

isRightAssoc

isReturnOverload

getApplicationString

isInterpreted