smtlib_lowlevel/
lib.rs

1#![deny(rustdoc::broken_intra_doc_links)]
2#![allow(clippy::manual_async_fn)]
3
4//! # smtlib-lowlevel
5//!
6//! _A low-level API for interacting with SMT solvers._
7
8use std::collections::HashSet;
9
10use ast::{QualIdentifier, Term};
11use backend::Backend;
12use itertools::Itertools;
13use parse::ParseError;
14
15use crate::ast::{Command, GeneralResponse};
16pub use crate::storage::Storage;
17
18#[rustfmt::skip]
19pub mod ast;
20mod ast_ext;
21pub mod backend;
22pub mod lexicon;
23mod parse;
24mod storage;
25#[cfg(test)]
26mod tests;
27
28#[derive(Debug, thiserror::Error, miette::Diagnostic)]
29pub enum Error {
30    #[error(transparent)]
31    #[diagnostic(transparent)]
32    Parse(
33        #[from]
34        #[diagnostic_source]
35        ParseError,
36    ),
37    #[error(transparent)]
38    IO(#[from] std::io::Error),
39}
40
41pub trait Logger: 'static {
42    fn exec(&self, cmd: ast::Command);
43    fn response(&self, cmd: ast::Command, res: &str);
44}
45
46impl<F, G> Logger for (F, G)
47where
48    F: Fn(ast::Command) + 'static,
49    G: Fn(ast::Command, &str) + 'static,
50{
51    fn exec(&self, cmd: ast::Command) {
52        (self.0)(cmd)
53    }
54
55    fn response(&self, cmd: ast::Command, res: &str) {
56        (self.1)(cmd, res)
57    }
58}
59
60pub struct Driver<'st, B> {
61    st: &'st Storage,
62    backend: B,
63    logger: Option<Box<dyn Logger>>,
64}
65
66impl<B: std::fmt::Debug> std::fmt::Debug for Driver<'_, B> {
67    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
68        f.debug_struct("Driver")
69            .field("backend", &self.backend)
70            .field("st", &"...")
71            .field(
72                "logger",
73                if self.logger.is_some() {
74                    &"Some(...)"
75                } else {
76                    &"None"
77                },
78            )
79            .finish()
80    }
81}
82
83impl<'st, B> Driver<'st, B>
84where
85    B: Backend,
86{
87    pub fn new(st: &'st Storage, backend: B) -> Result<Self, Error> {
88        let mut driver = Self {
89            st,
90            backend,
91            logger: None,
92        };
93
94        driver.exec(Command::SetOption(ast::Option::PrintSuccess(true)))?;
95
96        Ok(driver)
97    }
98    pub fn st(&self) -> &'st Storage {
99        self.st
100    }
101    pub fn set_logger(&mut self, logger: impl Logger) {
102        self.logger = Some(Box::new(logger))
103    }
104    pub fn exec(&mut self, cmd: Command<'st>) -> Result<GeneralResponse<'st>, Error> {
105        if let Some(logger) = &self.logger {
106            logger.exec(cmd);
107        }
108        let res = self.backend.exec(cmd)?;
109        if let Some(logger) = &self.logger {
110            logger.response(cmd, &res);
111        }
112        let res = if let Some(res) = cmd.parse_response(self.st, &res)? {
113            GeneralResponse::SpecificSuccessResponse(res)
114        } else {
115            GeneralResponse::parse(self.st, &res)?
116        };
117        Ok(res)
118    }
119}
120
121#[cfg(feature = "tokio")]
122pub mod tokio {
123    use crate::{
124        ast::{self, Command, GeneralResponse},
125        backend::tokio::TokioBackend,
126        storage::Storage,
127        Error, Logger,
128    };
129
130    pub struct TokioDriver<'st, B> {
131        st: &'st Storage,
132        backend: B,
133        logger: Option<Box<dyn Logger>>,
134    }
135
136    impl<B: std::fmt::Debug> std::fmt::Debug for TokioDriver<'_, B> {
137        fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
138            f.debug_struct("TokioDriver")
139                .field("backend", &self.backend)
140                .field("st", &"...")
141                .field(
142                    "logger",
143                    if self.logger.is_some() {
144                        &"Some(...)"
145                    } else {
146                        &"None"
147                    },
148                )
149                .finish()
150        }
151    }
152
153    impl<'st, B> TokioDriver<'st, B>
154    where
155        B: TokioBackend,
156    {
157        pub async fn new(st: &'st Storage, backend: B) -> Result<Self, Error> {
158            let mut driver = Self {
159                st,
160                backend,
161                logger: None,
162            };
163
164            driver
165                .exec(Command::SetOption(ast::Option::PrintSuccess(true)))
166                .await?;
167
168            Ok(driver)
169        }
170        pub fn st(&self) -> &'st Storage {
171            self.st
172        }
173        pub fn set_logger(&mut self, logger: impl Logger) {
174            self.logger = Some(Box::new(logger))
175        }
176        pub async fn exec(&mut self, cmd: Command<'st>) -> Result<GeneralResponse<'st>, Error> {
177            if let Some(logger) = &self.logger {
178                logger.exec(cmd);
179            }
180            let res = self.backend.exec(cmd).await?;
181            if let Some(logger) = &self.logger {
182                logger.response(cmd, &res);
183            }
184            let res = if let Some(res) = cmd.parse_response(self.st, &res)? {
185                GeneralResponse::SpecificSuccessResponse(res)
186            } else {
187                GeneralResponse::parse(self.st, &res)?
188            };
189            Ok(res)
190        }
191    }
192}
193
194// TODO: Use the definitions from 3.6.3 Scoping of variables and parameters
195impl<'st> Term<'st> {
196    pub fn all_consts(&self) -> HashSet<&QualIdentifier> {
197        match self {
198            Term::SpecConstant(_) => HashSet::new(),
199            Term::Identifier(q) => std::iter::once(q).collect(),
200            Term::Application(_, args) => args.iter().flat_map(|arg| arg.all_consts()).collect(),
201            Term::Let(_, _) => todo!(),
202            // TODO
203            Term::Forall(_, _) => HashSet::new(),
204            Term::Exists(_, _) => todo!(),
205            Term::Match(_, _) => todo!(),
206            Term::Annotation(_, _) => todo!(),
207        }
208    }
209    pub fn strip_sort(&'st self, st: &'st Storage) -> &'st Term<'st> {
210        match self {
211            Term::SpecConstant(_) => self,
212            Term::Identifier(
213                QualIdentifier::Identifier(ident) | QualIdentifier::Sorted(ident, _),
214            ) => st.alloc(Term::Identifier(QualIdentifier::Identifier(*ident))),
215            Term::Application(
216                QualIdentifier::Identifier(ident) | QualIdentifier::Sorted(ident, _),
217                args,
218            ) => st.alloc(Term::Application(
219                QualIdentifier::Identifier(*ident),
220                st.alloc_slice(&args.iter().map(|arg| arg.strip_sort(st)).collect_vec()),
221            )),
222            Term::Let(_, _) => todo!(),
223            Term::Forall(qs, rs) => st.alloc(Term::Forall(qs, rs)),
224            Term::Exists(_, _) => todo!(),
225            Term::Match(_, _) => todo!(),
226            Term::Annotation(_, _) => todo!(),
227        }
228    }
229}
smtlib_lowlevel/lib.rs

smtlib_lowlevel/
lib.rs
