From cd50afd72bc32da43a914792861d75ec7f3ada9d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Oliver=20B=C3=B8ving?= Date: Thu, 28 Dec 2023 19:40:33 +0100 Subject: [PATCH] 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 | 4 ++-- Cargo.lock | 12 ------------ README.md | 4 ++-- lowlevel/Cargo.toml | 6 +----- lowlevel/src/backend/cvc5.rs | 11 ++++++----- lowlevel/src/backend/mod.rs | 14 +++++--------- lowlevel/src/backend/z3_binary.rs | 11 ++++++----- lowlevel/src/lib.rs | 9 +++------ lowlevel/src/tests.rs | 1 - smtlib/Cargo.toml | 7 ++----- smtlib/src/lib.rs | 2 -- 11 files changed, 27 insertions(+), 54 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index c19b4fe..ed360e8 100644 --- a/.github/workflows/ci.yml +++ b/.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 diff --git a/Cargo.lock b/Cargo.lock index 907a484..9d11109 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -26,17 +26,6 @@ dependencies = [ "memchr", ] -[[package]] -name = "async-trait" -version = "0.1.74" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a66537f1bb974b254c98ed142ff995236e81b9d0fe4db0575f46612cb15eb0f9" -dependencies = [ - "proc-macro2", - "quote", - "syn", -] - [[package]] name = "autocfg" version = "1.1.0" @@ -736,7 +725,6 @@ dependencies = [ name = "smtlib-lowlevel" version = "0.1.8" dependencies = [ - "async-trait", "insta", "itertools", "logos", diff --git a/README.md b/README.md index 86cb52d..aa0f736 100644 --- a/README.md +++ b/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. diff --git a/lowlevel/Cargo.toml b/lowlevel/Cargo.toml index cb90256..7182aaa 100644 --- a/lowlevel/Cargo.toml +++ b/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"] diff --git a/lowlevel/src/backend/cvc5.rs b/lowlevel/src/backend/cvc5.rs index f8a6fd1..5924668 100644 --- a/lowlevel/src/backend/cvc5.rs +++ b/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 { - self.bin.exec(cmd).map(Into::into) + fn exec_async( + &mut self, + cmd: &crate::Command, + ) -> impl Future> { + async { self.bin.exec(cmd).map(Into::into) } } } diff --git a/lowlevel/src/backend/mod.rs b/lowlevel/src/backend/mod.rs index 54e7f8a..628aa84 100644 --- a/lowlevel/src/backend/mod.rs +++ b/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; } -#[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; + fn exec_async( + &mut self, + cmd: &crate::Command, + ) -> impl Future>; } struct BinaryBackend { diff --git a/lowlevel/src/backend/z3_binary.rs b/lowlevel/src/backend/z3_binary.rs index 9f2ce83..472c21f 100644 --- a/lowlevel/src/backend/z3_binary.rs +++ b/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 { - self.bin.exec(cmd).map(Into::into) + fn exec_async( + &mut self, + cmd: &crate::Command, + ) -> impl Future> { + async { self.bin.exec(cmd).map(Into::into) } } } diff --git a/lowlevel/src/lib.rs b/lowlevel/src/lib.rs index f068012..89290bb 100644 --- a/lowlevel/src/lib.rs +++ b/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 { backend: B, } -#[cfg(feature = "async")] impl AsyncDriver where B: AsyncBackend, @@ -84,7 +81,7 @@ where } pub async fn exec(&mut self, cmd: &Command) -> Result { // 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 { diff --git a/lowlevel/src/tests.rs b/lowlevel/src/tests.rs index c2a14c7..01ffc97 100644 --- a/lowlevel/src/tests.rs +++ b/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}; diff --git a/smtlib/Cargo.toml b/smtlib/Cargo.toml index b91dde7..1a5d8d7 100644 --- a/smtlib/Cargo.toml +++ b/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"] diff --git a/smtlib/src/lib.rs b/smtlib/src/lib.rs index 9a25922..37a852a 100644 --- a/smtlib/src/lib.rs +++ b/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::*};