rsmt2_zz/
common.rs

1//! Basic types used by the library.
2
3use std::{fmt, io};
4
5pub use crate::errors::*;
6
7/// Type of a model.
8pub type Model<Ident, Type, Value> = Vec<(Ident, Vec<(Ident, Type)>, Type, Value)>;
9
10/// A symbol printable in the SMT Lib 2 standard given some info.
11pub trait Sym2Smt<Info> {
12    /// Prints a symbol to a writer given some info.
13    fn sym_to_smt2<Writer>(&self, w: &mut Writer, i: Info) -> SmtRes<()>
14    where
15        Writer: io::Write;
16}
17
18/// An expression printable in the SMT Lib 2 standard given some info.
19pub trait Expr2Smt<Info> {
20    /// Prints an expression to a writer given some info.
21    fn expr_to_smt2<Writer>(&self, w: &mut Writer, i: Info) -> SmtRes<()>
22    where
23        Writer: io::Write;
24}
25
26/// A sort printable in the SMT Lib 2 standard.
27pub trait Sort2Smt {
28    /// Prints a sort to a writer info.
29    fn sort_to_smt2<Writer>(&self, w: &mut Writer) -> SmtRes<()>
30    where
31        Writer: io::Write;
32}
33
34/// Writes a string.
35#[inline(always)]
36pub fn write_str<W: io::Write>(w: &mut W, s: &str) -> SmtRes<()> {
37    w.write_all(s.as_bytes())?;
38    Ok(())
39}
40
41impl<'a, T, Info> Sym2Smt<Info> for &'a T
42where
43    T: Sym2Smt<Info> + ?Sized,
44{
45    fn sym_to_smt2<Writer>(&self, writer: &mut Writer, info: Info) -> SmtRes<()>
46    where
47        Writer: io::Write,
48    {
49        (*self).sym_to_smt2(writer, info)
50    }
51}
52
53impl<'a, T, Info> Expr2Smt<Info> for &'a T
54where
55    T: Expr2Smt<Info> + ?Sized,
56{
57    fn expr_to_smt2<Writer>(&self, writer: &mut Writer, info: Info) -> SmtRes<()>
58    where
59        Writer: io::Write,
60    {
61        (*self).expr_to_smt2(writer, info)
62    }
63}
64
65impl<'a, T> Sort2Smt for &'a T
66where
67    T: Sort2Smt + ?Sized,
68{
69    fn sort_to_smt2<Writer>(&self, writer: &mut Writer) -> SmtRes<()>
70    where
71        Writer: io::Write,
72    {
73        (*self).sort_to_smt2(writer)
74    }
75}
76
77impl<T> Sym2Smt<T> for str {
78    fn sym_to_smt2<Writer>(&self, writer: &mut Writer, _: T) -> SmtRes<()>
79    where
80        Writer: io::Write,
81    {
82        write_str(writer, self)
83    }
84}
85impl<T> Expr2Smt<T> for str {
86    fn expr_to_smt2<Writer>(&self, writer: &mut Writer, _: T) -> SmtRes<()>
87    where
88        Writer: io::Write,
89    {
90        write_str(writer, self)
91    }
92}
93impl Sort2Smt for str {
94    fn sort_to_smt2<Writer>(&self, writer: &mut Writer) -> SmtRes<()>
95    where
96        Writer: io::Write,
97    {
98        write_str(writer, self)
99    }
100}
101
102impl<T> Sym2Smt<T> for String {
103    fn sym_to_smt2<Writer>(&self, writer: &mut Writer, _: T) -> SmtRes<()>
104    where
105        Writer: io::Write,
106    {
107        write_str(writer, self)
108    }
109}
110impl<T> Expr2Smt<T> for String {
111    fn expr_to_smt2<Writer>(&self, writer: &mut Writer, _: T) -> SmtRes<()>
112    where
113        Writer: io::Write,
114    {
115        write_str(writer, self)
116    }
117}
118impl Sort2Smt for String {
119    fn sort_to_smt2<Writer>(&self, writer: &mut Writer) -> SmtRes<()>
120    where
121        Writer: io::Write,
122    {
123        write_str(writer, self)
124    }
125}
126
127/// SMT Lib 2 logics.
128///
129/// See [`Solver::set_logic`][logic].
130///
131/// [logic]: struct.Solver.html#method.set_logic
132#[allow(non_camel_case_types)]
133#[derive(Clone, Copy)]
134pub enum Logic {
135    QF_UFBV,
136    /// Quantifier-free uninterpreted functions.
137    QF_UF,
138    /// Quantifier-free linear integer arithmetic.
139    QF_LIA,
140    /// Quantifier-free non-linear integer arithmetic.
141    QF_NIA,
142    /// Quantifier-free linear real arithmetic.
143    QF_LRA,
144    /** Quantifier-free arrays, uninterpreted functions, linear integer
145    arithmetic. */
146    QF_AUFLIA,
147    /** Quantifier-free arrays, uninterpreted functions, linear integer
148    arithmetic. */
149    AUFLIA,
150    /// Arrays, uninterpreted functions, linear integer/real arithmetic.
151    AUFLIRA,
152    /// arrays, uninterpreted functions, non-linear integer/real arithmetic.
153    AUFNIRA,
154    /// Linear real arithmetic.
155    LRA,
156}
157impl fmt::Display for Logic {
158    fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result {
159        use self::Logic::*;
160        match *self {
161            QF_UFBV => write!(fmt, "QF_UFBV"),
162            QF_UF => write!(fmt, "QF_UF"),
163            QF_LIA => write!(fmt, "QF_LIA"),
164            QF_NIA => write!(fmt, "QF_NIA"),
165            QF_LRA => write!(fmt, "QF_LRA"),
166            QF_AUFLIA => write!(fmt, "QF_AUFLIA"),
167            AUFLIA => write!(fmt, "AUFLIA"),
168            AUFLIRA => write!(fmt, "AUFLIRA"),
169            AUFNIRA => write!(fmt, "AUFNIRA"),
170            LRA => write!(fmt, "LRA"),
171        }
172    }
173}
174impl Logic {
175    /// Prints the logic in a writer in SMT Lib 2 format.
176    pub fn to_smt2<W: io::Write>(self, writer: &mut W, _: ()) -> SmtRes<()> {
177        write!(writer, "{}", self)?;
178        Ok(())
179    }
180}
rsmt2_zz/common.rs

rsmt2_zz/
common.rs
