BREAKING CHANGE: Remove async-trait crate and async, z3, cvc5…

… features

With Rust 1.75 released we no have `async fn` and `-> impl Trait` in traits! This removes the need for the `async-trait` crate. It, however, requires us to bump MSRV to 1.75 which I am fine with.

Additionally, I chose to remove feature flags for `async` and the `z3` and `cvc5` brinary backends.

The `async` featrue flag includes almost only `AsyncBackend` and `AsyncSolver` which have no further dependencies, so they might as well be enabled by default. We might bring something back if we add tokio based `BinaryBackend`'s.

The `z3` and `cvc5` added no additional dependencies and very little code, since all they do is call out to a binary, so we might as well include them by default and reduce the complexity.

.github/workflows/ci.yml

@@ -67,7 +67,7 @@ jobs:
         build: [msrv, debug, release]
         include:
           - build: msrv
-            rust: 1.70.0 # MSRV
+            rust: 1.75.0 # MSRV
             target: x86_64-unknown-linux-gnu
             features: full
           - build: debug
@@ -143,7 +143,7 @@ jobs:
       - name: Install Rust
         uses: dtolnay/rust-toolchain@stable
         with:
-          toolchain: 1.70.0 # MSRV
+          toolchain: 1.75.0 # MSRV
           components: clippy
       - uses: Swatinem/rust-cache@v2
       - name: Lint

README.md

