java.lang.Object
- java.lang.Enum<FunctionDeclarationKind>
- - org.sosy_lab.java_smt.api.FunctionDeclarationKind

All Implemented Interfaces:

Serializable, Comparable<FunctionDeclarationKind>
```
public enum FunctionDeclarationKind
extends Enum<FunctionDeclarationKind>
```
Types of function declarations.

See Also:

FunctionDeclaration

Enum Constant Summary

Enum Constants
Enum Constant	Description
`ADD`	Addition over integers and rationals.
`AND`
`BV_ADD`	Addition over bitvectors.
`BV_AND`	Bitwise AND over bitvectors.
`BV_ASHR`	Arithmetic right-shift over bitvectors (fill from left with value of first bit).
`BV_CONCAT`	Concatenation over bitvectors.
`BV_EQ`	Equality over bitvectors.
`BV_EXTRACT`	Extraction over bitvectors.
`BV_LSHR`	Logical right-shift over bitvectors (fill from left with zeroes).
`BV_MUL`	Multiplication over bitvectors.
`BV_NEG`	Negation of a bitvector.
`BV_NOT`	Bitwise negation of a bitvector.
`BV_OR`	Bitwise OR over bitvectors.
`BV_SCASTTO_FP`	Cast a signed bitvector to a floating-point number.
`BV_SDIV`	Signed division over bitvectors.
`BV_SGE`	Signed greater-than-or-equal over bitvectors.
`BV_SGT`	Unsigned greater-than over bitvectors.
`BV_SHL`	Logical left-shift over bitvectors (fill from right with zeroes).
`BV_SIGN_EXTENSION`	Extend bitvectors according to their sign.
`BV_SLE`	Signed greater-than-or-equal over bitvectors.
`BV_SLT`	Unsigned less-than over bitvectors.
`BV_SMOD`	Signed modulo over bitvectors.
`BV_SREM`	Signed remainder over bitvectors.
`BV_SUB`	Subtraction over bitvectors.
`BV_UCASTTO_FP`	Cast an unsigned bitvector to a floating-point number.
`BV_UDIV`	Unsigned division over bitvectors.
`BV_UGE`	Unsigned greater-than-or-equal over bitvectors.
`BV_UGT`	Signed greater-than over bitvectors.
`BV_ULE`	Unsigned less-than-or-equal over bitvectors.
`BV_ULT`	Signed less-than over bitvectors.
`BV_UREM`	Unsigned remainder over bitvectors.
`BV_XOR`	Bitwise XOR over bitvectors.
`BV_ZERO_EXTENSION`	Extend bitvectors with zeros.
`CONST`
`DISTINCT`	Distinct operator for a set of numeric formulas.
`DIV`	Division over rationals and integer division over integers.
`EQ`	Equality over integers and rationals.
`EQ_ZERO`	Unary comparison to zero.
`FLOOR`	Floor operation, converts from rationals to integers, also known as `to_int`.
`FP_ABS`	Absolute value of a floating point.
`FP_ADD`	Addition over floating points.
`FP_AS_IEEEBV`
`FP_CASTTO_FP`
`FP_CASTTO_SBV`
`FP_CASTTO_UBV`
`FP_DIV`	Division over floating points.
`FP_EQ`	Equal over floating points.
`FP_FROM_IEEEBV`
`FP_GE`	Greater-than-or-equal over floating points.
`FP_GT`	Greater-than over floating points.
`FP_IS_INF`
`FP_IS_NAN`	Further FP queries.
`FP_IS_NEGATIVE`
`FP_IS_NORMAL`
`FP_IS_SUBNORMAL`
`FP_IS_ZERO`
`FP_LE`	Less-than-or-equal over floating points.
`FP_LT`	Less-than over floating points.
`FP_MAX`	Maximum of two floating points.
`FP_MIN`	Minimum of two floating points.
`FP_MUL`	Multiplication over floating points.
`FP_NEG`	Negation of a floating point.
`FP_ROUND_AWAY`	Rounding over floating points.
`FP_ROUND_EVEN`	Rounding over floating points.
`FP_ROUND_NEGATIVE`	Rounding over floating points.
`FP_ROUND_POSITIVE`	Rounding over floating points.
`FP_ROUND_TO_INTEGRAL`	Rounding over floating points.
`FP_ROUND_ZERO`	Rounding over floating points.
`FP_SQRT`	Square root of a floating point.
`FP_SUB`	Subtraction over floating points.
`GT`	Greater-than over integers and rationals.
`GTE`	Greater-than-or-equal over integers and rationals.
`GTE_ZERO`	Unary comparison with zero.
`IFF`	If and only if.
`IMPLIES`	Implication between two boolean formulas.
`INT_TO_STR`
`ITE`	If-then-else operator.
`LT`	Less-than over integers and rationals.
`LTE`	Less-than-or-equal over integers and rationals.
`MODULO`	Modulo operator over integers.
`MUL`	Multiplication over integers and rationals.
`NOT`
`OR`
`OTHER`	Solvers support a lot of different built-in theories.
`RE_COMPLEMENT`
`RE_CONCAT`
`RE_DIFFERENCE`
`RE_INTERSECT`
`RE_OPTIONAL`
`RE_PLUS`
`RE_RANGE`
`RE_STAR`
`RE_UNION`
`SELECT`
`STORE`	Store and select on arrays, and constant initialization.
`STR_CHAR_AT`
`STR_CONCAT`
`STR_CONTAINS`
`STR_IN_RE`
`STR_INDEX_OF`
`STR_LE`
`STR_LENGTH`
`STR_LT`
`STR_PREFIX`
`STR_REPLACE`
`STR_REPLACE_ALL`
`STR_SUBSTRING`
`STR_SUFFIX`
`STR_TO_INT`
`STR_TO_RE`
`SUB`	Subtraction over integers and rationals.
`TO_REAL`	Identity operation, converts from integers to rationals, also known as `to_real`.
`UF`	Uninterpreted function.
`UMINUS`	Unary minus.
`VAR`	User-defined variable.
`XOR`	Exclusive OR over two formulas.

