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 |
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.
|
public static final Logics CORE
public static final Logics ALL
public static final Logics QF_BV
public static final Logics QF_FP
public static final Logics QF_BVFP
public static final Logics QF_IDL
public static final Logics QF_RDL
public static final Logics QF_LIA
public static final Logics QF_LRA
public static final Logics QF_LIRA
public static final Logics QF_NIA
public static final Logics QF_NRA
public static final Logics QF_UF
public static final Logics QF_UFBV
public static final Logics QF_UFIDL
public static final Logics QF_UFLIA
public static final Logics QF_UFLRA
public static final Logics QF_UFLIRA
public static final Logics QF_UFNIA
public static final Logics QF_UFNRA
public static final Logics QF_AX
public static final Logics QF_ABV
public static final Logics QF_AUFBV
public static final Logics QF_ALIA
public static final Logics QF_AUFLIA
public static final Logics QF_AUFLIRA
public static final Logics BV
public static final Logics FP
public static final Logics BVFP
public static final Logics LIA
public static final Logics LRA
public static final Logics NIA
public static final Logics NRA
public static final Logics UF
public static final Logics UFBV
public static final Logics UFIDL
public static final Logics UFLIA
public static final Logics UFLRA
public static final Logics UFNIA
public static final Logics ALIA
public static final Logics AUFLIA
public static final Logics AUFLIRA
public static final Logics AUFNIRA
public static Logics[] values()
for (Logics c : Logics.values()) System.out.println(c);
public static Logics valueOf(java.lang.String name)
name
- the name of the enum constant to be returned.java.lang.IllegalArgumentException
- if this enum type has no constant with the specified namejava.lang.NullPointerException
- if the argument is nullpublic boolean isIRA()
true
if and only if mixed arithmetic can be used in
this logic.public boolean isUF()
true
if and only if the logic supports uninterpreted
functions and sorts.public boolean isArray()
true
if and only if this logic supports arrays.public boolean isBitVector()
true
if and only if this logic supports bit vectors.public boolean isQuantified()
true
if and only if quantified formulas can be build
in this logic.public boolean isArithmetic()
true
if and only if this logic supports arithmeticpublic boolean isDifferenceLogic()
true
if and only if this logic support difference
logic;
it returns false for linear arithmetic and non-linear arithmetic logics.public boolean isLinearArithmetic()
true
if and only if this logic support difference
logic; it returns false for nonlinear arithmetic logics.public boolean isNonLinearArithmetic()
true
if and only if this logic support non-linear
logic.public boolean hasIntegers()
true
if and only if this logic has integers.public boolean hasReals()
true
if and only if this logic has reals.public boolean isFloatingPoint()
true
if and only if this logic supports floating
point arithmetic.