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
60/// A simple debug logger that logs SMT commands and responses to stderr.
61pub struct StderrLogger;
62impl Logger for StderrLogger {
63    fn exec(&self, cmd: ast::Command) {
64        eprintln!("> {cmd}");
65    }
66    fn response(&self, _cmd: ast::Command, res: &str) {
67        eprintln!("< {res}");
68    }
69}
70
71pub struct Driver<'st, B> {
72    st: &'st Storage,
73    backend: B,
74    logger: Option<Box<dyn Logger>>,
75}
76
77impl<B: std::fmt::Debug> std::fmt::Debug for Driver<'_, B> {
78    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
79        f.debug_struct("Driver")
80            .field("backend", &self.backend)
81            .field("st", &"...")
82            .field(
83                "logger",
84                if self.logger.is_some() {
85                    &"Some(...)"
86                } else {
87                    &"None"
88                },
89            )
90            .finish()
91    }
92}
93
94impl<'st, B> Driver<'st, B>
95where
96    B: Backend,
97{
98    pub fn new(st: &'st Storage, backend: B) -> Result<Self, Error> {
99        let mut driver = Self {
100            st,
101            backend,
102            logger: None,
103        };
104
105        driver.exec(Command::SetOption(ast::Option::PrintSuccess(true)))?;
106
107        Ok(driver)
108    }
109    pub fn st(&self) -> &'st Storage {
110        self.st
111    }
112    pub fn set_logger(&mut self, logger: impl Logger) {
113        self.logger = Some(Box::new(logger))
114    }
115    pub fn exec(&mut self, cmd: Command<'st>) -> Result<GeneralResponse<'st>, Error> {
116        if let Some(logger) = &self.logger {
117            logger.exec(cmd);
118        }
119        let res = self.backend.exec(cmd)?;
120        if let Some(logger) = &self.logger {
121            logger.response(cmd, &res);
122        }
123        let res = if let Some(res) = cmd.parse_response(self.st, &res)? {
124            GeneralResponse::SpecificSuccessResponse(res)
125        } else {
126            GeneralResponse::parse(self.st, &res)?
127        };
128        Ok(res)
129    }
130}
131
132#[cfg(feature = "tokio")]
133pub mod tokio {
134    use crate::{
135        ast::{self, Command, GeneralResponse},
136        backend::tokio::TokioBackend,
137        storage::Storage,
138        Error, Logger,
139    };
140
141    pub struct TokioDriver<'st, B> {
142        st: &'st Storage,
143        backend: B,
144        logger: Option<Box<dyn Logger>>,
145    }
146
147    impl<B: std::fmt::Debug> std::fmt::Debug for TokioDriver<'_, B> {
148        fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
149            f.debug_struct("TokioDriver")
150                .field("backend", &self.backend)
151                .field("st", &"...")
152                .field(
153                    "logger",
154                    if self.logger.is_some() {
155                        &"Some(...)"
156                    } else {
157                        &"None"
158                    },
159                )
160                .finish()
161        }
162    }
163
164    impl<'st, B> TokioDriver<'st, B>
165    where
166        B: TokioBackend,
167    {
168        pub async fn new(st: &'st Storage, backend: B) -> Result<Self, Error> {
169            let mut driver = Self {
170                st,
171                backend,
172                logger: None,
173            };
174
175            driver
176                .exec(Command::SetOption(ast::Option::PrintSuccess(true)))
177                .await?;
178
179            Ok(driver)
180        }
181        pub fn st(&self) -> &'st Storage {
182            self.st
183        }
184        pub fn set_logger(&mut self, logger: impl Logger) {
185            self.logger = Some(Box::new(logger))
186        }
187        pub async fn exec(&mut self, cmd: Command<'st>) -> Result<GeneralResponse<'st>, Error> {
188            if let Some(logger) = &self.logger {
189                logger.exec(cmd);
190            }
191            let res = self.backend.exec(cmd).await?;
192            if let Some(logger) = &self.logger {
193                logger.response(cmd, &res);
194            }
195            let res = if let Some(res) = cmd.parse_response(self.st, &res)? {
196                GeneralResponse::SpecificSuccessResponse(res)
197            } else {
198                GeneralResponse::parse(self.st, &res)?
199            };
200            Ok(res)
201        }
202    }
203}
204
205// TODO: Use the definitions from 3.6.3 Scoping of variables and parameters
206impl<'st> Term<'st> {
207    pub fn all_consts(&self) -> HashSet<&QualIdentifier<'st>> {
208        match self {
209            Term::SpecConstant(_) => HashSet::new(),
210            Term::Identifier(q) => std::iter::once(q).collect(),
211            Term::Application(_, args) => args.iter().flat_map(|arg| arg.all_consts()).collect(),
212            Term::Let(_, _) => todo!(),
213            // TODO
214            Term::Forall(_, _) => HashSet::new(),
215            Term::Exists(_, _) => todo!(),
216            Term::Match(_, _) => todo!(),
217            Term::Annotation(_, _) => todo!(),
218        }
219    }
220    pub fn strip_sort(&'st self, st: &'st Storage) -> &'st Term<'st> {
221        match self {
222            Term::SpecConstant(_) => self,
223            Term::Identifier(
224                QualIdentifier::Identifier(ident) | QualIdentifier::Sorted(ident, _),
225            ) => st.alloc(Term::Identifier(QualIdentifier::Identifier(*ident))),
226            Term::Application(
227                QualIdentifier::Identifier(ident) | QualIdentifier::Sorted(ident, _),
228                args,
229            ) => st.alloc(Term::Application(
230                QualIdentifier::Identifier(*ident),
231                st.alloc_slice(&args.iter().map(|arg| arg.strip_sort(st)).collect_vec()),
232            )),
233            Term::Let(_, _) => todo!(),
234            Term::Forall(qs, rs) => st.alloc(Term::Forall(qs, rs)),
235            Term::Exists(_, _) => todo!(),
236            Term::Match(_, _) => todo!(),
237            Term::Annotation(_, _) => todo!(),
238        }
239    }
240}
smtlib_lowlevel/lib.rs

smtlib_lowlevel/
lib.rs
