feat: external solver interface

enable calling external solver binaries directly from RustSAT

resolves #78

.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

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]

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::<rustsat::instances::BasicVarManager>::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,23 +48,29 @@ 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);
     ts.extend(quote! {
         #[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);
     ts.extend(quote! {
         #[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();

solvertests/src/lib.rs

@@ -14,8 +14,7 @@ enum InitBy {
 
 impl Parse for InitBy {
     fn parse(input: syn::parse::ParseStream) -> syn::Result<Self> {
-        let typr: syn::Result<Type> = input.parse();
-        Ok(if let Ok(typ) = typr {
+        Ok(if let syn::Result::<Type>::Ok(typ) = input.parse() {
             Self::Default(typ)
         } else {
             Self::Expr(input.parse()?)

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)]

src/instances/fio/dimacs.rs

@@ -507,7 +507,7 @@ pub fn write_cnf_annotated<W: Write>(
     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()
 }

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 `<stdout>`. 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"),
         }
     }
 }