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
QF_UF
Quantifier-free uninterpreted functions.
QF_LIA
Quantifier-free linear integer arithmetic.
QF_NIA
Quantifier-free non-linear integer arithmetic.
QF_LRA
Quantifier-free linear real arithmetic.
QF_AUFLIA
Quantifier-free arrays, uninterpreted functions, linear integer arithmetic.
AUFLIA
Arrays, uninterpreted functions, linear integer arithmetic.
AUFLIRA
Arrays, uninterpreted functions, linear integer/real arithmetic.
AUFNIRA
arrays, uninterpreted functions, non-linear integer/real arithmetic.
LRA
Linear real arithmetic.
QF_BV
Quantifier-free fixed-size bitvectors.
QF_UFBV
Quantifier-free uninterpreted functions, fixed-size bitvectors.
QF_ABV
Quantifier-free arrays, fixed-size bitvectors.
QF_AUFBV
Quantifier-free arrays, uninterpreted functions, fixed-size bitvectors.
Implementations
Trait Implementations
Auto Trait Implementations
impl RefUnwindSafe for Logic
impl Send for Logic
impl Sync for Logic
impl Unpin for Logic
impl UnwindSafe for Logic
Blanket Implementations
sourceimpl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
const: unstable · sourcefn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more