Method Summary

All Methods Static Methods Concrete Methods
Modifier and Type	Method	Description
`static FunctionDeclarationKind`	`valueOf(String name)`	Returns the enum constant of this type with the specified name.
`static FunctionDeclarationKind[]`	`values()`	Returns an array containing the constants of this enum type, in the order they are declared.

Methods inherited from class java.lang.Enum
clone, compareTo, equals, finalize, getDeclaringClass, hashCode, name, ordinal, toString, valueOf

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

Enum Constant Detail

AND

public static final FunctionDeclarationKind AND

NOT

public static final FunctionDeclarationKind NOT

OR

public static final FunctionDeclarationKind OR

IFF

public static final FunctionDeclarationKind IFF

If and only if.

ITE

public static final FunctionDeclarationKind ITE

If-then-else operator.

XOR

public static final FunctionDeclarationKind XOR

Exclusive OR over two formulas.

IMPLIES

public static final FunctionDeclarationKind IMPLIES

Implication between two boolean formulas.

DISTINCT

public static final FunctionDeclarationKind DISTINCT

Distinct operator for a set of numeric formulas.

STORE
```
public static final FunctionDeclarationKind STORE
```
Store and select on arrays, and constant initialization.

SELECT

public static final FunctionDeclarationKind SELECT

CONST

public static final FunctionDeclarationKind CONST

UMINUS

public static final FunctionDeclarationKind UMINUS

Unary minus.

SUB

public static final FunctionDeclarationKind SUB

Subtraction over integers and rationals.

ADD

public static final FunctionDeclarationKind ADD

Addition over integers and rationals.

DIV
```
public static final FunctionDeclarationKind DIV
```
Division over rationals and integer division over integers.

MUL

public static final FunctionDeclarationKind MUL

Multiplication over integers and rationals.

MODULO

public static final FunctionDeclarationKind MODULO

Modulo operator over integers.

UF

public static final FunctionDeclarationKind UF

Uninterpreted function.

VAR

public static final FunctionDeclarationKind VAR

User-defined variable.

LT

public static final FunctionDeclarationKind LT

Less-than over integers and rationals.

LTE

public static final FunctionDeclarationKind LTE

Less-than-or-equal over integers and rationals.

GT

public static final FunctionDeclarationKind GT

Greater-than over integers and rationals.

GTE
```
public static final FunctionDeclarationKind GTE
```
Greater-than-or-equal over integers and rationals.

EQ
```
public static final FunctionDeclarationKind EQ
```
Equality over integers and rationals. Binary equality is modelled with IFF.

EQ_ZERO

public static final FunctionDeclarationKind EQ_ZERO

Unary comparison to zero.

GTE_ZERO

public static final FunctionDeclarationKind GTE_ZERO

Unary comparison with zero.

FLOOR
```
public static final FunctionDeclarationKind FLOOR
```
Floor operation, converts from rationals to integers, also known as to_int.

TO_REAL
```
public static final FunctionDeclarationKind TO_REAL
```
Identity operation, converts from integers to rationals, also known as to_real.

BV_EXTRACT

public static final FunctionDeclarationKind BV_EXTRACT

Extraction over bitvectors.

BV_CONCAT

public static final FunctionDeclarationKind BV_CONCAT

Concatenation over bitvectors.

BV_SIGN_EXTENSION

public static final FunctionDeclarationKind BV_SIGN_EXTENSION

