1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
//! Basic types used by the library.
use std::{fmt, io};
use crate::prelude::*;
/// SMT-LIB 2 logics, used with [`Solver::set_logic`][crate::Solver::set_logic].
#[allow(non_camel_case_types)]
#[derive(Clone, Copy)]
pub enum Logic {
/// Quantifier-free uninterpreted functions.
QF_UF,
/// Quantifier-free linear integer arithmetic.
QF_LIA,
/// Quantifier-free non-linear integer arithmetic.
QF_NIA,
/// Quantifier-free linear real arithmetic.
QF_LRA,
/// Quantifier-free arrays, uninterpreted functions, linear integer arithmetic.
QF_AUFLIA,
/// Arrays, uninterpreted functions, linear integer arithmetic.
AUFLIA,
/// Arrays, uninterpreted functions, linear integer/real arithmetic.
AUFLIRA,
/// arrays, uninterpreted functions, non-linear integer/real arithmetic.
AUFNIRA,
/// Linear real arithmetic.
LRA,
/// Quantifier-free fixed-size bitvectors.
QF_BV,
/// Quantifier-free uninterpreted functions, fixed-size bitvectors.
QF_UFBV,
/// Quantifier-free arrays, fixed-size bitvectors.
QF_ABV,
/// Quantifier-free arrays, uninterpreted functions, fixed-size bitvectors.
QF_AUFBV,
}
impl fmt::Display for Logic {
fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result {
use self::Logic::*;
match *self {
QF_UF => write!(fmt, "QF_UF"),
QF_LIA => write!(fmt, "QF_LIA"),
QF_NIA => write!(fmt, "QF_NIA"),
QF_LRA => write!(fmt, "QF_LRA"),
QF_AUFLIA => write!(fmt, "QF_AUFLIA"),
AUFLIA => write!(fmt, "AUFLIA"),
AUFLIRA => write!(fmt, "AUFLIRA"),
AUFNIRA => write!(fmt, "AUFNIRA"),
LRA => write!(fmt, "LRA"),
QF_BV => write!(fmt, "QF_BV"),
QF_UFBV => write!(fmt, "QF_UFBV"),
QF_ABV => write!(fmt, "QF_ABV"),
QF_AUFBV => write!(fmt, "QF_AUFBV"),
}
}
}
impl Logic {
/// Prints the logic in a writer in SMT-LIB 2 format.
pub fn to_smt2<W: io::Write>(self, writer: &mut W, _: ()) -> SmtRes<()> {
write!(writer, "{}", self)?;
Ok(())
}
}