LogicKind enum - z3 library

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: Non-linear real arithmetic.

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 uninterpreted sort and function symbols.

const LogicKind('QF_AUFLIA')
qfAlia → const LogicKind: Quantifier-free array linear integer arithmetic.

const LogicKind('QF_ALIA')
qfAuflira → const LogicKind: Quantifier-free array integer and real arithmetic with free sort and function symbols.

const LogicKind('QF_AUFLIRA')
qfAufnia → const LogicKind: Quantifier-free non-linear integer arithmetic in arrays with free sort and function symbols.

const LogicKind('QF_AUFNIA')
qfAufnira → const LogicKind: Quantifier-free non-linear integer and real arithmetic in arrays with free sort and function symbols.

const LogicKind('QF_AUFNIRA')
qfAnia → const LogicKind: Quantifier-free integer arithmetic in arrays.

const LogicKind('QF_ANIA')
qfLira → const LogicKind: Quantifier-free linear integer and real arithmetic.

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: Quantifier-free rational difference logic with uninterpreted sort and function symbols.

const LogicKind('QF_UFRDL')
qfNia → const LogicKind: Quantifier-free integer arithmetic.

const LogicKind('QF_NIA')
qfNira → const LogicKind: Quantifier-free non-linear integer and real arithmetic.

const LogicKind('QF_NIRA')
qfUfnia → const LogicKind: Quantifier-free non-linear integer arithmetic with uninterpreted sort and function symbols.

const LogicKind('QF_UFNIA')
qfUfnira → const LogicKind: Quantifier-free non-linear integer and real arithmetic with uninterpreted sort and function symbols.

const LogicKind('QF_UFNIRA')
qfBvre → const LogicKind: Quantifier-free bit-vector and RegEx theory.

const LogicKind('QF_BVRE')
alia → const LogicKind: Array linear integer arithmetic.

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-dimensional arrays of integer index and real value.

const LogicKind('AUFLIRA')
aufnia → const LogicKind: Non-linear integer arithmetic over arrays with uninterpreted sort and function symbols.

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: Linear integer arithmetic with uninterpreted sort and function symbols.

const LogicKind('UFLIA')
ufnra → const LogicKind: Non-linear real arithmetic with uninterpreted sort and function symbols.

const LogicKind('UFNRA')
ufnira → const LogicKind: Non-linear integer and real arithmetic with uninterpreted sort and function symbols.

const LogicKind('UFNIRA')
nia → const LogicKind: Non-linear integer arithmetic.

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: Integer difference logic with uninterpreted sort and function symbols.

const LogicKind('UFIDL')
qfFp → const LogicKind: Quantifier free floating point arithmetic.

const LogicKind('QF_FP')
fp → const LogicKind: Floating point arithmetic.

const LogicKind('FP')
qfFpbv → const LogicKind: Quantifier-free floating point and bit-vector arithmetic.

const LogicKind('QF_FPBV')
qfBvfp → const LogicKind: Quantifier-free floating point and bit-vector arithmetic.

const LogicKind('QF_BVFP')
qfS → const LogicKind: Quantifier-free theory of sequences.

const LogicKind('QF_S')
qfSlia → const LogicKind: Quantifier-free theory of sequences with linear integer arithmetic.

const LogicKind('QF_SLIA')
qfFd → const LogicKind: Quantifier-free theory of finite domains.

const LogicKind('QF_FD')
horn → const LogicKind: Solver for HORN clauses.

const LogicKind('HORN')
qfFplra → const LogicKind: Quantifier-free floating point and linear real arithmetic.

const LogicKind('QF_FPLRA')
ufbv → const LogicKind: Bit-vector arithmetic with uninterpreted sort and function symbols.

const LogicKind('UFBV')
aufbv → const LogicKind: Bit-vector arithmetic in arrays with uninterpreted sort and function symbols.

const LogicKind('AUFBV')
abv → const LogicKind: Array theory with bit-vectors.

const LogicKind('ABV')
bv → const LogicKind: Bit-vector arithmetic.

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 uninterpreted sort and function symbols.

const LogicKind('QF_AUFBV')
smtfd → const LogicKind: SMT solver on finite domains.

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: Quantifier-free formulas.

const LogicKind('UF')
qfUfdt → const LogicKind: Quantifier-free data-type and uninterpreted function logic.

const LogicKind('QF_UFDT')
qfDt → const LogicKind: Quantifier-free data-type logic.

const LogicKind('QF_DT')

Properties

hashCode → int: The hash code for this object.
no setterinherited
index → int: A numeric identifier for the enumerated value.
no setterinherited
name → String: Available on Enum, provided by the EnumName extension
The name of the enum value.
no setter
runtimeType → Type: A representation of the runtime type of the object.
no setterinherited
smtlibName → String: The name of the logic in SMT-LIB.
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.