breaking: Remove Async{Driver,Solver} in favor of `Tokio{Driver,Sol…

…ver}`

The previous implementations simply created a future and ran blocking code in that future. This was pretty much all we could do without having an actual variant of `Command` that was async.

So instead of trying to find some executor-agnostic approach, we will be explicit about using tokio.

This explicitness will allow is in the future to add other executors, and not give a false impression about being agnostic.

We might lift this or change the naming in the future.

One thing to note, is that the currenting naming is a bit strange; sort of a mix of suffixing/prefix `Tokio` where it fits. I could not immediately come up with a holistic way of doing this, so we stick with this for now.

README.md

@@ -29,7 +29,7 @@ cargo add smtlib
 Now you can go ahead and use the library in your project.
 
 ```rust
-use smtlib::{backend::Z3Binary, Int, SatResultWithModel, Solver, Sort};
+use smtlib::{backend::z3_binary::Z3Binary, Int, SatResultWithModel, Solver, Sort};
 
 fn main() -> Result<(), Box<dyn std::error::Error>> {
     // Initialize the solver with the Z3 backend. The "z3" string refers the

lowlevel/Cargo.toml

@@ -14,18 +14,20 @@ documentation = "https://docs.rs/smtlib-lowlevel"
 default = []
 z3-static = ["dep:z3-sys"]
 serde = ["dep:serde"]
+tokio = ["dep:tokio"]
 
 [dependencies]
 itertools.workspace = true
 logos = "0.13.0"
 miette.workspace = true
 serde = { workspace = true, optional = true }
 thiserror.workspace = true
+tokio = { version = "1.37.0", features = ["io-util", "process"], optional = true }
 z3-sys = { version = "0.8.1", features = ["static-link-z3"], optional = true }
 
 [dev-dependencies]
 insta.workspace = true
-smtlib-lowlevel = { path = ".", features = ["serde"] }
+smtlib-lowlevel = { path = ".", features = ["serde", "tokio"] }
 
 [package.metadata.docs.rs]
 features = ["serde"]

lowlevel/src/backend/cvc5_binary.rs

@@ -0,0 +1,58 @@
+use std::ffi::OsStr;
+
+use super::{Backend, BinaryBackend};
+
+pub struct Cvc5Binary {
+    bin: BinaryBackend,
+}
+
+impl Cvc5Binary {
+    pub fn new(cvc5: impl AsRef<OsStr>) -> Result<Self, std::io::Error> {
+        Ok(Cvc5Binary {
+            bin: BinaryBackend::new(cvc5, |cmd| {
+                cmd.args(["--lang", "smt2"])
+                    .args(["--produce-models"])
+                    .args(["--incremental"]);
+            })?,
+        })
+    }
+}
+
+impl Backend for Cvc5Binary {
+    fn exec(&mut self, cmd: &crate::Command) -> Result<String, crate::Error> {
+        self.bin.exec(cmd).map(Into::into)
+    }
+}
+
+#[cfg(feature = "tokio")]
+pub mod tokio {
+    use std::{ffi::OsStr, future::Future};
+
+    use crate::backend::tokio::TokioBinaryBackend;
+
+    pub struct Cvc5BinaryTokio {
+        bin: TokioBinaryBackend,
+    }
+
+    impl Cvc5BinaryTokio {
+        pub async fn new(cvc5: impl AsRef<OsStr>) -> Result<Self, std::io::Error> {
+            Ok(Cvc5BinaryTokio {
+                bin: TokioBinaryBackend::new(cvc5, |cmd| {
+                    cmd.args(["--lang", "smt2"])
+                        .args(["--produce-models"])
+                        .args(["--incremental"]);
+                })
+                .await?,
+            })
+        }
+    }
+
+    impl crate::backend::tokio::TokioBackend for Cvc5BinaryTokio {
+        fn exec(
+            &mut self,
+            cmd: &crate::Command,
+        ) -> impl Future<Output = Result<String, crate::Error>> {
+            async { self.bin.exec(cmd).await.map(Into::into) }
+        }
+    }
+}