diff --git a/Cargo.lock b/Cargo.lock index 80e49d5..538ae00 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -26,6 +26,28 @@ dependencies = [ "memchr", ] +[[package]] +name = "async-stream" +version = "0.3.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cd56dd203fef61ac097dd65721a419ddccb106b2d2b70ba60a6b529f03961a51" +dependencies = [ + "async-stream-impl", + "futures-core", + "pin-project-lite", +] + +[[package]] +name = "async-stream-impl" +version = "0.3.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "16e62a023e7c117e27523144c5d2459f4397fcc3cab0085af8e2224f643a0193" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + [[package]] name = "autocfg" version = "1.1.0" @@ -100,6 +122,12 @@ version = "2.4.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "327762f6e5a765692301e5bb513e0d9fef63be86bbc14528052b1cd3e6f03e07" +[[package]] +name = "bytes" +version = "1.6.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "514de17de45fdb8dc022b1a7975556c53c86f9f0aa5f534b98977b171857c2c9" + [[package]] name = "cc" version = "1.0.83" @@ -529,6 +557,17 @@ dependencies = [ "adler", ] +[[package]] +name = "mio" +version = "0.8.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a4a650543ca06a924e8b371db273b2756685faae30f8487da1b56505a8f78b0c" +dependencies = [ + "libc", + "wasi", + "windows-sys 0.48.0", +] + [[package]] name = "nom" version = "7.1.3" @@ -721,6 +760,15 @@ version = "1.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "a7cee0529a6d40f580e7a5e6c495c8fbfe21b7b52795ed4bb5e62cdf92bc6380" +[[package]] +name = "signal-hook-registry" +version = "1.4.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a9e9e0b4211b72e7b8b6e85c807d36c212bdb33ea8587f7569562a84df5465b1" +dependencies = [ + "libc", +] + [[package]] name = "similar" version = "2.3.0" @@ -754,6 +802,7 @@ dependencies = [ "smtlib", "smtlib-lowlevel", "thiserror", + "tokio-test", ] [[package]] @@ -767,6 +816,7 @@ dependencies = [ "serde", "smtlib-lowlevel", "thiserror", + "tokio", "z3-sys", ] @@ -860,6 +910,45 @@ dependencies = [ "once_cell", ] +[[package]] +name = "tokio" +version = "1.37.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1adbebffeca75fcfd058afa480fb6c0b81e165a0323f9c9d39c9697e37c46787" +dependencies = [ + "backtrace", + "bytes", + "libc", + "mio", + "pin-project-lite", + "signal-hook-registry", + "windows-sys 0.48.0", +] + +[[package]] +name = "tokio-stream" +version = "0.1.15" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "267ac89e0bec6e691e5813911606935d77c476ff49024f98abcea3e7b15e37af" +dependencies = [ + "futures-core", + "pin-project-lite", + "tokio", +] + +[[package]] +name = "tokio-test" +version = "0.4.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2468baabc3311435b55dd935f702f42cd1b8abb7e754fb7dfb16bd36aa88f9f7" +dependencies = [ + "async-stream", + "bytes", + "futures-core", + "tokio", + "tokio-stream", +] + [[package]] name = "toml" version = "0.8.8" @@ -959,6 +1048,12 @@ version = "0.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "830b7e5d4d90034032940e4ace0d9a9a057e7a45cd94e6c007832e39edb82f6d" +[[package]] +name = "wasi" +version = "0.11.0+wasi-snapshot-preview1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423" + [[package]] name = "winapi" version = "0.3.9" diff --git a/README.md b/README.md index aa0f736..e8b2202 100644 --- a/README.md +++ b/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> { // Initialize the solver with the Z3 backend. The "z3" string refers the diff --git a/lowlevel/Cargo.toml b/lowlevel/Cargo.toml index 101f9b5..cec8d61 100644 --- a/lowlevel/Cargo.toml +++ b/lowlevel/Cargo.toml @@ -14,6 +14,7 @@ documentation = "https://docs.rs/smtlib-lowlevel" default = [] z3-static = ["dep:z3-sys"] serde = ["dep:serde"] +tokio = ["dep:tokio"] [dependencies] itertools.workspace = true @@ -21,11 +22,12 @@ 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"] diff --git a/lowlevel/src/backend/cvc5.rs b/lowlevel/src/backend/cvc5.rs deleted file mode 100644 index 5924668..0000000 --- a/lowlevel/src/backend/cvc5.rs +++ /dev/null @@ -1,34 +0,0 @@ -use std::{ffi::OsStr, future::Future}; - -use super::{Backend, BinaryBackend}; - -pub struct Cvc5Binary { - bin: BinaryBackend, -} - -impl Cvc5Binary { - pub fn new(cvc5: impl AsRef) -> Result { - 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 { - self.bin.exec(cmd).map(Into::into) - } -} - -impl super::AsyncBackend for Cvc5Binary { - fn exec_async( - &mut self, - cmd: &crate::Command, - ) -> impl Future> { - async { self.bin.exec(cmd).map(Into::into) } - } -} diff --git a/lowlevel/src/backend/cvc5_binary.rs b/lowlevel/src/backend/cvc5_binary.rs new file mode 100644 index 0000000..f2b9507 --- /dev/null +++ b/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) -> Result { + 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 { + 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) -> Result { + 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> { + async { self.bin.exec(cmd).await.map(Into::into) } + } + } +} diff --git a/lowlevel/src/backend/mod.rs b/lowlevel/src/backend/mod.rs index 628aa84..3a0929b 100644 --- a/lowlevel/src/backend/mod.rs +++ b/lowlevel/src/backend/mod.rs @@ -13,22 +13,16 @@ //! - **[`Cvc5Binary`]**: A [cvc5](https://cvc5.github.io/) backend using the binary CLI interface. use std::{ - future::Future, io::{BufRead, BufReader, Write}, process::{Child, ChildStdin, ChildStdout}, }; -mod cvc5; -pub use cvc5::*; - -mod z3_binary; use logos::Lexer; -pub use z3_binary::*; +pub mod cvc5_binary; +pub mod z3_binary; #[cfg(feature = "z3-static")] -mod z3_static; -#[cfg(feature = "z3-static")] -pub use z3_static::*; +pub mod z3_static; use crate::parse::Token; @@ -39,16 +33,6 @@ pub trait Backend { fn exec(&mut self, cmd: &crate::Command) -> Result; } -/// 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. -pub trait AsyncBackend { - fn exec_async( - &mut self, - cmd: &crate::Command, - ) -> impl Future>; -} - struct BinaryBackend { #[allow(unused)] child: Child, @@ -103,3 +87,85 @@ impl BinaryBackend { } } } + +#[cfg(feature = "tokio")] +pub mod tokio { + use std::future::Future; + + use logos::Lexer; + use tokio::io::{AsyncBufReadExt, AsyncWriteExt, BufReader}; + + use crate::parse::Token; + + /// The [`TokioBackend`] trait is used to interact with SMT solver using the SMT-LIB language. + /// + /// For more details read the [`backend`](crate::backend) module documentation. + pub trait TokioBackend { + fn exec( + &mut self, + cmd: &crate::Command, + ) -> impl Future>; + } + + pub(crate) struct TokioBinaryBackend { + #[allow(unused)] + child: tokio::process::Child, + stdin: tokio::process::ChildStdin, + stdout: BufReader, + buf: String, + } + + #[cfg(feature = "tokio")] + impl TokioBinaryBackend { + pub(crate) async fn new( + program: impl AsRef, + init: impl FnOnce(&mut tokio::process::Command), + ) -> Result { + use std::process::Stdio; + use tokio::process::Command; + + let mut cmd = Command::new(program); + init(&mut cmd); + let mut child = cmd + .kill_on_drop(true) + .stdin(Stdio::piped()) + .stdout(Stdio::piped()) + .spawn()?; + let stdin = child.stdin.take().unwrap(); + let stdout = BufReader::new(child.stdout.take().unwrap()); + + Ok(TokioBinaryBackend { + child, + stdin, + stdout, + buf: String::new(), + }) + } + pub(crate) async fn exec(&mut self, cmd: &crate::Command) -> Result<&str, crate::Error> { + // eprintln!("> {cmd}"); + self.stdin.write_all(cmd.to_string().as_bytes()).await?; + self.stdin.write_all(b"\n").await?; + self.stdin.flush().await?; + + self.buf.clear(); + loop { + let n = self.stdout.read_line(&mut self.buf).await?; + if n == 0 { + continue; + } + if Lexer::new(self.buf.as_str()) + .map(|tok| tok.unwrap_or(Token::Error)) + .fold(0i32, |acc, tok| match tok { + Token::LParen => acc + 1, + Token::RParen => acc - 1, + _ => acc, + }) + != 0 + { + continue; + } + return Ok(&self.buf); + } + } + } +} diff --git a/lowlevel/src/backend/z3_binary.rs b/lowlevel/src/backend/z3_binary.rs index 472c21f..cab8493 100644 --- a/lowlevel/src/backend/z3_binary.rs +++ b/lowlevel/src/backend/z3_binary.rs @@ -1,4 +1,4 @@ -use std::{ffi::OsStr, future::Future}; +use std::ffi::OsStr; use super::{Backend, BinaryBackend}; @@ -22,11 +22,33 @@ impl Backend for Z3Binary { } } -impl super::AsyncBackend for Z3Binary { - fn exec_async( - &mut self, - cmd: &crate::Command, - ) -> impl Future> { - async { 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 Z3BinaryTokio { + bin: TokioBinaryBackend, + } + + impl Z3BinaryTokio { + pub async fn new(z3: impl AsRef) -> Result { + Ok(Z3BinaryTokio { + bin: TokioBinaryBackend::new(z3, |cmd| { + cmd.arg("smtlib2_compliant=true").arg("-in"); + }) + .await?, + }) + } + } + + impl crate::backend::tokio::TokioBackend for Z3BinaryTokio { + fn exec( + &mut self, + cmd: &crate::Command, + ) -> impl Future> { + async move { self.bin.exec(cmd).await.map(Into::into) } + } } } diff --git a/lowlevel/src/lib.rs b/lowlevel/src/lib.rs index 46faff4..6bc966e 100644 --- a/lowlevel/src/lib.rs +++ b/lowlevel/src/lib.rs @@ -8,7 +8,7 @@ use std::collections::HashSet; use ast::{QualIdentifier, Term}; -use backend::{AsyncBackend, Backend}; +use backend::Backend; use parse::ParseError; use crate::ast::{Command, GeneralResponse}; @@ -62,33 +62,42 @@ where } } -#[derive(Debug)] -pub struct AsyncDriver { - backend: B, -} +#[cfg(feature = "tokio")] +pub mod tokio { + use crate::{ + ast::{self, Command, GeneralResponse}, + backend::tokio::TokioBackend, + Error, + }; -impl AsyncDriver -where - B: AsyncBackend, -{ - pub async fn new(backend: B) -> Result { - let mut driver = Self { backend }; + #[derive(Debug)] + pub struct TokioDriver { + backend: B, + } - driver - .exec(&Command::SetOption(ast::Option::PrintSuccess(true))) - .await?; + impl TokioDriver + where + B: TokioBackend, + { + pub async fn new(backend: B) -> Result { + let mut driver = Self { backend }; - Ok(driver) - } - pub async fn exec(&mut self, cmd: &Command) -> Result { - // println!("> {cmd}"); - let res = self.backend.exec_async(cmd).await?; - let res = if let Some(res) = cmd.parse_response(&res)? { - GeneralResponse::SpecificSuccessResponse(res) - } else { - GeneralResponse::parse(&res)? - }; - Ok(res) + driver + .exec(&Command::SetOption(ast::Option::PrintSuccess(true))) + .await?; + + Ok(driver) + } + pub async fn exec(&mut self, cmd: &Command) -> Result { + // println!("> {cmd}"); + let res = self.backend.exec(cmd).await?; + let res = if let Some(res) = cmd.parse_response(&res)? { + GeneralResponse::SpecificSuccessResponse(res) + } else { + GeneralResponse::parse(&res)? + }; + Ok(res) + } } } diff --git a/lowlevel/src/tests.rs b/lowlevel/src/tests.rs index 01ffc97..dc347a5 100644 --- a/lowlevel/src/tests.rs +++ b/lowlevel/src/tests.rs @@ -13,7 +13,7 @@ fn bubble_sort() { } mod z3 { - use crate::{ast::Command, backend::Z3Binary, Driver}; + use crate::{ast::Command, backend::z3_binary::Z3Binary, Driver}; macro_rules! cmd { ($d:expr, $cmd:literal) => { diff --git a/smtlib/Cargo.toml b/smtlib/Cargo.toml index 64b66fb..be51531 100644 --- a/smtlib/Cargo.toml +++ b/smtlib/Cargo.toml @@ -15,6 +15,7 @@ default = [] serde = ["dep:serde", "smtlib-lowlevel/serde"] z3-static = ["smtlib-lowlevel/z3-static"] const-bit-vec = [] +tokio = ["smtlib-lowlevel/tokio"] [dependencies] itertools.workspace = true @@ -27,7 +28,8 @@ thiserror.workspace = true futures = "0.3.29" insta.workspace = true miette = { workspace = true, features = ["fancy"] } -smtlib = { path = ".", features = ["serde"] } +smtlib = { path = ".", features = ["serde", "tokio"] } +tokio-test = "0.4.4" [package.metadata.docs.rs] features = ["serde", "const-bit-vec"] diff --git a/smtlib/examples/queens.rs b/smtlib/examples/queens.rs index ff361ca..610ff0e 100644 --- a/smtlib/examples/queens.rs +++ b/smtlib/examples/queens.rs @@ -4,7 +4,7 @@ use miette::IntoDiagnostic; use smtlib::backend::Z3Static; use smtlib::{ and, - backend::{Backend, Cvc5Binary, Z3Binary}, + backend::{cvc5_binary::Cvc5Binary, z3_binary::Z3Binary, Backend}, distinct, or, terms::Sort, Int, Logic, SatResultWithModel, Solver, diff --git a/smtlib/examples/queens_bv.rs b/smtlib/examples/queens_bv.rs index 09fad4b..ea6f1cc 100644 --- a/smtlib/examples/queens_bv.rs +++ b/smtlib/examples/queens_bv.rs @@ -4,7 +4,7 @@ use itertools::Itertools; use miette::IntoDiagnostic; use smtlib::{ and, - backend::{Backend, Cvc5Binary, Z3Binary}, + backend::{cvc5_binary::Cvc5Binary, z3_binary::Z3Binary, Backend}, distinct, or, terms::Sort, BitVec, SatResultWithModel, Solver, diff --git a/smtlib/examples/queens_bv2.rs b/smtlib/examples/queens_bv2.rs index 64da4db..dd16bb6 100644 --- a/smtlib/examples/queens_bv2.rs +++ b/smtlib/examples/queens_bv2.rs @@ -4,7 +4,7 @@ use itertools::Itertools; use miette::IntoDiagnostic; use smtlib::{ and, - backend::{Backend, Cvc5Binary, Z3Binary}, + backend::{cvc5_binary::Cvc5Binary, z3_binary::Z3Binary, Backend}, distinct, or, terms::Sort, BitVec, Logic, SatResultWithModel, Solver, diff --git a/smtlib/examples/simplify.rs b/smtlib/examples/simplify.rs index 08c6869..f103c99 100644 --- a/smtlib/examples/simplify.rs +++ b/smtlib/examples/simplify.rs @@ -166,7 +166,8 @@ fn main() -> miette::Result<()> { let (expr, _) = parse_expr(&src); let smt = expr_to_smt(&expr); - let mut solver = smtlib::Solver::new(smtlib::backend::Z3Binary::new("z3").into_diagnostic()?)?; + let mut solver = + smtlib::Solver::new(smtlib::backend::z3_binary::Z3Binary::new("z3").into_diagnostic()?)?; let sexpr = solver.simplify(smt)?; let s = smt_to_expr(&sexpr); diff --git a/smtlib/src/lib.rs b/smtlib/src/lib.rs index 8b72884..e872126 100644 --- a/smtlib/src/lib.rs +++ b/smtlib/src/lib.rs @@ -12,18 +12,20 @@ pub use terms::Sort; pub use backend::Backend; pub use logics::Logic; -pub use smtlib_lowlevel::backend; +pub use smtlib_lowlevel::{self as lowlevel, backend}; -mod async_solver; +#[cfg(feature = "tokio")] +mod tokio_solver; #[rustfmt::skip] mod logics; mod solver; pub mod terms; pub mod theories; -pub use async_solver::AsyncSolver; pub use solver::Solver; pub use theories::{core::*, fixed_size_bit_vectors::*, ints::*, reals::*}; +#[cfg(feature = "tokio")] +pub use tokio_solver::TokioSolver; /// The satisfiability result produced by a solver #[derive(Debug)] @@ -155,7 +157,7 @@ impl Model { /// ``` /// # use smtlib::{Int, Sort}; /// # fn main() -> Result<(), Box> { - /// # let mut solver = smtlib::Solver::new(smtlib::backend::Z3Binary::new("z3")?)?; + /// # let mut solver = smtlib::Solver::new(smtlib::backend::z3_binary::Z3Binary::new("z3")?)?; /// let x = Int::from_name("x"); /// solver.assert(x._eq(12))?; /// let model = solver.check_sat_with_model()?.expect_sat()?; diff --git a/smtlib/src/solver.rs b/smtlib/src/solver.rs index 7b8f5d4..4177432 100644 --- a/smtlib/src/solver.rs +++ b/smtlib/src/solver.rs @@ -15,7 +15,7 @@ use crate::{terms::Dynamic, Bool, Error, Logic, Model, SatResult, SatResultWithM /// # use smtlib::{Int, Sort}; /// # fn main() -> Result<(), Box> { /// // 1. Set up the backend (in this case z3) -/// let backend = smtlib::backend::Z3Binary::new("z3")?; +/// let backend = smtlib::backend::z3_binary::Z3Binary::new("z3")?; /// // 2. Set up the solver /// let mut solver = smtlib::Solver::new(backend)?; /// // 3. Declare the necessary constants @@ -68,29 +68,18 @@ where ast::GeneralResponse::Error(_) => todo!(), } } + /// Runs the given command on the solver, and returns the result. + pub fn run_command(&mut self, cmd: &ast::Command) -> Result { + Ok(self.driver.exec(cmd)?) + } /// Adds the constraint of `b` as an assertion to the solver. To check for /// satisfiability call [`Solver::check_sat`] or /// [`Solver::check_sat_with_model`]. pub fn assert(&mut self, b: Bool) -> Result<(), Error> { - let term = ast::Term::from(b); - for q in term.all_consts() { - match q { - QualIdentifier::Identifier(_) => {} - QualIdentifier::Sorted(i, s) => match self.decls.entry(i.clone()) { - Entry::Occupied(stored) => assert_eq!(s, stored.get()), - Entry::Vacant(v) => { - v.insert(s.clone()); - match i { - Identifier::Simple(sym) => { - self.driver - .exec(&ast::Command::DeclareConst(sym.clone(), s.clone()))?; - } - Identifier::Indexed(_, _) => todo!(), - } - } - }, - } - } + let term = b.into(); + + self.declare_all_consts(&term)?; + let cmd = ast::Command::Assert(term); match self.driver.exec(&cmd)? { ast::GeneralResponse::Success => Ok(()), @@ -145,8 +134,20 @@ where } /// Simplifies the given term pub fn simplify(&mut self, t: Dynamic) -> Result { - let term = ast::Term::from(t); - for q in term.all_consts() { + self.declare_all_consts(&t.into())?; + + let cmd = ast::Command::Simplify(t.into()); + + match self.driver.exec(&cmd)? { + ast::GeneralResponse::SpecificSuccessResponse( + ast::SpecificSuccessResponse::SimplifyResponse(t), + ) => Ok(t.0), + res => todo!("{res:?}"), + } + } + + fn declare_all_consts(&mut self, t: &ast::Term) -> Result<(), Error> { + for q in t.all_consts() { match q { QualIdentifier::Identifier(_) => {} QualIdentifier::Sorted(i, s) => match self.decls.entry(i.clone()) { @@ -164,14 +165,6 @@ where }, } } - - let cmd = ast::Command::Simplify(t.into()); - - match self.driver.exec(&cmd)? { - ast::GeneralResponse::SpecificSuccessResponse( - ast::SpecificSuccessResponse::SimplifyResponse(t), - ) => Ok(t.0), - res => todo!("{res:?}"), - } + Ok(()) } } diff --git a/smtlib/src/async_solver.rs b/smtlib/src/tokio_solver.rs similarity index 82% rename from smtlib/src/async_solver.rs rename to smtlib/src/tokio_solver.rs index 5313132..f624fa9 100644 --- a/smtlib/src/async_solver.rs +++ b/smtlib/src/tokio_solver.rs @@ -4,21 +4,21 @@ use smtlib_lowlevel::{ ast::{self, Identifier, QualIdentifier}, backend, lexicon::Symbol, - AsyncDriver, + tokio::TokioDriver, }; use crate::{Bool, Error, Logic, Model, SatResult, SatResultWithModel}; -/// The [`AsyncSolver`] type is the primary entrypoint to interaction with the +/// The [`TokioSolver`] type is the primary entrypoint to interaction with the /// solver. Checking for validity of a set of assertions requires: /// ``` /// # use smtlib::{Int, Sort}; /// # fn main() -> Result<(), Box> { -/// # futures::executor::block_on(async { +/// # tokio_test::block_on(async { /// // 1. Set up the backend (in this case z3) -/// let backend = smtlib::backend::Z3Binary::new("z3")?; +/// let backend = smtlib::backend::z3_binary::tokio::Z3BinaryTokio::new("z3").await?; /// // 2. Set up the solver -/// let mut solver = smtlib::AsyncSolver::new(backend).await?; +/// let mut solver = smtlib::TokioSolver::new(backend).await?; /// // 3. Declare the necessary constants /// let x = Int::from_name("x"); /// // 4. Add assertions to the solver @@ -38,14 +38,14 @@ use crate::{Bool, Error, Logic, Model, SatResult, SatResultWithModel}; /// # } /// ``` #[derive(Debug)] -pub struct AsyncSolver { - driver: AsyncDriver, +pub struct TokioSolver { + driver: TokioDriver, decls: HashMap, } -impl AsyncSolver +impl TokioSolver where - B: backend::AsyncBackend, + B: backend::tokio::TokioBackend, { /// Construct a new solver provided with the backend to use. /// @@ -53,7 +53,7 @@ where /// documentation of the [`backend`] module. pub async fn new(backend: B) -> Result { Ok(Self { - driver: AsyncDriver::new(backend).await?, + driver: TokioDriver::new(backend).await?, decls: Default::default(), }) } @@ -70,9 +70,13 @@ where ast::GeneralResponse::Error(_) => todo!(), } } + /// Runs the given command on the solver, and returns the result. + pub async fn run_command(&mut self, cmd: &ast::Command) -> Result { + Ok(self.driver.exec(cmd).await?) + } /// Adds the constraint of `b` as an assertion to the solver. To check for - /// satisfiability call [`AsyncSolver::check_sat`] or - /// [`AsyncSolver::check_sat_with_model`]. + /// satisfiability call [`TokioSolver::check_sat`] or + /// [`TokioSolver::check_sat_with_model`]. pub async fn assert(&mut self, b: Bool) -> Result<(), Error> { let term = ast::Term::from(b); for q in term.all_consts() { @@ -102,10 +106,10 @@ where } } /// Checks for satisfiability of the assertions sent to the solver using - /// [`AsyncSolver::assert`]. + /// [`TokioSolver::assert`]. /// /// If you are interested in producing a model satisfying the assertions - /// check out [`AsyncSolver::check_sat`]. + /// check out [`TokioSolver::check_sat`]. pub async fn check_sat(&mut self) -> Result { let cmd = ast::Command::CheckSat; match self.driver.exec(&cmd).await? { @@ -121,10 +125,10 @@ where } } /// Checks for satisfiability of the assertions sent to the solver using - /// [`AsyncSolver::assert`], and produces a [model](Model) in case of `sat`. + /// [`TokioSolver::assert`], and produces a [model](Model) in case of `sat`. /// /// If you are not interested in the produced model, check out - /// [`AsyncSolver::check_sat`]. + /// [`TokioSolver::check_sat`]. pub async fn check_sat_with_model(&mut self) -> Result { match self.check_sat().await? { SatResult::Unsat => Ok(SatResultWithModel::Unsat), @@ -133,11 +137,11 @@ where } } /// Produces the model for satisfying the assertions. If you are looking to - /// retrieve a model after calling [`AsyncSolver::check_sat`], consider using - /// [`AsyncSolver::check_sat_with_model`] instead. + /// retrieve a model after calling [`TokioSolver::check_sat`], consider using + /// [`TokioSolver::check_sat_with_model`] instead. /// /// > **NOTE:** This must only be called after having called - /// > [`AsyncSolver::check_sat`] and it returning [`SatResult::Sat`]. + /// > [`TokioSolver::check_sat`] and it returning [`SatResult::Sat`]. pub async fn get_model(&mut self) -> Result { match self.driver.exec(&ast::Command::GetModel).await? { ast::GeneralResponse::SpecificSuccessResponse(