Logics (SMTInterpol 2.1 Public API)

java.lang.Object
- java.lang.Enum<Logics>
- - de.uni_freiburg.informatik.ultimate.logic.Logics

All Implemented Interfaces:

java.io.Serializable, java.lang.Comparable<Logics>
```
public enum Logics
extends java.lang.Enum<Logics>
```
All logics configured in SMTLIB and some extensions supported by SMTInterpol.

Author:

Juergen Christ

Enum Constant Summary

Enum Constants
Enum Constant and Description
`ALIA`
`ALL`
`AUFLIA`
`AUFLIRA`
`AUFNIRA`
`BV`
`BVFP`
`CORE`
`FP`
`LIA`
`LRA`
`NIA`
`NRA`
`QF_ABV`
`QF_ALIA`
`QF_AUFBV`
`QF_AUFLIA`
`QF_AUFLIRA`
`QF_AX`
`QF_BV`
`QF_BVFP`
`QF_FP`
`QF_IDL`
`QF_LIA`
`QF_LIRA`
`QF_LRA`
`QF_NIA`
`QF_NRA`
`QF_RDL`
`QF_UF`
`QF_UFBV`
`QF_UFIDL`
`QF_UFLIA`
`QF_UFLIRA`
`QF_UFLRA`
`QF_UFNIA`
`QF_UFNRA`
`UF`
`UFBV`
`UFIDL`
`UFLIA`
`UFLRA`
`UFNIA`

Method Summary

All Methods Static Methods Instance Methods Concrete Methods
Modifier and Type	Method and Description
`boolean`	`hasIntegers()` Does this logic have integers?
`boolean`	`hasReals()` Does this logic have real numbers?
`boolean`	`isArithmetic()` Does this logic support arithmetic operators?
`boolean`	`isArray()` Does this logic support arrays?
`boolean`	`isBitVector()` Does this logic support bit vectors?
`boolean`	`isDifferenceLogic()` Does this logic support difference logic?
`boolean`	`isFloatingPoint()` Does this logic support floating point arithmetic?
`boolean`	`isIRA()` Is this logic mixed integer and real?
`boolean`	`isLinearArithmetic()` Does this logic support linear arithmetic?
`boolean`	`isNonLinearArithmetic()` Does this logic support non-linear arithmetic?
`boolean`	`isQuantified()` Does this logic support quantifiers?
`boolean`	`isUF()` Does this logic support uninterpreted functions and sorts?
`static Logics`	`valueOf(java.lang.String name)` Returns the enum constant of this type with the specified name.
`static Logics[]`	`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
  - CORE
```
public static final Logics CORE
```
  - ALL
```
public static final Logics ALL
```
  - QF_BV
```
public static final Logics QF_BV
```
  - QF_FP
```
public static final Logics QF_FP
```
  - QF_BVFP
```
public static final Logics QF_BVFP
```
  - QF_IDL
```
public static final Logics QF_IDL
```
  - QF_RDL
```
public static final Logics QF_RDL
```
  - QF_LIA
```
public static final Logics QF_LIA
```
  - QF_LRA
```
public static final Logics QF_LRA
```
  - QF_LIRA
```
public static final Logics QF_LIRA
```
  - QF_NIA
```
public static final Logics QF_NIA
```
  - QF_NRA
```
public static final Logics QF_NRA
```
  - QF_UF
```
public static final Logics QF_UF
```
  - QF_UFBV
```
public static final Logics QF_UFBV
```
  - QF_UFIDL
```
public static final Logics QF_UFIDL
```
  - QF_UFLIA
```
public static final Logics QF_UFLIA
```
  - QF_UFLRA
```
public static final Logics QF_UFLRA
```
  - QF_UFLIRA
```
public static final Logics QF_UFLIRA
```
  - QF_UFNIA
```
public static final Logics QF_UFNIA
```
  - QF_UFNRA
```
public static final Logics QF_UFNRA
```
  - QF_AX
```
public static final Logics QF_AX
```
  - QF_ABV
```
public static final Logics QF_ABV
```
  - QF_AUFBV
```
public static final Logics QF_AUFBV
```
  - QF_ALIA
```
public static final Logics QF_ALIA
```
  - QF_AUFLIA
```
public static final Logics QF_AUFLIA
```
  - QF_AUFLIRA
```
public static final Logics QF_AUFLIRA
```
  - BV
```
public static final Logics BV
```
  - FP
```
public static final Logics FP
```
  - BVFP
```
public static final Logics BVFP
```
  - LIA
```
public static final Logics LIA
```
  - LRA
```
public static final Logics LRA
```
  - NIA
```
public static final Logics NIA
```
  - NRA
```
public static final Logics NRA
```
  - UF
```
public static final Logics UF
```
  - UFBV
```
public static final Logics UFBV
```
  - UFIDL
```
public static final Logics UFIDL
```
  - UFLIA
```
public static final Logics UFLIA
```
  - UFLRA
```
public static final Logics UFLRA
```
  - UFNIA
```
public static final Logics UFNIA
```
  - ALIA
```
public static final Logics ALIA
```
  - AUFLIA
```
public static final Logics AUFLIA
```
  - AUFLIRA
```
public static final Logics AUFLIRA
```
  - AUFNIRA
```
public static final Logics AUFNIRA
```
- Method Detail
  - values
```
public static Logics[] values()
```
    Returns an array containing the constants of this enum type, in the order they are declared. This method may be used to iterate over the constants as follows:
```
for (Logics c : Logics.values())
    System.out.println(c);
