smtlib/
lib.rs

1#![cfg_attr(feature = "const-bit-vec", allow(incomplete_features))]
2#![cfg_attr(feature = "const-bit-vec", feature(generic_const_exprs))]
3#![doc = include_str!("../README.md")]
4#![warn(missing_docs)]
5
6use std::collections::HashMap;
7
8pub use backend::Backend;
9use itertools::Itertools;
10pub use logics::Logic;
11use smtlib_lowlevel::ast;
12pub use smtlib_lowlevel::{self as lowlevel, backend, Logger};
13pub use terms::Sorted;
14use terms::{Const, STerm};
15
16#[cfg(feature = "tokio")]
17mod tokio_solver;
18#[rustfmt::skip]
19#[allow(clippy::all)]
20mod logics;
21pub mod funs;
22mod solver;
23pub mod sorts;
24pub mod terms;
25#[cfg(test)]
26mod tests;
27pub mod theories;
28
29pub use smtlib_lowlevel::Storage;
30pub use solver::Solver;
31pub use theories::{core::*, fixed_size_bit_vectors::*, floating_point::*, ints::*, reals::*};
32#[cfg(feature = "tokio")]
33pub use tokio_solver::TokioSolver;
34
35pub mod prelude {
36    //! The prelude module contains the most commonly used types and traits in
37    //! `smtlib`. It is recommended to import this module when using `smtlib`.
38
39    pub use crate::terms::{Sorted, StaticSorted};
40}
41
42/// The satisfiability result produced by a solver
43#[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
44pub enum SatResult {
45    /// The solver produced `unsat`
46    Unsat,
47    /// The solver produced `sat`
48    Sat,
49    /// The solver produced `unknown`
50    Unknown,
51}
52
53impl std::fmt::Display for SatResult {
54    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
55        match self {
56            SatResult::Unsat => write!(f, "unsat"),
57            SatResult::Sat => write!(f, "sat"),
58            SatResult::Unknown => write!(f, "unknown"),
59        }
60    }
61}
62
63/// The satisfiability result produced by a solver, where the
64/// [`Sat`](SatResultWithModel::Sat) variant carries the satisfying model as
65/// well.
66#[derive(Debug)]
67pub enum SatResultWithModel<'st> {
68    /// The solver produced `unsat`
69    Unsat,
70    /// The solver produced `sat` and the associated model
71    Sat(Model<'st>),
72    /// The solver produced `unknown`
73    Unknown,
74}
75
76impl<'st> SatResultWithModel<'st> {
77    /// Expect the result to be `sat` returning the satisfying model. If not
78    /// `sat`, returns an error.
79    pub fn expect_sat(self) -> Result<Model<'st>, Error> {
80        match self {
81            SatResultWithModel::Sat(m) => Ok(m),
82            SatResultWithModel::Unsat => Err(Error::UnexpectedSatResult {
83                expected: SatResult::Sat,
84                actual: SatResult::Unsat,
85            }),
86            SatResultWithModel::Unknown => Err(Error::UnexpectedSatResult {
87                expected: SatResult::Sat,
88                actual: SatResult::Unknown,
89            }),
90        }
91    }
92}
93
94/// An error that occurred during any stage of using `smtlib`.
95#[derive(Debug, thiserror::Error, miette::Diagnostic)]
96#[non_exhaustive]
97pub enum Error {
98    #[error(transparent)]
99    #[diagnostic(transparent)]
100    /// An error originating from the low-level crate. These can for example be
101    /// parsing errors, or solvers occurring with interacting the the solvers.
102    Lowlevel(
103        #[from]
104        #[diagnostic_source]
105        smtlib_lowlevel::Error,
106    ),
107    #[error("SMT error {0} after running {1}")]
108    /// An error produced by the SMT solver. These are of the form
109    ///
110    /// ```ignore
111    /// (error "the error goes here")
112    /// ```
113    Smt(String, String),
114    #[error("Expected the model to be {expected} but was {actual}")]
115    /// Can occur by calling [`SatResultWithModel::expect_sat`] for example.
116    UnexpectedSatResult {
117        /// The expected sat result
118        expected: SatResult,
119        /// The actual sat result
120        actual: SatResult,
121    },
122    /// An error that occurred when trying to cast a dynamic term to a different
123    /// sort.
124    #[error("tried to cast a dynamic of sort {expected} to {actual}")]
125    DynamicCastSortMismatch {
126        /// The expected sort
127        expected: String,
128        /// The actual sort
129        actual: String,
130    },
131    /// Operation is not supported by the underlying solver
132    #[error("Operation is not supported by the underlying solver")]
133    Unsupported,
134}
135
136/// A [`Model`] contains the values of all named constants returned through
137/// [`Solver::check_sat_with_model`] or by calling [`Solver::get_model`].
138///
139/// The two most common usages of [`Model`] is to:
140/// - Extract values for constants using [`Model::eval`].
141/// - Print out the produced model using `println!("{model}")`.
142#[cfg_attr(feature = "serde", derive(serde::Serialize))]
143pub struct Model<'st> {
144    values: HashMap<String, STerm<'st>>,
145}
146
147impl std::fmt::Debug for Model<'_> {
148    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
149        self.values.fmt(f)
150    }
151}
152impl std::fmt::Display for Model<'_> {
153    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
154        write!(
155            f,
156            "{{ {} }}",
157            self.values
158                .iter()
159                .sorted_by_key(|(n, _)| n.as_str())
160                .map(|(n, t)| format!("{n}: {}", t.term()))
161                .format(", ")
162        )
163    }
164}
165
166impl<'st> Model<'st> {
167    fn new(st: &'st Storage, model: ast::GetModelResponse<'st>) -> Self {
168        Self {
169            values: model
170                .0
171                .iter()
172                .map(|res| match res {
173                    ast::ModelResponse::DefineFun(f) => (f.0 .0.trim_matches('|').into(), f.3),
174                    ast::ModelResponse::DefineFunRec(_) => todo!(),
175                    ast::ModelResponse::DefineFunsRec(_, _) => todo!(),
176                })
177                .map(|(name, term)| (name, STerm::new_from_ref(st, term)))
178                .collect(),
179        }
180    }
181    /// Extract the value of a constant. Returns `None` if the value was not
182    /// part of the model, which occurs if the constant was not part of any
183    /// expression asserted.
184    ///
185    /// ```
186    /// # use smtlib::{Int, Storage, prelude::*};
187    /// # fn main() -> Result<(), Box<dyn std::error::Error>> {
188    /// # let st = Storage::new();
189    /// # let mut solver = smtlib::Solver::new(&st, smtlib::backend::z3_binary::Z3Binary::new("z3")?)?;
190    /// let x = Int::new_const(&st, "x");
191    /// solver.assert(x._eq(12))?;
192    /// let model = solver.check_sat_with_model()?.expect_sat()?;
193    /// match model.eval(x) {
194    ///     Some(x) => println!("This is the value of x: {x}"),
195    ///     None => panic!("Oh no! This should never happen, as x was part of an assert"),
196    /// }
197    /// # Ok(())
198    /// # }
199    /// ```
200    pub fn eval<T: Sorted<'st>>(&self, x: Const<'st, T>) -> Option<T::Inner>
201    where
202        T::Inner: From<STerm<'st>>,
203    {
204        Some((*self.values.get(x.name().trim_matches('|'))?).into())
205    }
206}
smtlib/lib.rs

smtlib/
lib.rs