@@ -20,10 +20,10 @@ Thus the goal of `smtlib` (and [`smtlib-lowlevel`](https://crates.io/crates/smtl
 
 ## Usage
 
-The primary way to use `smtlib` is by constructing a [`smtlib::Solver`](https://docs.rs/smtlib/latest/smtlib/struct.Solver.html). A solver takes as argument a [`smtlib::Backend`](https://docs.rs/smtlib/latest/smtlib/trait.Backend.html). To see which backends are provided with the library check out the [`smtlib::backend`](https://docs.rs/smtlib/latest/smtlib/backend/index.html) module. Each backend is behind a feature flag, so for example to use the [Z3](https://github.com/Z3Prover/z3) binary backend install `smtlib` by running
+The primary way to use `smtlib` is by constructing a [`smtlib::Solver`](https://docs.rs/smtlib/latest/smtlib/struct.Solver.html). A solver takes as argument a [`smtlib::Backend`](https://docs.rs/smtlib/latest/smtlib/trait.Backend.html). To see which backends are provided with the library check out the [`smtlib::backend`](https://docs.rs/smtlib/latest/smtlib/backend/index.html) module. Some backend is behind a feature flag, so for example to use the [Z3](https://github.com/Z3Prover/z3) statically backend install `smtlib` by running `cargo add smtlib -F z3-static`, but otherwise add it by running:
 
 ```bash
-cargo add smtlib --features z3
+cargo add smtlib
 ```
 
 Now you can go ahead and use the library in your project.

lowlevel/Cargo.toml

@@ -12,14 +12,10 @@ documentation = "https://docs.rs/smtlib-lowlevel"
 
 [features]
 default = []
-z3 = []
 z3-static = ["dep:z3-sys"]
-cvc5 = []
 serde = ["dep:serde"]
-async = ["dep:async-trait"]
 
 [dependencies]
-async-trait = { version = "0.1.74", optional = true }
 itertools.workspace = true
 logos = "0.13.0"
 miette.workspace = true
@@ -35,4 +31,4 @@ smtlib-lowlevel = { path = ".", features = ["serde"] }
 smtlib-build-util = { version = "0.1.8", path = "../build-util" }
 
 [package.metadata.docs.rs]
-features = ["z3", "cvc5", "serde", "async"]
+features = ["serde"]

lowlevel/src/backend/cvc5.rs

@@ -1,4 +1,4 @@
-use std::ffi::OsStr;
+use std::{ffi::OsStr, future::Future};
 
 use super::{Backend, BinaryBackend};
 
@@ -24,10 +24,11 @@ impl Backend for Cvc5Binary {
     }
 }
 
-#[cfg(feature = "async")]
-#[async_trait::async_trait(?Send)]
 impl super::AsyncBackend for Cvc5Binary {
-    async fn exec(&mut self, cmd: &crate::Command) -> Result<String, crate::Error> {
-        self.bin.exec(cmd).map(Into::into)
+    fn exec_async(
+        &mut self,
+        cmd: &crate::Command,
+    ) -> impl Future<Output = Result<String, crate::Error>> {
+        async { self.bin.exec(cmd).map(Into::into) }
     }
 }

lowlevel/src/backend/mod.rs

@@ -8,26 +8,21 @@
 //! ## Backends
 //!
 //! - **[`Z3Binary`]**: A [Z3](https://github.com/Z3Prover/z3) backend using the binary CLI interface.
-//!     - **Enabled by feature:** `z3`
 //! - **[`Z3Static`]**: A [Z3](https://github.com/Z3Prover/z3) backend using the [`z3-sys` crate](https://github.com/prove-rs/z3.rs).
 //!     - **Enabled by feature:** `z3-static`
 //! - **[`Cvc5Binary`]**: A [cvc5](https://cvc5.github.io/) backend using the binary CLI interface.
-//!     - **Enabled by feature:** `cvc5`
 
 use std::{
+    future::Future,
     io::{BufRead, BufReader, Write},
     process::{Child, ChildStdin, ChildStdout},
 };
 
-#[cfg(feature = "cvc5")]
 mod cvc5;
-#[cfg(feature = "cvc5")]
 pub use cvc5::*;
 
-#[cfg(feature = "z3")]
 mod z3_binary;
 use logos::Lexer;
-#[cfg(feature = "z3")]
 pub use z3_binary::*;
 
 #[cfg(feature = "z3-static")]
@@ -44,13 +39,14 @@ pub trait Backend {
     fn exec(&mut self, cmd: &crate::Command) -> Result<String, crate::Error>;
 }
 
-#[cfg(feature = "async")]
 /// The [`AsyncBackend`] trait is used to interact with SMT solver using the SMT-LIB language.
 ///
 /// For more details read the [`backend`](crate::backend) module documentation.
-#[async_trait::async_trait(?Send)]
 pub trait AsyncBackend {
-    async fn exec(&mut self, cmd: &crate::Command) -> Result<String, crate::Error>;
+    fn exec_async(
+        &mut self,
+        cmd: &crate::Command,
+    ) -> impl Future<Output = Result<String, crate::Error>>;
 }
 
 struct BinaryBackend {

lowlevel/src/backend/z3_binary.rs

@@ -1,4 +1,4 @@
-use std::ffi::OsStr;
+use std::{ffi::OsStr, future::Future};
 
 use super::{Backend, BinaryBackend};
 
@@ -22,10 +22,11 @@ impl Backend for Z3Binary {
     }
 }
 
-#[cfg(feature = "async")]
-#[async_trait::async_trait(?Send)]
 impl super::AsyncBackend for Z3Binary {
-    async fn exec(&mut self, cmd: &crate::Command) -> Result<String, crate::Error> {
-        self.bin.exec(cmd).map(Into::into)
+    fn exec_async(
+        &mut self,
+        cmd: &crate::Command,
+    ) -> impl Future<Output = Result<String, crate::Error>> {
+        async { self.bin.exec(cmd).map(Into::into) }
     }
 }

lowlevel/src/lib.rs

@@ -1,4 +1,5 @@
 #![deny(rustdoc::broken_intra_doc_links)]
+#![allow(clippy::manual_async_fn)]
 
 //! # smtlib-lowlevel
 //!
@@ -7,9 +8,7 @@
 use std::collections::HashSet;
 
 use ast::{QualIdentifier, Term};
-#[cfg(feature = "async")]
-use backend::AsyncBackend;
-use backend::Backend;
+use backend::{AsyncBackend, Backend};
 use parse::ParseError;
 
 use crate::ast::{Command, GeneralResponse};
@@ -62,13 +61,11 @@ where
     }
 }
 
-#[cfg(feature = "async")]
 #[derive(Debug)]
 pub struct AsyncDriver<B> {
     backend: B,
 }
 
-#[cfg(feature = "async")]
 impl<B> AsyncDriver<B>
 where
     B: AsyncBackend,
@@ -84,7 +81,7 @@ where
     }
     pub async fn exec(&mut self, cmd: &Command) -> Result<GeneralResponse, Error> {
         // println!("> {cmd}");
-        let res = self.backend.exec(cmd).await?;
+        let res = self.backend.exec_async(cmd).await?;
         let res = if let Some(res) = cmd.parse_response(&res)? {
             GeneralResponse::SpecificSuccessResponse(res)
         } else {

lowlevel/src/tests.rs

@@ -12,7 +12,6 @@ fn bubble_sort() {
     insta::assert_ron_snapshot!(Script::parse(include_str!("../examples/bubble_sort.smt2")));
 }
 
-#[cfg(feature = "z3")]
 mod z3 {
     use crate::{ast::Command, backend::Z3Binary, Driver};
 

smtlib/Cargo.toml

@@ -13,11 +13,8 @@ documentation = "https://docs.rs/smtlib"
 [features]
 default = []
 serde = ["dep:serde", "smtlib-lowlevel/serde"]
-z3 = ["smtlib-lowlevel/z3"]
 z3-static = ["smtlib-lowlevel/z3-static"]
-cvc5 = ["smtlib-lowlevel/cvc5"]
 const-bit-vec = []
-async = ["smtlib-lowlevel/async"]
 
 [dependencies]
 itertools.workspace = true
@@ -30,11 +27,11 @@ thiserror.workspace = true
 futures = "0.3.29"
 insta.workspace = true
 miette = { workspace = true, features = ["fancy"] }
-smtlib = { path = ".", features = ["serde", "z3", "cvc5", "async"] }
+smtlib = { path = ".", features = ["serde"] }
 
 [build-dependencies]
 smtlib-build-util = { version = "0.1.8", path = "../build-util" }
 smtlib-lowlevel = { version = "0.1.8", path = "../lowlevel" }
 
 [package.metadata.docs.rs]
-features = ["serde", "z3", "cvc5", "const-bit-vec", "async"]
+features = ["serde", "const-bit-vec"]

smtlib/src/lib.rs

@@ -14,14 +14,12 @@ pub use backend::Backend;
 pub use logics::Logic;
 pub use smtlib_lowlevel::backend;
 
-#[cfg(feature = "async")]
 mod async_solver;
 mod logics;
 mod solver;
 pub mod terms;
 pub mod theories;
 
-#[cfg(feature = "async")]
 pub use async_solver::AsyncSolver;
 pub use solver::Solver;
 pub use theories::{core::*, fixed_size_bit_vectors::*, ints::*, reals::*};