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::*, 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}
132
133/// A [`Model`] contains the values of all named constants returned through
134/// [`Solver::check_sat_with_model`] or by calling [`Solver::get_model`].
135///
136/// The two most common usages of [`Model`] is to:
137/// - Extract values for constants using [`Model::eval`].
138/// - Print out the produced model using `println!("{model}")`.
139#[cfg_attr(feature = "serde", derive(serde::Serialize))]
140pub struct Model<'st> {
141    values: HashMap<String, STerm<'st>>,
142}
143
144impl std::fmt::Debug for Model<'_> {
145    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
146        self.values.fmt(f)
147    }
148}
149impl std::fmt::Display for Model<'_> {
150    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
151        write!(
152            f,
153            "{{ {} }}",
154            self.values
155                .iter()
156                .sorted_by_key(|(n, _)| n.as_str())
157                .map(|(n, t)| format!("{n}: {}", t.term()))
158                .format(", ")
159        )
160    }
161}
162
163impl<'st> Model<'st> {
164    fn new(st: &'st Storage, model: ast::GetModelResponse<'st>) -> Self {
165        Self {
166            values: model
167                .0
168                .iter()
169                .map(|res| match res {
170                    ast::ModelResponse::DefineFun(f) => (f.0 .0.trim_matches('|').into(), f.3),
171                    ast::ModelResponse::DefineFunRec(_) => todo!(),
172                    ast::ModelResponse::DefineFunsRec(_, _) => todo!(),
173                })
174                .map(|(name, term)| (name, STerm::new_from_ref(st, term)))
175                .collect(),
176        }
177    }
178    /// Extract the value of a constant. Returns `None` if the value was not
179    /// part of the model, which occurs if the constant was not part of any
180    /// expression asserted.
181    ///
182    /// ```
183    /// # use smtlib::{Int, Storage, prelude::*};
184    /// # fn main() -> Result<(), Box<dyn std::error::Error>> {
185    /// # let st = Storage::new();
186    /// # let mut solver = smtlib::Solver::new(&st, smtlib::backend::z3_binary::Z3Binary::new("z3")?)?;
187    /// let x = Int::new_const(&st, "x");
188    /// solver.assert(x._eq(12))?;
189    /// let model = solver.check_sat_with_model()?.expect_sat()?;
190    /// match model.eval(x) {
191    ///     Some(x) => println!("This is the value of x: {x}"),
192    ///     None => panic!("Oh no! This should never happen, as x was part of an assert"),
193    /// }
194    /// # Ok(())
195    /// # }
196    /// ```
197    pub fn eval<T: Sorted<'st>>(&self, x: Const<'st, T>) -> Option<T::Inner>
198    where
199        T::Inner: From<STerm<'st>>,
200    {
201        Some((*self.values.get(x.name().trim_matches('|'))?).into())
202    }
203}
smtlib/lib.rs

smtlib/
lib.rs
