smtlib_lowlevel/backend/
z3_binary.rs

1use std::ffi::OsStr;
2
3use super::{Backend, BinaryBackend};
4
5pub struct Z3Binary {
6    bin: BinaryBackend,
7}
8
9impl Z3Binary {
10    pub fn new(z3: impl AsRef<OsStr>) -> Result<Self, std::io::Error> {
11        Ok(Z3Binary {
12            bin: BinaryBackend::new(z3, |cmd| {
13                cmd.arg("smtlib2_compliant=true").arg("-in");
14            })?,
15        })
16    }
17}
18
19impl Backend for Z3Binary {
20    fn exec(&mut self, cmd: crate::Command) -> Result<String, crate::Error> {
21        self.bin.exec(cmd).map(Into::into)
22    }
23}
24
25#[cfg(feature = "tokio")]
26pub mod tokio {
27    use std::{ffi::OsStr, future::Future};
28
29    use crate::backend::tokio::TokioBinaryBackend;
30
31    pub struct Z3BinaryTokio {
32        bin: TokioBinaryBackend,
33    }
34
35    impl Z3BinaryTokio {
36        pub async fn new(z3: impl AsRef<OsStr>) -> Result<Self, std::io::Error> {
37            Ok(Z3BinaryTokio {
38                bin: TokioBinaryBackend::new(z3, |cmd| {
39                    cmd.arg("smtlib2_compliant=true").arg("-in");
40                })
41                .await?,
42            })
43        }
44    }
45
46    impl crate::backend::tokio::TokioBackend for Z3BinaryTokio {
47        fn exec(
48            &mut self,
49            cmd: crate::Command,
50        ) -> impl Future<Output = Result<String, crate::Error>> {
51            async move { self.bin.exec(cmd).await.map(Into::into) }
52        }
53    }
54}
smtlib_lowlevel/backend/z3_binary.rs

smtlib_lowlevel/backend/
z3_binary.rs
