diff --git a/.github/workflows/rustsat.yml b/.github/workflows/rustsat.yml index 488ed93b..2a283746 100644 --- a/.github/workflows/rustsat.yml +++ b/.github/workflows/rustsat.yml @@ -34,3 +34,21 @@ jobs: run: cargo test -p rustsat --verbose --features=all env: CMAKE_BUILD_PARALLEL_LEVEL: ${{ fromJSON('["", "4"]')[matrix.os == 'macos-latest'] }} + - name: CaDiCaL external solver + if: matrix.os == 'ubuntu-latest' + run: | + curl -O https://media.christophjabs.info/cadical-2-0-0 + chmod +x cadical-2-0-0 + RS_EXT_SOLVER=./cadical-2-0-0 cargo test --test external_solver --verbose -- --ignored + - name: Kissat external solver + if: matrix.os == 'ubuntu-latest' + run: | + curl -O https://media.christophjabs.info/kissat-3-1-1 + chmod +x kissat-3-1-1 + RS_EXT_SOLVER=./kissat-3-1-1 cargo test --test external_solver --verbose -- --ignored + - name: Gimsatul external solver + if: matrix.os == 'ubuntu-latest' + run: | + curl -O https://media.christophjabs.info/gimsatul-1-1-2 + chmod +x gimsatul-1-1-2 + RS_EXT_SOLVER=./gimsatul-1-1-2 cargo test --test external_solver --verbose -- --ignored diff --git a/Cargo.toml b/Cargo.toml index cf2c4d18..0f250fa7 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -42,6 +42,7 @@ rustsat-cadical = { version = "0.3.1", path = "./cadical" } rustsat-minisat = { version = "0.3.1", path = "./minisat" } rustsat-solvertests = { path = "./solvertests" } signal-hook = "0.3.17" +tempfile = "3.10.1" visibility = "0.1.0" xz2 = "0.1.7" @@ -67,10 +68,12 @@ bzip2 = { workspace = true, optional = true } flate2 = { workspace = true, optional = true } rand = { workspace = true, optional = true } rustc-hash = { workspace = true, optional = true } +tempfile.workspace = true xz2 = { workspace = true, optional = true } [dev-dependencies] -rustsat-minisat = { path = "./minisat" } +rustsat-minisat.workspace = true +rustsat-solvertests.workspace = true rustsat-tools = { path = "./tools" } [features] diff --git a/solvertests/src/integration.rs b/solvertests/src/integration.rs index 98d417aa..a5c75594 100644 --- a/solvertests/src/integration.rs +++ b/solvertests/src/integration.rs @@ -16,22 +16,16 @@ pub fn base(input: MacroInput) -> TokenStream { } }; let mut ts = quote! { + macro_rules! init_slv { + ($slv:ty) => { + <$slv>::default() + }; + ($init:expr) => { + $init + }; + } + macro_rules! test_inst { - ($slv:ty, $inst:expr, $res:expr) => {{ - let manifest = std::env::var("CARGO_MANIFEST_DIR").unwrap(); - let mut solver = <$slv>::default(); - let inst = rustsat::instances::SatInstance::::from_dimacs_path(format!("{manifest}/{}", $inst)) - .expect("failed to parse instance"); - rustsat::solvers::Solve::add_cnf_ref(&mut solver, inst.cnf()) - .expect("failed to add cnf to solver"); - let res = rustsat::solvers::Solve::solve(&mut solver).expect("failed solving"); - assert_eq!(res, $res); - if $res == rustsat::solvers::SolverResult::Sat { - let sol = rustsat::solvers::Solve::solution(&solver, inst.max_var().expect("no variables in instance")) - .expect("failed to get solution from solver"); - assert!(inst.is_sat(&sol)); - } - }}; ($init:expr, $inst:expr, $res:expr) => {{ let manifest = std::env::var("CARGO_MANIFEST_DIR").unwrap(); let mut solver = $init; @@ -54,7 +48,9 @@ pub fn base(input: MacroInput) -> TokenStream { #[test] #ignore fn small_sat() { - test_inst!(#slv, "data/AProVE11-12.cnf", rustsat::solvers::SolverResult::Sat); + let testid = "small_sat"; + let solver = init_slv!(#slv); + test_inst!(solver, "data/AProVE11-12.cnf", rustsat::solvers::SolverResult::Sat); } }); let ignore = ignoretok(1); @@ -62,7 +58,9 @@ pub fn base(input: MacroInput) -> TokenStream { #[test] #ignore fn small_unsat() { - test_inst!(#slv, "data/smtlib-qfbv-aigs-ext_con_032_008_0256-tseitin.cnf", rustsat::solvers::SolverResult::Unsat); + let testid = "small_unsat"; + let solver = init_slv!(#slv); + test_inst!(solver, "data/smtlib-qfbv-aigs-ext_con_032_008_0256-tseitin.cnf", rustsat::solvers::SolverResult::Unsat); } }); let ignore = ignoretok(2); @@ -70,7 +68,9 @@ pub fn base(input: MacroInput) -> TokenStream { #[test] #ignore fn minisat_segfault() { - test_inst!(#slv, "data/minisat-segfault.cnf", rustsat::solvers::SolverResult::Unsat); + let testid = "minisat_segfault"; + let solver = init_slv!(#slv); + test_inst!(solver, "data/minisat-segfault.cnf", rustsat::solvers::SolverResult::Unsat); } }); ts @@ -106,6 +106,7 @@ pub fn incremental(input: MacroInput) -> TokenStream { solvers::{Solve, SolveIncremental, SolverResult::{Sat, Unsat}}, }; + let testid = "assumption_sequence"; let mut solver = init_slv!(#slv); let inst: SatInstance = SatInstance::from_dimacs_path("data/small.cnf").unwrap(); @@ -214,6 +215,7 @@ pub fn phasing(input: MacroInput) -> TokenStream { types::TernaryVal::{True, False}, var, }; + let testid = "user_phases"; let mut solver = init_slv!(#slv); let inst: SatInstance = SatInstance::from_dimacs_path("data/small.cnf").unwrap(); diff --git a/solvertests/src/lib.rs b/solvertests/src/lib.rs index e8a0bea1..9251c2a0 100644 --- a/solvertests/src/lib.rs +++ b/solvertests/src/lib.rs @@ -14,8 +14,7 @@ enum InitBy { impl Parse for InitBy { fn parse(input: syn::parse::ParseStream) -> syn::Result { - let typr: syn::Result = input.parse(); - Ok(if let Ok(typ) = typr { + Ok(if let syn::Result::::Ok(typ) = input.parse() { Self::Default(typ) } else { Self::Expr(input.parse()?) diff --git a/src/instances/fio.rs b/src/instances/fio.rs index a5e3ebb2..6da5e430 100644 --- a/src/instances/fio.rs +++ b/src/instances/fio.rs @@ -11,7 +11,10 @@ use std::{ }; use thiserror::Error; -use crate::types::{self, Assignment}; +use crate::{ + solvers::{SolverResult, SolverState}, + types::{self, Assignment}, +}; pub mod dimacs; pub mod opb; @@ -99,6 +102,24 @@ pub enum SolverOutput { Unknown, } +impl SolverOutput { + pub(crate) fn result(&self) -> SolverResult { + match self { + SolverOutput::Sat(_) => SolverResult::Sat, + SolverOutput::Unsat => SolverResult::Unsat, + SolverOutput::Unknown => SolverResult::Interrupted, + } + } + + pub(crate) fn state(&self) -> SolverState { + match self { + SolverOutput::Sat(_) => SolverState::Sat, + SolverOutput::Unsat => SolverState::Unsat, + SolverOutput::Unknown => SolverState::Unknown, + } + } +} + /// Possible errors in SAT solver output parsing #[derive(Error, Debug)] #[allow(clippy::enum_variant_names)] diff --git a/src/instances/fio/dimacs.rs b/src/instances/fio/dimacs.rs index 07dfaa81..9b670ef3 100644 --- a/src/instances/fio/dimacs.rs +++ b/src/instances/fio/dimacs.rs @@ -507,7 +507,7 @@ pub fn write_cnf_annotated( n_vars: u32, ) -> Result<(), io::Error> { writeln!(writer, "c CNF file written by RustSAT")?; - writeln!(writer, "p cnf {} {}", n_vars, cnf.len())?; + writeln!(writer, "p cnf {n_vars} {}", cnf.len())?; cnf.iter().try_for_each(|cl| write_clause(writer, cl))?; writer.flush() } diff --git a/src/solvers.rs b/src/solvers.rs index 1fd5c590..74e38e6a 100644 --- a/src/solvers.rs +++ b/src/solvers.rs @@ -76,6 +76,12 @@ //! - Fork used in solver crate: //! [https://github.com/chrjabs/glucose4](https://github.com/chrjabs/glucose4) //! +//! ### External Solvers +//! +//! RustSAT provides an interface for calling external solver binaries by passing them DIMACS input +//! and parsing their output written to ``. For more details, see the [`ExternalSolver`] +//! type. +//! //! ### IPASIR //! //! [IPASIR](https://github.com/biotomas/ipasir) is a C API for incremental SAT @@ -93,6 +99,9 @@ use core::time::Duration; use std::fmt; use thiserror::Error; +pub mod external; +pub use external::Solver as ExternalSolver; + /// Trait for all SAT solvers in this library. /// Solvers outside of this library can also implement this trait to be able to /// use them with this library. @@ -517,6 +526,8 @@ pub enum SolverState { Sat, /// The query was found unsatisfiable. Unsat, + /// Solving was terminated before a conclusion was reached + Unknown, } impl fmt::Display for SolverState { @@ -526,6 +537,7 @@ impl fmt::Display for SolverState { SolverState::Input => write!(f, "INPUT"), SolverState::Sat => write!(f, "SAT"), SolverState::Unsat => write!(f, "UNSAT"), + SolverState::Unknown => write!(f, "UNKNOWN"), } } } diff --git a/src/solvers/external.rs b/src/solvers/external.rs new file mode 100644 index 00000000..67284dd6 --- /dev/null +++ b/src/solvers/external.rs @@ -0,0 +1,431 @@ +//! # Solver Inferface for External Executables + +use std::{ + fs, io, + path::{Path, PathBuf}, + process::{self, Command}, +}; + +use crate::{ + instances::{ + fio::{self, SolverOutput}, + Cnf, + }, + types::{Assignment, Clause}, +}; + +use super::Solve; + +/// Specifies what argument position the instance is passed to the solver at +/// +/// Most solvers expect the instance as the last argument +#[derive(Debug, Clone, Copy, Default, PartialEq, Eq)] +enum InstanceArg { + /// Pass the instance file path as the first solver argument + First, + /// Pass the instance file path as the last argument + #[default] + Last, +} + +/// Options for how the input instance should be passed to the external solver +#[derive(Debug, Clone)] +pub struct InputVia(InputViaInt); + +#[derive(Debug, Clone)] +enum InputViaInt { + /// Passes the instance by writing it to a file at the specified path + /// + /// The file will _not_ be removed afterwards + File(PathBuf, InstanceArg), + /// Passes the instance by writing it to a temporary file that will automatically be removed + TempFile(InstanceArg), + /// Passes the instance through a pipe to `stdin` + /// + /// Note, not all solvers support reading input from `stdin` + Pipe, +} + +impl InputVia { + /// Pass the input via a persistent file at `path`, passed to the solver as the last argument + #[must_use] + pub fn file_last>(path: P) -> Self { + InputVia(InputViaInt::File( + path.as_ref().to_path_buf(), + InstanceArg::Last, + )) + } + + /// Pass the input via a persistent file at `path`, passed to the solver as the first argument + #[must_use] + pub fn file_first>(path: P) -> Self { + InputVia(InputViaInt::File( + path.as_ref().to_path_buf(), + InstanceArg::First, + )) + } + + /// Pass the input via a temporary file, passed to the solver as the last argument + #[must_use] + pub fn tempfile_last() -> Self { + InputVia(InputViaInt::TempFile(InstanceArg::Last)) + } + + /// Pass the input via a temporary file, passed to the solver as the first argument + #[must_use] + pub fn tempfile_first() -> Self { + InputVia(InputViaInt::TempFile(InstanceArg::First)) + } + + /// Pass the input via a pipe to `` + #[must_use] + pub fn pipe() -> Self { + InputVia(InputViaInt::Pipe) + } +} + +impl Default for InputVia { + fn default() -> Self { + InputVia(InputViaInt::TempFile(InstanceArg::default())) + } +} + +/// Options for how the output of the solver is read by RustSAT +#[derive(Debug, Clone, Default)] +pub struct OutputVia(OutputViaInt); + +#[derive(Debug, Clone, Default)] +enum OutputViaInt { + /// The solver output is written to a file at the given path that is not automatically deleted + File(PathBuf), + /// The solver output is read directly through a pipe + #[default] + Pipe, +} + +impl OutputVia { + /// Process the solver output via a persistent file at `path` + #[must_use] + pub fn file>(path: P) -> Self { + OutputVia(OutputViaInt::File(path.as_ref().to_path_buf())) + } + + /// Process the solver output via a pipe from `` + #[must_use] + pub fn pipe() -> Self { + OutputVia(OutputViaInt::Pipe) + } +} + +/// A solver called via an external executable +/// +/// This solver will perform a call to the solver executable via [`Command`] and parse the solver +/// output via [`fio::parse_sat_solver_output`] +#[derive(Debug)] +pub struct Solver { + signature: &'static str, + state: SolverState, +} + +#[derive(Debug)] +enum SolverState { + Pre(SolverPre), + Post(fio::SolverOutput), +} + +/// State before calling the external solver +#[derive(Debug)] +struct SolverPre { + cmd: Command, + input: InputVia, + output: OutputVia, + cnf: Cnf, + n_vars: u32, +} + +impl Solver { + /// Initializes a solver with a [`Command`] that is fully set up, except for the input instance + /// + /// # Notes + /// + /// - If input is passed via a file with a path that ends in a compression extension, RustSAT + /// will write a compressed file + /// - If the solver output is processed via a file, compression is _not_ supported + /// - If [`Command::env_clear`] was called on the command and the input is passed via a + /// file as the first argument, the fact that the environment has been cleared might be + /// forgotten + /// + /// # Example + /// + /// ``` + /// use std::process::Command; + /// use rustsat::solvers::{ExternalSolver, external}; + /// let solver = ExternalSolver::new( + /// Command::new(""), + /// external::InputVia::tempfile_last(), + /// external::OutputVia::pipe(), + /// "solver-signature", + /// ); + /// ``` + /// After this initialization, the `solver` instance can be used with the [`Solve`] trait. + #[must_use] + pub fn new(cmd: Command, input: InputVia, output: OutputVia, signature: &'static str) -> Self { + Solver { + signature, + state: SolverState::Pre(SolverPre { + cmd, + input, + output, + cnf: Cnf::default(), + n_vars: 0, + }), + } + } + + /// Initializes a solver with default values for [`InputVia`] and [`OutputVia`] + /// + /// The default values are passing the input via a temporary file and processing the output via + /// a pipe. + /// + /// # Example + /// + /// ``` + /// use std::process::Command; + /// use rustsat::solvers::{ExternalSolver, external}; + /// let solver = ExternalSolver::new_default( + /// Command::new(""), + /// "solver-signature", + /// ); + /// ``` + /// After this initialization, the `solver` instance can be used with the [`Solve`] trait. + #[must_use] + pub fn new_default(cmd: Command, signature: &'static str) -> Self { + Solver::new(cmd, InputVia::default(), OutputVia::default(), signature) + } +} + +impl Solve for Solver { + fn signature(&self) -> &'static str { + self.signature + } + + fn solve(&mut self) -> anyhow::Result { + if let SolverState::Post(state) = &self.state { + anyhow::bail!(super::StateError { + required_state: super::SolverState::Input, + actual_state: match state { + fio::SolverOutput::Sat(_) => super::SolverState::Sat, + fio::SolverOutput::Unsat => super::SolverState::Unsat, + fio::SolverOutput::Unknown => super::SolverState::Unknown, + } + }); + } + let SolverState::Pre(config) = + std::mem::replace(&mut self.state, SolverState::Post(SolverOutput::Unknown)) + else { + unreachable!() + }; + let post = call_external(config)?; + let res = post.result(); + self.state = SolverState::Post(post); + Ok(res) + } + + fn lit_val(&self, lit: crate::types::Lit) -> anyhow::Result { + match &self.state { + SolverState::Pre(_) => anyhow::bail!(super::StateError { + required_state: super::SolverState::Sat, + actual_state: super::SolverState::Input + }), + SolverState::Post(SolverOutput::Sat(sol)) => Ok(sol.lit_value(lit)), + SolverState::Post(state) => anyhow::bail!(super::StateError { + required_state: super::SolverState::Sat, + actual_state: state.state() + }), + } + } + + fn add_clause_ref(&mut self, clause: &Clause) -> anyhow::Result<()> { + self.add_clause(clause.clone()) + } + + fn solution(&self, high_var: crate::types::Var) -> anyhow::Result { + match &self.state { + SolverState::Pre(_) => anyhow::bail!(super::StateError { + required_state: super::SolverState::Sat, + actual_state: super::SolverState::Input + }), + SolverState::Post(SolverOutput::Sat(sol)) => Ok(sol.clone().truncate(high_var)), + SolverState::Post(state) => anyhow::bail!(super::StateError { + required_state: super::SolverState::Sat, + actual_state: state.state() + }), + } + } + + fn add_clause(&mut self, clause: Clause) -> anyhow::Result<()> { + let state = match &mut self.state { + SolverState::Pre(state) => state, + SolverState::Post(state) => anyhow::bail!(super::StateError { + required_state: super::SolverState::Input, + actual_state: state.state() + }), + }; + for lit in &clause { + state.n_vars = std::cmp::max(lit.var().idx32() + 1, state.n_vars); + } + state.cnf.add_clause(clause); + Ok(()) + } +} + +impl Extend for Solver { + fn extend>(&mut self, iter: T) { + iter.into_iter().for_each(|cl| { + self.add_clause(cl).expect("Error adding clause in extend"); + }); + } +} + +impl<'a> Extend<&'a Clause> for Solver { + fn extend>(&mut self, iter: T) { + iter.into_iter().for_each(|cl| { + self.add_clause_ref(cl) + .expect("Error adding clause in extend"); + }); + } +} + +macro_rules! check_exit_code { + ($status:expr) => { + match $status.code() { + // these are the expected return codes for SAT solvers + // we don't check them against the ouput though + Some(0 | 10 | 20) => (), + Some(x) => anyhow::bail!("solver returned unexpected code {x}"), + None => anyhow::bail!("solver process terminated by signal"), + }; + }; +} + +fn call_external(config: SolverPre) -> anyhow::Result { + // when writing to a temporary file, this needs to be explicitly closed at the end + let mut temppath = None; + // build the final command + let mut cmd = match config.input.0 { + InputViaInt::File(in_path, argpos) => { + // write input to file + fio::dimacs::write_cnf_annotated( + &mut fio::open_compressed_uncompressed_write(&in_path)?, + &config.cnf, + config.n_vars, + )?; + construct_command_path(config.cmd, in_path, argpos) + } + InputViaInt::TempFile(argpos) => { + let mut writer = io::BufWriter::new(tempfile::NamedTempFile::new()?); + // write input to file + fio::dimacs::write_cnf_annotated(&mut writer, &config.cnf, config.n_vars)?; + let path = writer.into_inner()?.into_temp_path(); + let cmd = construct_command_path(config.cmd, path.to_path_buf(), argpos); + temppath = Some(path); + cmd + } + InputViaInt::Pipe => { + let mut cmd = config.cmd; + cmd.stdin(process::Stdio::piped()); + match config.output.0 { + OutputViaInt::File(path) => { + // pipe output into file and spawn + // NOTE: this currently does not support compression + let mut child = cmd.stdout(fs::File::create(&path)?).spawn()?; + // write input to stdin + let mut stdin = io::BufWriter::new(child.stdin.take().unwrap()); + fio::dimacs::write_cnf_annotated(&mut stdin, &config.cnf, config.n_vars)?; + drop(stdin); + let exit = child.wait()?; + // parse output from file + let output = fio::parse_sat_solver_output(&mut io::BufReader::new( + fs::File::open(&path)?, + ))?; + check_exit_code!(exit); + return Ok(output); + } + OutputViaInt::Pipe => { + let mut child = cmd.stdout(process::Stdio::piped()).spawn()?; + let mut stdin = io::BufWriter::new(child.stdin.take().unwrap()); + // second thread for processing stdout to avoid blocking + let mut stdout = io::BufReader::new(child.stdout.take().unwrap()); + let output_handle = + std::thread::spawn(move || -> anyhow::Result<(fio::SolverOutput, io::BufReader)> { + // this thread passes stdout back to ensure that it remains open long + // enough for the solver to terminate + let output = fio::parse_sat_solver_output(&mut stdout)?; + Ok((output, stdout)) + }); + // main thread writes input to stdin + fio::dimacs::write_cnf_annotated(&mut stdin, &config.cnf, config.n_vars)?; + drop(stdin); + let exit = child.wait()?; + let (output, stdout) = output_handle + .join() + .expect("could not join output parsing thread")?; + drop(stdout); + check_exit_code!(exit); + return Ok(output); + } + } + } + }; + // case input pipe handeled above + let output = match config.output.0 { + OutputViaInt::File(path) => { + // pipe output into file + // NOTE: this currently does not support compression + cmd.stdout(fs::File::create(&path)?); + let exit = cmd.status()?; + let output = + fio::parse_sat_solver_output(&mut io::BufReader::new(fs::File::open(&path)?))?; + check_exit_code!(exit); + output + } + OutputViaInt::Pipe => { + let mut child = cmd.stdout(process::Stdio::piped()).spawn()?; + let mut stdout = io::BufReader::new(child.stdout.take().unwrap()); + let output = fio::parse_sat_solver_output(&mut stdout)?; + check_exit_code!(child.wait()?); + // keep pipe open till after child has terminated + drop(stdout); + output + } + }; + if let Some(temppath) = temppath { + temppath.close()?; + } + Ok(output) +} + +fn construct_command_path(mut cmd: Command, path: PathBuf, argpos: InstanceArg) -> Command { + match argpos { + InstanceArg::First => { + // reconstruct command with argument at the beginning + let mut new_cmd = Command::new(cmd.get_program()); + new_cmd.arg(path).args(cmd.get_args()); + for (key, val) in cmd.get_envs() { + if let Some(val) = val { + new_cmd.env(key, val); + } else { + new_cmd.env_remove(key); + } + } + if let Some(dir) = cmd.get_current_dir() { + new_cmd.current_dir(dir); + } + new_cmd + } + InstanceArg::Last => { + cmd.arg(path); + cmd + } + } +} diff --git a/tests/external_solver.rs b/tests/external_solver.rs new file mode 100644 index 00000000..2c3fc630 --- /dev/null +++ b/tests/external_solver.rs @@ -0,0 +1,120 @@ +mod file_file { + use rustsat::solvers::{external, ExternalSolver}; + use std::process::Command; + + rustsat_solvertests::base_tests!( + { + let manifest = std::env::var("CARGO_MANIFEST_DIR").unwrap(); + let slv = std::env::var("RS_EXT_SOLVER").expect( + "please set the `RS_EXT_SOLVER` enviroment variable to run tests for external solvers", + ); + ExternalSolver::new( + Command::new(slv), + external::InputVia::file_last(format!( + "{manifest}/target/extsolver_file_file_{testid}.cnf" + )), + external::OutputVia::file(format!( + "{manifest}/target/extsolver_file_file_{testid}.log" + )), + "extsolver", + ) + }, + true, + true, + true + ); +} + +mod file_pipe { + use rustsat::solvers::{external, ExternalSolver}; + use std::process::Command; + + rustsat_solvertests::base_tests!( + { + let manifest = std::env::var("CARGO_MANIFEST_DIR").unwrap(); + let slv = std::env::var("RS_EXT_SOLVER").expect( + "please set the `RS_EXT_SOLVER` enviroment variable to run tests for external solvers", + ); + ExternalSolver::new( + Command::new(slv), + external::InputVia::file_last(format!( + "{manifest}/target/extsolver_file_pipe_{testid}.cnf" + )), + external::OutputVia::pipe(), + "extsolver", + ) + }, + true, + true, + true + ); +} + +mod tempfile_pipe { + use rustsat::solvers::{external, ExternalSolver}; + use std::process::Command; + + rustsat_solvertests::base_tests!( + { + let slv = std::env::var("RS_EXT_SOLVER").expect( + "please set the `RS_EXT_SOLVER` enviroment variable to run tests for external solvers", + ); + ExternalSolver::new( + Command::new(slv), + external::InputVia::tempfile_last(), + external::OutputVia::pipe(), + "extsolver", + ) + }, + true, + true, + true + ); +} + +mod pipe_pipe { + use rustsat::solvers::{external, ExternalSolver}; + use std::process::Command; + + rustsat_solvertests::base_tests!( + { + let slv = std::env::var("RS_EXT_SOLVER").expect( + "please set the `RS_EXT_SOLVER` enviroment variable to run tests for external solvers", + ); + ExternalSolver::new( + Command::new(slv), + external::InputVia::pipe(), + external::OutputVia::pipe(), + "extsolver", + ) + }, + true, + true, + true + ); +} + +mod pipe_file { + use rustsat::solvers::{external, ExternalSolver}; + use std::process::Command; + + rustsat_solvertests::base_tests!( + { + let slv = std::env::var("RS_EXT_SOLVER").expect( + "please set the `RS_EXT_SOLVER` enviroment variable to run tests for external solvers", + ); + let manifest = std::env::var("CARGO_MANIFEST_DIR").unwrap(); + ExternalSolver::new( + Command::new(slv), + external::InputVia::pipe(), + external::OutputVia::file(format!( + "{manifest}/target/extsolver_pipe_file_{testid}.log" + )), + "extsolver", + ) + }, + true, + true, + true + ); +}