smtlib_lowlevel/backend/
mod.rs

1//! Backends are concrete solvers which can be communicated with using the
2//! SMT-LIB language.
3//!
4//! This module contains the solver which are supported out-of-the-box by
5//! `smtlib`. Each backend is feature gated, which means that a feature must be
6//! enabled to use the backend.
7//!
8//! ## Backends
9//!
10//! - **[`Z3Binary`](z3_binary::Z3Binary)**: A [Z3](https://github.com/Z3Prover/z3)
11//!   backend using the binary CLI interface.
12//! - **[`Z3BinaryTokio`](z3_binary::tokio::Z3BinaryTokio)**: An async [Z3](https://github.com/Z3Prover/z3)
13//!   backend using the binary CLI interface with [`tokio`](::tokio).
14//!     - **Enabled by feature:** `tokio`
15//! - **`Z3Static`**: A [Z3](https://github.com/Z3Prover/z3) backend using the [`z3-sys`
16//!   crate](https://github.com/prove-rs/z3.rs).
17//!     - **Enabled by feature:** `z3-static`
18//! - **[`Cvc5Binary`](cvc5_binary::Cvc5Binary)**: A [cvc5](https://cvc5.github.io/)
19//!   backend using the binary CLI interface.
20//! - **[`Cvc5BinaryTokio`](cvc5_binary::tokio::Cvc5BinaryTokio)**: An async [cvc5](https://cvc5.github.io/)
21//!   backend using the binary CLI interface with [`tokio`](::tokio).
22//!     - **Enabled by feature:** `tokio`
23
24use std::{
25    io::{BufRead, BufReader, Write},
26    process::{Child, ChildStdin, ChildStdout},
27};
28
29use logos::Lexer;
30
31pub mod cvc5_binary;
32pub mod z3_binary;
33#[cfg(feature = "z3-static")]
34pub mod z3_static;
35
36use crate::parse::Token;
37
38/// The [`Backend`] trait is used to interact with SMT solver using the SMT-LIB
39/// language.
40///
41/// For more details read the [`backend`](crate::backend) module documentation.
42pub trait Backend {
43    fn exec(&mut self, cmd: crate::Command) -> Result<String, crate::Error>;
44}
45
46struct BinaryBackend {
47    #[allow(unused)]
48    child: Child,
49    stdin: ChildStdin,
50    stdout: BufReader<ChildStdout>,
51    buf: String,
52}
53
54impl BinaryBackend {
55    pub(crate) fn new(
56        program: impl AsRef<std::ffi::OsStr>,
57        init: impl FnOnce(&mut std::process::Command),
58    ) -> Result<Self, std::io::Error> {
59        use std::process::{Command, Stdio};
60
61        let mut cmd = Command::new(program);
62        init(&mut cmd);
63        let mut child = cmd.stdin(Stdio::piped()).stdout(Stdio::piped()).spawn()?;
64        let stdin = child.stdin.take().unwrap();
65        let stdout = BufReader::new(child.stdout.take().unwrap());
66
67        Ok(BinaryBackend {
68            child,
69            stdin,
70            stdout,
71            buf: String::new(),
72        })
73    }
74    pub(crate) fn exec(&mut self, cmd: crate::Command) -> Result<&str, crate::Error> {
75        // println!("> {cmd}");
76        writeln!(self.stdin, "{cmd}")?;
77        self.stdin.flush()?;
78
79        self.buf.clear();
80        loop {
81            let n = self.stdout.read_line(&mut self.buf)?;
82            if n == 0 {
83                continue;
84            }
85            if Lexer::new(self.buf.as_str())
86                .map(|tok| tok.unwrap_or(Token::Error))
87                .fold(0i32, |acc, tok| match tok {
88                    Token::LParen => acc + 1,
89                    Token::RParen => acc - 1,
90                    _ => acc,
91                })
92                != 0
93            {
94                continue;
95            }
96            return Ok(&self.buf);
97        }
98    }
99}
100
101#[cfg(feature = "tokio")]
102pub mod tokio {
103    use std::future::Future;
104
105    use logos::Lexer;
106    use tokio::io::{AsyncBufReadExt, AsyncWriteExt, BufReader};
107
108    use crate::parse::Token;
109
110    /// The [`TokioBackend`] trait is used to interact with SMT solver using the
111    /// SMT-LIB language.
112    ///
113    /// For more details read the [`backend`](crate::backend) module
114    /// documentation.
115    pub trait TokioBackend {
116        fn exec(
117            &mut self,
118            cmd: crate::Command,
119        ) -> impl Future<Output = Result<String, crate::Error>>;
120    }
121
122    pub(crate) struct TokioBinaryBackend {
123        #[allow(unused)]
124        child: tokio::process::Child,
125        stdin: tokio::process::ChildStdin,
126        stdout: BufReader<tokio::process::ChildStdout>,
127        buf: String,
128    }
129
130    #[cfg(feature = "tokio")]
131    impl TokioBinaryBackend {
132        pub(crate) async fn new(
133            program: impl AsRef<std::ffi::OsStr>,
134            init: impl FnOnce(&mut tokio::process::Command),
135        ) -> Result<Self, std::io::Error> {
136            use std::process::Stdio;
137
138            use tokio::process::Command;
139
140            let mut cmd = Command::new(program);
141            init(&mut cmd);
142            let mut child = cmd
143                .kill_on_drop(true)
144                .stdin(Stdio::piped())
145                .stdout(Stdio::piped())
146                .spawn()?;
147            let stdin = child.stdin.take().unwrap();
148            let stdout = BufReader::new(child.stdout.take().unwrap());
149
150            Ok(TokioBinaryBackend {
151                child,
152                stdin,
153                stdout,
154                buf: String::new(),
155            })
156        }
157        pub(crate) async fn exec(&mut self, cmd: crate::Command<'_>) -> Result<&str, crate::Error> {
158            // eprintln!("> {cmd}");
159            self.stdin.write_all(cmd.to_string().as_bytes()).await?;
160            self.stdin.write_all(b"\n").await?;
161            self.stdin.flush().await?;
162
163            self.buf.clear();
164            loop {
165                let n = self.stdout.read_line(&mut self.buf).await?;
166                if n == 0 {
167                    continue;
168                }
169                if Lexer::new(self.buf.as_str())
170                    .map(|tok| tok.unwrap_or(Token::Error))
171                    .fold(0i32, |acc, tok| match tok {
172                        Token::LParen => acc + 1,
173                        Token::RParen => acc - 1,
174                        _ => acc,
175                    })
176                    != 0
177                {
178                    continue;
179                }
180                return Ok(&self.buf);
181            }
182        }
183    }
184}
smtlib_lowlevel/backend/mod.rs

smtlib_lowlevel/backend/
mod.rs