```
    Returns:
    
    an array containing the constants of this enum type, in the order they are declared
  - valueOf
```
public static Logics valueOf(java.lang.String name)
```
    Returns the enum constant of this type with the specified name. The string must match exactly an identifier used to declare an enum constant in this type. (Extraneous whitespace characters are not permitted.)
    
    Parameters:
    
    name - the name of the enum constant to be returned.
    
    Returns:
    
    the enum constant with the specified name
    
    Throws:
    
    java.lang.IllegalArgumentException - if this enum type has no constant with the specified name
    
    java.lang.NullPointerException - if the argument is null
  - isIRA
```
public boolean isIRA()
```
    Is this logic mixed integer and real?
    
    Returns:
    
    true if and only if mixed arithmetic can be used in this logic.
  - isUF
```
public boolean isUF()
```
    Does this logic support uninterpreted functions and sorts?
    
    Returns:
    
    true if and only if the logic supports uninterpreted functions and sorts.
  - isArray
```
public boolean isArray()
```
    Does this logic support arrays?
    
    Returns:
    
    true if and only if this logic supports arrays.
  - isBitVector
```
public boolean isBitVector()
```
    Does this logic support bit vectors?
    
    Returns:
    
    true if and only if this logic supports bit vectors.
  - isQuantified
```
public boolean isQuantified()
```
    Does this logic support quantifiers?
    
    Returns:
    
    true if and only if quantified formulas can be build in this logic.
  - isArithmetic
```
public boolean isArithmetic()
```
    Does this logic support arithmetic operators?
    
    Returns:
    
    true if and only if this logic supports arithmetic
  - isDifferenceLogic
```
public boolean isDifferenceLogic()
```
    Does this logic support difference logic?
    
    Returns:
    
    true if and only if this logic support difference logic; it returns false for linear arithmetic and non-linear arithmetic logics.
  - isLinearArithmetic
```
public boolean isLinearArithmetic()
```
    Does this logic support linear arithmetic?
    
    Returns:
    
    true if and only if this logic support difference logic; it returns false for nonlinear arithmetic logics.
  - isNonLinearArithmetic
```
public boolean isNonLinearArithmetic()
```
    Does this logic support non-linear arithmetic?
    
    Returns:
    
    true if and only if this logic support non-linear logic.
  - hasIntegers
```
public boolean hasIntegers()
```
    Does this logic have integers?
    
    Returns:
    
    true if and only if this logic has integers.
  - hasReals
```
public boolean hasReals()
```
    Does this logic have real numbers?
    
    Returns:
    
    true if and only if this logic has reals.
  - isFloatingPoint
```
public boolean isFloatingPoint()
```
    Does this logic support floating point arithmetic?
    
    Returns:
    
    true if and only if this logic supports floating point arithmetic.

Enum Logics

Enum Constant Summary

Method Summary

Methods inherited from class java.lang.Enum

Methods inherited from class java.lang.Object

Enum Constant Detail

CORE

ALL

QF_BV

QF_FP

QF_BVFP

QF_IDL

QF_RDL

QF_LIA

QF_LRA

QF_LIRA

QF_NIA

QF_NRA

QF_UF

QF_UFBV

QF_UFIDL

QF_UFLIA

QF_UFLRA

QF_UFLIRA

QF_UFNIA

QF_UFNRA

QF_AX

QF_ABV

QF_AUFBV

QF_ALIA

QF_AUFLIA

QF_AUFLIRA

BV

FP

BVFP

LIA

LRA

NIA

NRA

UF

UFBV

UFIDL

UFLIA

UFLRA

UFNIA

ALIA

AUFLIA

AUFLIRA

AUFNIRA

Method Detail

values

valueOf

isIRA

isUF

isArray

isBitVector

isQuantified

isArithmetic

isDifferenceLogic

isLinearArithmetic

isNonLinearArithmetic

hasIntegers

hasReals

isFloatingPoint