Extend bitvectors according to their sign.

BV_ZERO_EXTENSION

public static final FunctionDeclarationKind BV_ZERO_EXTENSION

Extend bitvectors with zeros.

BV_NOT

public static final FunctionDeclarationKind BV_NOT

Bitwise negation of a bitvector.

BV_NEG

public static final FunctionDeclarationKind BV_NEG

Negation of a bitvector.

BV_OR

public static final FunctionDeclarationKind BV_OR

Bitwise OR over bitvectors.

BV_AND

public static final FunctionDeclarationKind BV_AND

Bitwise AND over bitvectors.

BV_XOR

public static final FunctionDeclarationKind BV_XOR

Bitwise XOR over bitvectors.

BV_SUB

public static final FunctionDeclarationKind BV_SUB

Subtraction over bitvectors.

BV_ADD

public static final FunctionDeclarationKind BV_ADD

Addition over bitvectors.

BV_SDIV

public static final FunctionDeclarationKind BV_SDIV

Signed division over bitvectors.

BV_UDIV

public static final FunctionDeclarationKind BV_UDIV

Unsigned division over bitvectors.

BV_SREM

public static final FunctionDeclarationKind BV_SREM

Signed remainder over bitvectors.

BV_UREM

public static final FunctionDeclarationKind BV_UREM

Unsigned remainder over bitvectors.

BV_SMOD

public static final FunctionDeclarationKind BV_SMOD

Signed modulo over bitvectors.

BV_MUL

public static final FunctionDeclarationKind BV_MUL

Multiplication over bitvectors.

BV_ULT

public static final FunctionDeclarationKind BV_ULT

Signed less-than over bitvectors.

BV_SLT

public static final FunctionDeclarationKind BV_SLT

Unsigned less-than over bitvectors.

BV_ULE

public static final FunctionDeclarationKind BV_ULE

Unsigned less-than-or-equal over bitvectors.

BV_SLE

public static final FunctionDeclarationKind BV_SLE

Signed greater-than-or-equal over bitvectors.

BV_UGT

public static final FunctionDeclarationKind BV_UGT

Signed greater-than over bitvectors.

BV_SGT

public static final FunctionDeclarationKind BV_SGT

Unsigned greater-than over bitvectors.

BV_UGE

public static final FunctionDeclarationKind BV_UGE

Unsigned greater-than-or-equal over bitvectors.

BV_SGE

public static final FunctionDeclarationKind BV_SGE

Signed greater-than-or-equal over bitvectors.

BV_EQ
```
public static final FunctionDeclarationKind BV_EQ
```
Equality over bitvectors. Binary equality is modeled with IFF.

BV_SHL
```
public static final FunctionDeclarationKind BV_SHL
```
Logical left-shift over bitvectors (fill from right with zeroes).

BV_LSHR
```
public static final FunctionDeclarationKind BV_LSHR
```
Logical right-shift over bitvectors (fill from left with zeroes).

BV_ASHR
```
public static final FunctionDeclarationKind BV_ASHR
```
Arithmetic right-shift over bitvectors (fill from left with value of first bit).

BV_UCASTTO_FP
```
public static final FunctionDeclarationKind BV_UCASTTO_FP
```
Cast an unsigned bitvector to a floating-point number.

BV_SCASTTO_FP
```
public static final FunctionDeclarationKind BV_SCASTTO_FP
```
Cast a signed bitvector to a floating-point number.

FP_NEG

public static final FunctionDeclarationKind FP_NEG

Negation of a floating point.

FP_ABS

public static final FunctionDeclarationKind FP_ABS

Absolute value of a floating point.

FP_MAX

public static final FunctionDeclarationKind FP_MAX

Maximum of two floating points.

FP_MIN

public static final FunctionDeclarationKind FP_MIN

Minimum of two floating points.

FP_SQRT

public static final FunctionDeclarationKind FP_SQRT

Square root of a floating point.

FP_SUB

public static final FunctionDeclarationKind FP_SUB

Subtraction over floating points.

FP_ADD

public static final FunctionDeclarationKind FP_ADD

Addition over floating points.

FP_DIV

public static final FunctionDeclarationKind FP_DIV

Division over floating points.

FP_MUL

public static final FunctionDeclarationKind FP_MUL

Multiplication over floating points.

FP_LT

public static final FunctionDeclarationKind FP_LT

Less-than over floating points.

FP_LE

public static final FunctionDeclarationKind FP_LE

Less-than-or-equal over floating points.

FP_GE

public static final FunctionDeclarationKind FP_GE

Greater-than-or-equal over floating points.

FP_GT

public static final FunctionDeclarationKind FP_GT

Greater-than over floating points.

FP_EQ

public static final FunctionDeclarationKind FP_EQ

Equal over floating points.