LogicKind enum

Inheritance

• Object
• Enum
• LogicKind

Constructors

LogicKind(String smtlibName)

const

Values

all → const LogicKind

Use all logics available.

const LogicKind('ALL')

qfRdl → const LogicKind

Difference Logic over the reals. In essence, Boolean combinations of inequations of the form x - y < b where x and y are real variables and b is a rational constant.

const LogicKind('QF_RDL')

qfLra → const LogicKind

Unquantified linear real arithmetic. In essence, Boolean combinations of inequations between linear polynomials over real variables.

const LogicKind('QF_LRA')

uflra → const LogicKind

Linear real arithmetic with uninterpreted sort and function symbols.

const LogicKind('UFLRA')

lra → const LogicKind

Closed linear formulas in linear real arithmetic.

const LogicKind('LRA')

rdl → const LogicKind

Difference Logic over the reals (in essence) but with uninterpreted sort and function symbols.

const LogicKind('RDL')

nra → const LogicKind

const LogicKind('NRA')

qfNra → const LogicKind

Quantifier-free real arithmetic.

const LogicKind('QF_NRA')

qfUfnra → const LogicKind

Unquantified non-linear real arithmetic with uninterpreted sort and function symbols.

const LogicKind('QF_UFNRA')

qfUflra → const LogicKind

Unquantified linear real arithmetic with uninterpreted sort and function symbols.

const LogicKind('QF_UFLRA')

qfLia → const LogicKind

Unquantified linear integer arithmetic. In essence, Boolean combinations of inequations between linear polynomials over integer variables.

const LogicKind('QF_LIA')

qfIdl → const LogicKind

Difference Logic over the integers. In essence, Boolean combinations of inequations of the form x - y < b where x and y are integer variables and b is an integer constant.

const LogicKind('QF_IDL')

qfAuflia → const LogicKind

Closed quantifier-free linear formulas over the theory of integer arrays extended with free sort and function symbols.

const LogicKind('QF_AUFLIA')

qfAlia → const LogicKind

const LogicKind('QF_ALIA')

qfAuflira → const LogicKind

const LogicKind('QF_AUFLIRA')

qfAufnia → const LogicKind

const LogicKind('QF_AUFNIA')

qfAufnira → const LogicKind

const LogicKind('QF_AUFNIRA')

qfAnia → const LogicKind

const LogicKind('QF_ANIA')

qfLira → const LogicKind

const LogicKind('QF_LIRA')

qfUflia → const LogicKind

Unquantified linear integer arithmetic with uninterpreted sort and function symbols.

const LogicKind('QF_UFLIA')

qfUfidl → const LogicKind

Difference Logic over the integers (in essence) but with uninterpreted sort and function symbols.

const LogicKind('QF_UFIDL')

qfUfrdl → const LogicKind

const LogicKind('QF_UFRDL')

qfNia → const LogicKind

Quantifier-free integer arithmetic.

const LogicKind('QF_NIA')

qfNira → const LogicKind

const LogicKind('QF_NIRA')

qfUfnia → const LogicKind

const LogicKind('QF_UFNIA')

qfUfnira → const LogicKind

const LogicKind('QF_UFNIRA')

qfBvre → const LogicKind

const LogicKind('QF_BVRE')

alia → const LogicKind

const LogicKind('ALIA')

auflia → const LogicKind

Closed formulas over the theory of linear integer arithmetic and arrays extended with free sort and function symbols but restricted to arrays with integer indices and values.

const LogicKind('AUFLIA')

auflira → const LogicKind

Closed linear formulas with free sort and function symbols over one- and two-dimentional arrays of integer index and real value.

const LogicKind('AUFLIRA')

aufnia → const LogicKind

const LogicKind('AUFNIA')

aufnira → const LogicKind

Closed formulas with free function and predicate symbols over a theory of arrays of arrays of integer index and real value.

const LogicKind('AUFNIRA')

uflia → const LogicKind

const LogicKind('UFLIA')

ufnra → const LogicKind

const LogicKind('UFNRA')

ufnira → const LogicKind

const LogicKind('UFNIRA')

nia → const LogicKind

const LogicKind('NIA')

ufnia → const LogicKind

Non-linear integer arithmetic with uninterpreted sort and function symbols.

const LogicKind('UFNIA')

lia → const LogicKind

Closed linear formulas over linear integer arithmetic.

const LogicKind('LIA')

ufidl → const LogicKind

const LogicKind('UFIDL')

qfFp → const LogicKind

const LogicKind('QF_FP')

fp → const LogicKind

const LogicKind('FP')

qfFpbv → const LogicKind

const LogicKind('QF_FPBV')

qfBvfp → const LogicKind

const LogicKind('QF_BVFP')

qfS → const LogicKind

const LogicKind('QF_S')

qfSlia → const LogicKind

const LogicKind('QF_SLIA')

qfFd → const LogicKind

const LogicKind('QF_FD')

horn → const LogicKind

const LogicKind('HORN')

qfFplra → const LogicKind

const LogicKind('QF_FPLRA')

ufbv → const LogicKind

const LogicKind('UFBV')

aufbv → const LogicKind

const LogicKind('AUFBV')

abv → const LogicKind

const LogicKind('ABV')

bv → const LogicKind

const LogicKind('BV')

qfBv → const LogicKind

Closed quantifier-free formulas over the theory of fixed-size bitvectors.

const LogicKind('QF_BV')

qfUfbv → const LogicKind

Unquantified formulas over bitvectors with uninterpreted sort function and symbols.

const LogicKind('QF_UFBV')

qfAbv → const LogicKind

Closed quantifier-free formulas over the theory of bitvectors and bitvector arrays.

const LogicKind('QF_ABV')

qfAufbv → const LogicKind

Closed quantifier-free formulas over the theory of bitvectors and bitvector arrays extended with free sort and function symbols.

const LogicKind('QF_AUFBV')

smtfd → const LogicKind

const LogicKind('SMTFD')

qfAx → const LogicKind

Closed quantifier-free formulas over the theory of arrays with extensionality.

const LogicKind('QF_AX')

qfUf → const LogicKind

Unquantified formulas built over a signature of uninterpreted (i.e., free) sort and function symbols.

const LogicKind('QF_UF')

uf → const LogicKind

const LogicKind('UF')

qfUfdt → const LogicKind

const LogicKind('QF_UFDT')

qfDt → const LogicKind

const LogicKind('QF_DT')

Properties

hashCode → int

The hash code for this object.

no setter, inherited

index → int

A numeric identifier for the enumerated value.

no setter, inherited

runtimeType → Type

A representation of the runtime type of the object.

no setter, inherited

smtlibName → String

final

Methods

noSuchMethod(Invocation invocation) → dynamic

Invoked when a nonexistent method or property is accessed.

inherited

toString() → String

A string representation of this object.

inherited

Operators

operator ==(Object other) → bool

The equality operator.

inherited

Constants

values → const List<LogicKind>

A constant List of the values in this enum, in order of their declaration.