smtlib_lowlevel/backend/
cvc5_binary.rs

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

smtlib_lowlevel/backend/
cvc5_binary.rs
