Enum rsmt2::Logic [−][src]
pub enum Logic {
Show 13 variants
QF_UF,
QF_LIA,
QF_NIA,
QF_LRA,
QF_AUFLIA,
AUFLIA,
AUFLIRA,
AUFNIRA,
LRA,
QF_BV,
QF_UFBV,
QF_ABV,
QF_AUFBV,
}
Expand description
SMT Lib 2 logics, used with Solver::set_logic
.
Variants
Quantifier-free uninterpreted functions.
Quantifier-free linear integer arithmetic.
Quantifier-free non-linear integer arithmetic.
Quantifier-free linear real arithmetic.
Quantifier-free arrays, uninterpreted functions, linear integer arithmetic.
Arrays, uninterpreted functions, linear integer arithmetic.
Arrays, uninterpreted functions, linear integer/real arithmetic.
arrays, uninterpreted functions, non-linear integer/real arithmetic.
Linear real arithmetic.
Quantifier-free fixed-size bitvectors.
Quantifier-free uninterpreted functions, fixed-size bitvectors.
Quantifier-free arrays, fixed-size bitvectors.
Quantifier-free arrays, uninterpreted functions, fixed-size bitvectors.
Implementations
Trait Implementations
Auto Trait Implementations
impl RefUnwindSafe for Logic
impl UnwindSafe for Logic
Blanket Implementations
Mutably borrows from an owned value. Read more