Enum rsmt2::Logic
[−]
[src]
pub enum Logic { QF_UF, QF_LIA, QF_NIA, QF_LRA, QF_AUFLIA, AUFLIA, AUFLIRA, AUFNIRA, LRA, }
SMT Lib 2 logics.
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
Quantifier-free 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.
Methods
impl Logic
[src]
fn to_smt2(&self, writer: &mut Write, _: ()) -> Res<()>
Prints the logic in a writer in SMT Lib 2 format.