Repository: chrjabs/rustsat (language: python)

Issue:
Support for external solvers and solver output parsing?
Hi, I'm checking if there are any plans or thoughts related to these features that would be useful for us:

1. Ability to read and parse [solver output files](https://satcompetition.github.io/2024/output.html) into `rustsat::types::Assignment` objects, maybe something like `Assignment::from_solver_output(reader)` and `Assignment::from_solver_output_path(path)`.
2. Ability to run an external program as a solver. The user would just specify the path + command line arguments, and under the hood it'd invoke an external process, pipe the output of `SatInstance::to_dimacs` to the solver, check the exit status as usual (supporting also external processes that report satisfiability using [error codes 0/10/20](http://www.satcompetition.org/2004/format-solvers2004.html)) and parse the output using `Assignment::from_solver_output`.

In particular, we'd be currently interested in using multi-threaded [Gimsatul](https://github.com/arminbiere/gimsatul) as the external solver.

Here feature 1 alone would already be useful, and even if we had feature 2, we'd still like to have also feature 1, as it'd make it possible to have workflows in which e.g. SAT instance generation and solution parsing is done on one computer, while SAT solving is done in another machine.

If it helps, I can try to find someone who could contribute these features, but I'd like to first know if this makes sense, if this kind of features should be insider RustSAT or in another crate that depends on it, and if there are already some plans related to this?


Discussion / hints:
Since I am developing RustSAT mainly based on what I need for my own work, there isn't really a clear roadmap for what I would want to do (except for some rough ideas tracked as issues). That being said, I agree that a more flexible option to include any solver via files/pipes sounds quite helpful, and I think it would nicely extend RustSAT. I can give this a try myself sometime, but if you need it urgently, you would need to find somebody else to contribute this.
Skimming through gimsatul a bit right now, it looks like including it via the API more directly is not as trivial as for the other solvers I've worked on so far. So even more reason to add functionality for external solvers.
Since I am not sure when I will get to this, I'll drop some notes on how I would approach this here, in case somebody else wants to pick this up. Also, if anybody is interested to do this, feel free to reach out to me to talk about this more.

Solver output parsing:
- Add `Assignment::from_vline(line: String)` function, creating an assignment from a solver output assignment line (starting with a `v `, hence dubbed v-line
- Add `Assignment::from_solver_output<R: BufRead>(reader: R)`, scanning through solver output and calling `from_vline` when a v-line is detected
- Add `Assignment::from_solver_output_path<P: AsRef<Path>>(path: P)` calling `from_solver_output`

External solver:
- Implement in `rustsat::solvers::external` and reexport main type(s) from `rustsat::solvers`
- One main type `ExternalSolver` with a `ExternalSolver::new(config: Config)` initializer
- `Config` specifies executable path, optional arguments, whether to write output to file or capture via a pipe, ...
- Run solver via `std::process::Command`
- Detect solving result from exit code or s-line and parse solution from v-line

If I get to this at one point myself, these notes should also be quite helpful.
Hi @chrjabs. I am currently working on the first problem @suomela mentioned. I have a few questions about the implementation.
1. Is there any style that I have to format my code according to?
2. Can I create new enum for the return value like SATISFIABLE, UNSAT,. I did not see such an enum in the documentation file?
3. This roughly the code if there is anything you want to point out please do so.
```rust
///Get the solution from a solvers output
    pub fn from_solver_output_path(&mut self, filepath: &str) -> Option<SATRESULT> {
        let sat_solution_file = fs::File::open(filepath).expect("Can not read SAT solution file");

        let sat_solution_reader = BufReader::new(sat_solution_file);

        let sat_result: &str = "";

        for line in sat_solution_reader.lines() {
            let line_ls = line.as_ref().expect("Couldn't read SAT solution line");
            
            if line_ls.starts_with('s') {
                for result_of_sat in ["SATISFIABLE", "UNSATISFIABLE", "UNKNOWN"] {
                    if line_ls.contains(result_of_sat) {
                        //We have a solution line
                        sat_result = result_of_sat;
                    }
                }
            }
            
            if line_ls.starts_with('v') {
                // There is a solution and the literals have values 
                //I assume that the output literal is 2*variable_index + signe
                for number in line_ls.split(' ') {
                    if number.parse::<u32>().is_ok() {
                        let number_v = number.parse::<u32>().unwrap();
                        //End of the value lines
                        if number_v == 0 {
                            continue;
                        }
                        self.assignment[(number_v >> 1) as usize] = match number_v > 0 {
                            true => TernaryVal::True,
                            false => TernaryVal::False,
                        };
                    }
                }
            }
        }
        
        return match sat_result {
            "SATISFIABLE" => Some(SATRESULT::SATISFIABLE),
            _ => None,
        };
    
    }
```
1. Yes, please use `rustfmt` via `cargo fmt --all` to format code

I guess I should write some proper contribution guidelines, now that some more people are working with this library.

Some more general thoughts on this now that I see your code:

Maybe it makes more sense to have a separate parsing function within the [`fio` module](https://github.com/chrjabs/rustsat/blob/main/rustsat/src/instances/fio.rs), something along the lines of this
```rust
pub enum SolverOutput {
    Sat(Assignment),
    Unsat,
    Unknown,
}

pub fn parse_sat_solver_output<R: BufRead>(reader: R) -> anyhow::Result<SolverOutput> {
    // Parsing code goes here
    // when encoutering vline, call `Assignment::from_vline`
}
```
And then in `Assignment` one could do
```rust
impl Assignment {
    pub fn from_solver_output_path<P: AsRef<Path>>(path: P) -> anyhow::Result<Self> {
        let reader = fio::open_compressed_uncompressed_read(path).context("failed to open reader")?;
        match fio::parse_sat_solver_output(reader) {
            SolverOutput::Sat(assignment) => assignment,
            _ => // return some error
        }
    }

    pub fn from_vline(line: &str) -> Assignment {
        // parse the actual vline
    }
}
```
I guess this would feel a bit more clean to me and the `parse_sat_solver_output` function could then also be used in the `ExternalSolver` type in the future.

Two more things:
- Make sure to use [`Lit::from_ipasir`](https://docs.rs/rustsat/latest/rustsat/types/struct.Lit.html#method.from_ipasir) in combination with [`Lit::vidx`](https://docs.rs/rustsat/latest/rustsat/types/struct.Lit.html#method.vidx) to index the assignment correctly
- It would be great if `Assignment::from_vline` could support the newer [v-line format of the MaxSAT evaluation](https://maxsat-evaluations.github.io/2022/vline.html) as well (even though I'm not sure there any SAT solvers outputting in the format)

Thanks for working on this and feel free to open a draft pull request once you have some things done, it might be easier to comment on the actual code.
Hi @chrjabs. I think I am almost finished (okay I just miracolusly used rm -rf in the wrong directory), but still I have one problems now.
1. In the code that you have sent  the `let reader = fio::open_compressed_uncompressed_read(path).context("failed to open reader")?;` variable does not satisfy the BufRead trait and I could not solve this.
Just wrap the reader in a [`std::io::BufReader`](https://doc.rust-lang.org/stable/std/io/struct.BufReader.html). In the file parsers in the `fio` module I'm mostly doing that inside the parser function, but I should change that to not potentially buffer a reader again that is already buffered.

Fix patch:
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/cadical/examples/cadical-cli.rs b/cadical/examples/cadical-cli.rs
index 6db718af..30c91399 100644
--- a/cadical/examples/cadical-cli.rs
+++ b/cadical/examples/cadical-cli.rs
@@ -43,10 +43,13 @@ fn main() -> anyhow::Result<()> {
                 .context("error parsing the input file as OPB")?,
         }
     } else if args.opb {
-        SatInstance::from_opb(io::BufReader::new(io::stdin()), opb::Options::default())
-            .context("error parsing input as OPB")?
+        SatInstance::from_opb(
+            &mut io::BufReader::new(io::stdin()),
+            opb::Options::default(),
+        )
+        .context("error parsing input as OPB")?
     } else {
-        SatInstance::from_dimacs(io::BufReader::new(io::stdin()))
+        SatInstance::from_dimacs(&mut io::BufReader::new(io::stdin()))
             .context("error parsing input as CNF")?
     };
 
diff --git a/kissat/examples/kissat-cli.rs b/kissat/examples/kissat-cli.rs
index a8c26084..b641ace5 100644
--- a/kissat/examples/kissat-cli.rs
+++ b/kissat/examples/kissat-cli.rs
@@ -43,10 +43,13 @@ fn main() -> anyhow::Result<()> {
                 .context("error parsing the input file as OPB")?,
         }
     } else if args.opb {
-        SatInstance::from_opb(io::BufReader::new(io::stdin()), opb::Options::default())
-            .context("error parsing input as OPB")?
+        SatInstance::from_opb(
+            &mut io::BufReader::new(io::stdin()),
+            opb::Options::default(),
+        )
+        .context("error parsing input as OPB")?
     } else {
-        SatInstance::from_dimacs(io::BufReader::new(io::stdin()))
+        SatInstance::from_dimacs(&mut io::BufReader::new(io::stdin()))
             .context("error parsing input as CNF")?
     };
 
diff --git a/minisat/examples/minisat-cli.rs b/minisat/examples/minisat-cli.rs
index 48ccc23e..60d1d1cc 100644
--- a/minisat/examples/minisat-cli.rs
+++ b/minisat/examples/minisat-cli.rs
@@ -46,10 +46,13 @@ fn main() -> anyhow::Result<()> {
                 .context("error parsing the input file as OPB")?,
         }
     } else if args.opb {
-        SatInstance::from_opb(io::BufReader::new(io::stdin()), opb::Options::default())
-            .context("error parsing input as OPB")?
+        SatInstance::from_opb(
+            &mut io::BufReader::new(io::stdin()),
+            opb::Options::default(),
+        )
+        .context("error parsing input as OPB")?
     } else {
-        SatInstance::from_dimacs(io::BufReader::new(io::stdin()))
+        SatInstance::from_dimacs(&mut io::BufReader::new(io::stdin()))
             .context("error parsing input as CNF")?
     };
 
diff --git a/src/encodings/am1.rs b/src/encodings/am1.rs
index 6f6b1684..a60e5b37 100644
--- a/src/encodings/am1.rs
+++ b/src/encodings/am1.rs
@@ -3,7 +3,7 @@
 //! The module contains implementations of CNF encodings for at-most-1
 //! constraints.
 //!
-//! ## Example Useage
+//! ## Example Usage
 //!
 //! ```
 //! # use rustsat::{
diff --git a/src/encodings/card.rs b/src/encodings/card.rs
index 73f02566..cd3a5d52 100644
--- a/src/encodings/card.rs
+++ b/src/encodings/card.rs
@@ -4,7 +4,7 @@
 //! constraints. It defines traits for (non-)incremental cardinality constraints
 //! and encodings implementing these traits.
 //!
-//! ## Example Useage
+//! ## Example Usage
 //!
 //! ```
 //! # use rustsat::{
diff --git a/src/encodings/pb.rs b/src/encodings/pb.rs
index 2015cb5b..eec4d438 100644
--- a/src/encodings/pb.rs
+++ b/src/encodings/pb.rs
@@ -4,7 +4,7 @@
 //! constraints. It defines traits for (non-)incremental PB constraints and
 //! encodings implementing these traits.
 //!
-//! ## Example Useage
+//! ## Example Usage
 //!
 //! ```
 //! # use rustsat::{
diff --git a/src/instances/fio.rs b/src/instances/fio.rs
index f8801190..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)]
@@ -120,7 +141,7 @@ pub enum SatSolverOutputError {
 ///
 /// Either [`SatSolverOutputError`], [`types::InvalidVLine`], or other parsing errors on invalid
 /// input.
-pub fn parse_sat_solver_output<R: BufRead>(reader: R) -> anyhow::Result<SolverOutput> {
+pub fn parse_sat_solver_output<R: BufRead>(reader: &mut R) -> anyhow::Result<SolverOutput> {
     let mut is_sat = false;
     let mut solution: Option<Assignment> = None;
 
@@ -184,50 +205,43 @@ mod tests {
         ]));
 
         let data = "c this is a comment\ns SATISFIABLE\nv 1 -2 4 -5 6 0\n";
-        let reader = io::Cursor::new(data);
-        let res = parse_sat_solver_output(reader).unwrap();
+        let res = parse_sat_solver_output(&mut io::Cursor::new(data)).unwrap();
         assert_eq!(res, ground_truth);
 
         let data = "c this is a comment\nv 1 -2 4 -5 6 0\ns SATISFIABLE\n";
-        let reader = io::Cursor::new(data);
-        let res = parse_sat_solver_output(reader).unwrap();
+        let res = parse_sat_solver_output(&mut io::Cursor::new(data)).unwrap();
         assert_eq!(res, ground_truth);
 
         let data = "c this is a comment\ns SATISFIABLE\nv 1 -2 4 \nv -5 6 0\n";
-        let reader = io::Cursor::new(data);
-        let res = parse_sat_solver_output(reader).unwrap();
+        let res = parse_sat_solver_output(&mut io::Cursor::new(data)).unwrap();
         assert_eq!(res, ground_truth);
     }
 
     #[test]
     fn parse_solver_output_unsat() {
         let data = "c this is a comment\ns UNSATISFIABLE\n";
-        let reader = io::Cursor::new(data);
-        let res = parse_sat_solver_output(reader).unwrap();
+        let res = parse_sat_solver_output(&mut io::Cursor::new(data)).unwrap();
         assert_eq!(res, SolverOutput::Unsat);
     }
 
     #[test]
     fn parse_solver_output_unknown() {
         let data = "c this is a comment\ns UNKNOWN\n";
-        let reader = io::Cursor::new(data);
-        let res = parse_sat_solver_output(reader).unwrap();
+        let res = parse_sat_solver_output(&mut io::Cursor::new(data)).unwrap();
         assert_eq!(res, SolverOutput::Unknown);
     }
 
     #[test]
     fn parse_solver_output_indeterminate() {
         let data = "c this is a comment\ns INDETERMINATE\n";
-        let reader = io::Cursor::new(data);
-        let res = parse_sat_solver_output(reader).unwrap();
+        let res = parse_sat_solver_output(&mut io::Cursor::new(data)).unwrap();
         assert_eq!(res, SolverOutput::Unknown);
     }
 
     #[test]
     fn parse_solver_output_noslinewithvline() {
         let data = "c this is a comment\nv 1 -2 4 -5 6 0\n";
-        let reader = io::Cursor::new(data);
-        let res = parse_sat_solver_output(reader);
+        let res = parse_sat_solver_output(&mut io::Cursor::new(data));
         assert!(matches!(
             res.unwrap_err().downcast::<SatSolverOutputError>(),
             Ok(SatSolverOutputError::NoSLine)
@@ -237,8 +251,7 @@ mod tests {
     #[test]
     fn parse_solver_output_novlinewithsatisfy() {
         let data = "c this is a comment\ns SATISFIABLE\n";
-        let reader = io::Cursor::new(data);
-        let res = parse_sat_solver_output(reader);
+        let res = parse_sat_solver_output(&mut io::Cursor::new(data));
         assert!(matches!(
             res.unwrap_err().downcast::<SatSolverOutputError>(),
             Ok(SatSolverOutputError::NoVLine)
@@ -248,8 +261,7 @@ mod tests {
     #[test]
     fn parse_solver_output_emptysolution() {
         let data = "c this is a comment\ns SATISFIABLE\nv 0\n";
-        let reader = io::Cursor::new(data);
-        let res = parse_sat_solver_output(reader).unwrap();
+        let res = parse_sat_solver_output(&mut io::Cursor::new(data)).unwrap();
         assert_eq!(res, SolverOutput::Sat(Assignment::default()));
     }
 
@@ -259,33 +271,33 @@ mod tests {
         let instance: SatInstance =
             SatInstance::from_dimacs_path(format!("{manifest}/data/AProVE11-12.cnf")).unwrap();
 
-        let reader = super::open_compressed_uncompressed_read(format!(
+        let mut reader = super::open_compressed_uncompressed_read(format!(
             "{manifest}/data/gimsatul-AProVE11-12.log"
         ))
         .unwrap();
-        let res = parse_sat_solver_output(reader).unwrap();
+        let res = parse_sat_solver_output(&mut reader).unwrap();
         if let SolverOutput::Sat(sol) = res {
             assert!(instance.is_sat(&sol));
         } else {
             panic!()
         }
 
-        let reader = super::open_compressed_uncompressed_read(format!(
+        let mut reader = super::open_compressed_uncompressed_read(format!(
             "{manifest}/data/kissat-AProVE11-12.log"
         ))
         .unwrap();
-        let res = parse_sat_solver_output(reader).unwrap();
+        let res = parse_sat_solver_output(&mut reader).unwrap();
         if let SolverOutput::Sat(sol) = res {
             assert!(instance.is_sat(&sol));
         } else {
             panic!()
         }
 
-        let reader = super::open_compressed_uncompressed_read(format!(
+        let mut reader = super::open_compressed_uncompressed_read(format!(
             "{manifest}/data/cadical-AProVE11-12.log"
         ))
         .unwrap();
-        let res = parse_sat_solver_output(reader).unwrap();
+        let res = parse_sat_solver_output(&mut reader).unwrap();
         if let SolverOutput::Sat(sol) = res {
             assert!(instance.is_sat(&sol));
         } else {
@@ -296,28 +308,28 @@ mod tests {
     #[test]
     fn parse_solver_output_unsat_logs() {
         let manifest = std::env::var("CARGO_MANIFEST_DIR").unwrap();
-        let reader = super::open_compressed_uncompressed_read(format!(
+        let mut reader = super::open_compressed_uncompressed_read(format!(
             "{manifest}/data/gimsatul-smtlib-qfbv-aigs-ext_con_032_008_0256-tseitin.log"
         ))
         .unwrap();
         assert_eq!(
-            parse_sat_solver_output(reader).unwrap(),
+            parse_sat_solver_output(&mut reader).unwrap(),
             SolverOutput::Unsat
         );
-        let reader = super::open_compressed_uncompressed_read(format!(
+        let mut reader = super::open_compressed_uncompressed_read(format!(
             "{manifest}/data/kissat-smtlib-qfbv-aigs-ext_con_032_008_0256-tseitin.log"
         ))
         .unwrap();
         assert_eq!(
-            parse_sat_solver_output(reader,).unwrap(),
+            parse_sat_solver_output(&mut reader).unwrap(),
             SolverOutput::Unsat
         );
-        let reader = super::open_compressed_uncompressed_read(format!(
+        let mut reader = super::open_compressed_uncompressed_read(format!(
             "{manifest}/data/cadical-smtlib-qfbv-aigs-ext_con_032_008_0256-tseitin.log"
         ))
         .unwrap();
         assert_eq!(
-            parse_sat_solver_output(reader,).unwrap(),
+            parse_sat_solver_output(&mut reader).unwrap(),
             SolverOutput::Unsat
         );
     }
diff --git a/src/instances/fio/dimacs.rs b/src/instances/fio/dimacs.rs
index d3c6e994..9b670ef3 100644
--- a/src/instances/fio/dimacs.rs
+++ b/src/instances/fio/dimacs.rs
@@ -55,7 +55,7 @@ pub struct InvalidPLine(String);
 /// # Errors
 ///
 /// Parsing errors or [`io::Error`].
-pub fn parse_cnf<R, VM>(reader: R) -> anyhow::Result<SatInstance<VM>>
+pub fn parse_cnf<R, VM>(reader: &mut R) -> anyhow::Result<SatInstance<VM>>
 where
     R: BufRead,
     VM: ManageVars + Default,
@@ -78,7 +78,7 @@ where
 /// # Errors
 ///
 /// Parsing errors or [`io::Error`].
-pub fn parse_wcnf_with_idx<R, VM>(reader: R, obj_idx: usize) -> anyhow::Result<OptInstance<VM>>
+pub fn parse_wcnf_with_idx<R, VM>(reader: &mut R, obj_idx: usize) -> anyhow::Result<OptInstance<VM>>
 where
     R: BufRead,
     VM: ManageVars + Default,
@@ -103,7 +103,7 @@ where
 /// # Errors
 ///
 /// Parsing errors or [`io::Error`].
-pub fn parse_mcnf<R, VM>(reader: R) -> anyhow::Result<MultiOptInstance<VM>>
+pub fn parse_mcnf<R, VM>(reader: &mut R) -> anyhow::Result<MultiOptInstance<VM>>
 where
     R: BufRead,
     VM: ManageVars + Default,
@@ -136,12 +136,12 @@ enum Preamble {
 /// # Errors
 ///
 /// Parsing errors or [`io::Error`].
-fn parse_dimacs<R, VM>(reader: R) -> anyhow::Result<BodyContent<VM>>
+fn parse_dimacs<R, VM>(reader: &mut R) -> anyhow::Result<BodyContent<VM>>
 where
     R: BufRead,
     VM: ManageVars + Default,
 {
-    let (reader, preamble) = parse_preamble(reader)?;
+    let preamble = parse_preamble(reader)?;
     let content = match preamble {
         Preamble::Cnf {
             n_vars: _,    // Intentionally ignored (lean acceptance)
@@ -164,7 +164,7 @@ where
 /// # Errors
 ///
 /// Parsing errors or [`io::Error`].
-fn parse_preamble<R: BufRead>(mut reader: R) -> anyhow::Result<(R, Preamble)> {
+fn parse_preamble<R: BufRead>(reader: &mut R) -> anyhow::Result<Preamble> {
     let mut buf = String::new();
     while reader.read_line(&mut buf)? > 0 {
         if buf.starts_with('c') || buf.trim().is_empty() {
@@ -175,13 +175,13 @@ fn parse_preamble<R: BufRead>(mut reader: R) -> anyhow::Result<(R, Preamble)> {
             let Ok((_, preamble)) = parse_p_line(&buf) else {
                 return Err(InvalidPLine(buf).into());
             };
-            return Ok((reader, preamble));
+            return Ok(preamble);
         }
         break;
     }
     #[cfg(feature = "optimization")]
     {
-        Ok((reader, Preamble::NoPLine { first_line: buf }))
+        Ok(Preamble::NoPLine { first_line: buf })
     }
     #[cfg(not(feature = "optimization"))]
     {
@@ -194,7 +194,7 @@ fn parse_preamble<R: BufRead>(mut reader: R) -> anyhow::Result<(R, Preamble)> {
 /// # Errors
 ///
 /// Parsing errors or [`io::Error`].
-fn parse_cnf_body<R, VM>(mut reader: R) -> anyhow::Result<BodyContent<VM>>
+fn parse_cnf_body<R, VM>(reader: &mut R) -> anyhow::Result<BodyContent<VM>>
 where
     R: BufRead,
     VM: ManageVars + Default,
@@ -226,7 +226,7 @@ where
 /// # Errors
 ///
 /// Parsing errors or [`io::Error`].
-fn parse_wcnf_pre22_body<R, VM>(mut reader: R, top: usize) -> anyhow::Result<BodyContent<VM>>
+fn parse_wcnf_pre22_body<R, VM>(reader: &mut R, top: usize) -> anyhow::Result<BodyContent<VM>>
 where
     R: BufRead,
     VM: ManageVars + Default,
@@ -259,7 +259,7 @@ where
 /// # Errors
 ///
 /// Parsing errors or [`io::Error`].
-fn parse_no_pline_body<R, VM>(mut reader: R, first_line: &str) -> anyhow::Result<BodyContent<VM>>
+fn parse_no_pline_body<R, VM>(reader: &mut R, first_line: &str) -> anyhow::Result<BodyContent<VM>>
 where
     R: BufRead,
     VM: ManageVars + Default,
@@ -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()
 }
@@ -939,12 +939,9 @@ mod tests {
     #[test]
     fn parse_cnf_preamble() {
         let data = "c test\np cnf 5 2\n1 2 0";
-        let reader = Cursor::new(data);
-
-        let (_, preamble) = parse_preamble(reader).unwrap();
 
         assert_eq!(
-            preamble,
+            parse_preamble(&mut Cursor::new(data)).unwrap(),
             Preamble::Cnf {
                 n_vars: 5,
                 n_clauses: 2,
@@ -956,12 +953,9 @@ mod tests {
     #[test]
     fn parse_wcnf_pre22_preamble() {
         let data = "c test\np wcnf 5 2 10\n1 2 0";
-        let reader = Cursor::new(data);
-
-        let (_, preamble) = parse_preamble(reader).unwrap();
 
         assert_eq!(
-            preamble,
+            parse_preamble(&mut Cursor::new(data)).unwrap(),
             Preamble::WcnfPre22 {
                 n_vars: 5,
                 n_clauses: 2,
@@ -974,12 +968,9 @@ mod tests {
     #[test]
     fn parse_wcnf_post22_preamble() {
         let data = "c test\nh 5 2 0\n1 2 0";
-        let reader = Cursor::new(data);
-
-        let (_, preamble) = parse_preamble(reader).unwrap();
 
         assert_eq!(
-            preamble,
+            parse_preamble(&mut Cursor::new(data)).unwrap(),
             Preamble::NoPLine {
                 first_line: String::from("h 5 2 0\n"),
             }
@@ -990,12 +981,9 @@ mod tests {
     #[test]
     fn parse_mcnf_preamble() {
         let data = "c test\no1 2 0\nh 5 2 0";
-        let reader = Cursor::new(data);
-
-        let (_, preamble) = parse_preamble(reader).unwrap();
 
         assert_eq!(
-            preamble,
+            parse_preamble(&mut Cursor::new(data)).unwrap(),
             Preamble::NoPLine {
                 first_line: String::from("o1 2 0\n")
             }
@@ -1005,9 +993,8 @@ mod tests {
     #[test]
     fn parse_cnf_body_pass() {
         let data = "1 2 0\n-3 4 5 0\n";
-        let reader = Cursor::new(data);
 
-        let parsed_inst = parse_cnf_body(reader).unwrap();
+        let parsed_inst = parse_cnf_body(&mut Cursor::new(data)).unwrap();
 
         let mut true_inst: SatInstance = SatInstance::new();
         true_inst.add_clause(clause![ipasir_lit![1], ipasir_lit![2]]);
@@ -1023,9 +1010,8 @@ mod tests {
     #[test]
     fn parse_wcnf_pre22_body_pass() {
         let data = "42 1 2 0\n10 -3 4 5 0\n";
-        let reader = Cursor::new(data);
 
-        let parsed_inst = parse_wcnf_pre22_body(reader, 42).unwrap();
+        let parsed_inst = parse_wcnf_pre22_body(&mut Cursor::new(data), 42).unwrap();
 
         let mut true_constrs: SatInstance = SatInstance::new();
         let mut true_obj = Objective::new();
@@ -1039,9 +1025,8 @@ mod tests {
     #[test]
     fn parse_wcnf_post22_body_pass() {
         let data = "h 1 2 0\n10 -3 4 5 0\n";
-        let reader = Cursor::new(data);
 
-        let parsed_inst = parse_no_pline_body(reader, "c test").unwrap();
+        let parsed_inst = parse_no_pline_body(&mut Cursor::new(data), "c test").unwrap();
 
         let mut true_constrs: SatInstance = SatInstance::new();
         let mut true_obj = Objective::new();
@@ -1055,9 +1040,8 @@ mod tests {
     #[test]
     fn parse_mcnf_body_pass() {
         let data = "h 1 2 0\no2 10 -3 4 5 0\n";
-        let reader = Cursor::new(data);
 
-        let parsed_inst = parse_no_pline_body(reader, "c test\n").unwrap();
+        let parsed_inst = parse_no_pline_body(&mut Cursor::new(data), "c test\n").unwrap();
 
         let mut true_constrs: SatInstance = SatInstance::new();
         let mut true_obj = Objective::new();
@@ -1073,9 +1057,8 @@ mod tests {
     #[test]
     fn parse_cnf() {
         let data = "p cnf 5 2\n1 2 0\n-3 4 5 0\n";
-        let reader = Cursor::new(data);
 
-        let parsed_inst = parse_dimacs(reader).unwrap();
+        let parsed_inst = parse_dimacs(&mut Cursor::new(data)).unwrap();
 
         let mut true_inst: SatInstance = SatInstance::new();
         true_inst.add_clause(clause![ipasir_lit![1], ipasir_lit![2]]);
@@ -1091,9 +1074,8 @@ mod tests {
     #[test]
     fn parse_wcnf_pre22() {
         let data = "p wcnf 5 2 42\n42 1 2 0\n10 -3 4 5 0\n";
-        let reader = Cursor::new(data);
 
-        let parsed_inst = parse_dimacs(reader).unwrap();
+        let parsed_inst = parse_dimacs(&mut Cursor::new(data)).unwrap();
 
         let mut true_constrs: SatInstance = SatInstance::new();
         let mut true_obj = Objective::new();
@@ -1107,9 +1089,8 @@ mod tests {
     #[test]
     fn parse_wcnf_post22() {
         let data = "h 1 2 0\n10 -3 4 5 0\n";
-        let reader = Cursor::new(data);
 
-        let parsed_inst = parse_dimacs(reader).unwrap();
+        let parsed_inst = parse_dimacs(&mut Cursor::new(data)).unwrap();
 
         let mut true_constrs: SatInstance = SatInstance::new();
         let mut true_obj = Objective::new();
@@ -1123,9 +1104,8 @@ mod tests {
     #[test]
     fn parse_mcnf() {
         let data = "c test\nh 1 2 0\no2 10 -3 4 5 0\no1 3 -1 0\n";
-        let reader = Cursor::new(data);
 
-        let parsed_inst = parse_dimacs(reader).unwrap();
+        let parsed_inst = parse_dimacs(&mut Cursor::new(data)).unwrap();
 
         let mut true_constrs: SatInstance = SatInstance::new();
         let mut true_obj0 = Objective::new();
@@ -1149,7 +1129,7 @@ mod tests {
 
         cursor.rewind().unwrap();
 
-        let parsed_inst: SatInstance = super::parse_cnf(cursor).unwrap();
+        let parsed_inst: SatInstance = super::parse_cnf(&mut cursor).unwrap();
         let (parsed_cnf, _) = parsed_inst.into_cnf();
 
         assert_eq!(parsed_cnf, true_cnf);
@@ -1176,7 +1156,7 @@ mod tests {
 
         cursor.rewind().unwrap();
 
-        let parsed_inst = super::parse_wcnf_with_idx(cursor, 0).unwrap();
+        let parsed_inst = super::parse_wcnf_with_idx(&mut cursor, 0).unwrap();
 
         assert_eq!(parsed_inst, OptInstance::compose(true_constrs, true_obj));
     }
@@ -1209,7 +1189,7 @@ mod tests {
 
         cursor.rewind().unwrap();
 
-        let parsed_inst = super::parse_mcnf(cursor).unwrap();
+        let parsed_inst = super::parse_mcnf(&mut cursor).unwrap();
 
         assert_eq!(
             parsed_inst,
diff --git a/src/instances/fio/opb.rs b/src/instances/fio/opb.rs
index f5db39e5..8a57d001 100644
--- a/src/instances/fio/opb.rs
+++ b/src/instances/fio/opb.rs
@@ -94,7 +94,7 @@ enum OpbData {
 /// # Errors
 ///
 /// Parsing errors or [`io::Error`].
-pub fn parse_sat<R, VM>(reader: R, opts: Options) -> anyhow::Result<SatInstance<VM>>
+pub fn parse_sat<R, VM>(reader: &mut R, opts: Options) -> anyhow::Result<SatInstance<VM>>
 where
     R: BufRead,
     VM: ManageVars + Default,
@@ -117,7 +117,7 @@ where
 ///
 /// Parsing errors or [`io::Error`].
 pub fn parse_opt_with_idx<R, VM>(
-    reader: R,
+    reader: &mut R,
     obj_idx: usize,
     opts: Options,
 ) -> anyhow::Result<OptInstance<VM>>
@@ -159,7 +159,7 @@ where
 /// # Errors
 ///
 /// Parsing errors or [`io::Error`].
-pub fn parse_multi_opt<R, VM>(reader: R, opts: Options) -> anyhow::Result<MultiOptInstance<VM>>
+pub fn parse_multi_opt<R, VM>(reader: &mut R, opts: Options) -> anyhow::Result<MultiOptInstance<VM>>
 where
     R: BufRead,
     VM: ManageVars + Default,
@@ -176,7 +176,7 @@ where
 }
 
 /// Parses all OPB data of a reader
-fn parse_opb_data<R: BufRead>(mut reader: R, opts: Options) -> anyhow::Result<Vec<OpbData>> {
+fn parse_opb_data<R: BufRead>(reader: &mut R, opts: Options) -> anyhow::Result<Vec<OpbData>> {
     let mut buf = String::new();
     let mut data = vec![];
     // TODO: consider not necessarily reading a full line
@@ -984,8 +984,7 @@ mod test {
     fn multi_opb_data() {
         let data = "* test\n5 x1 -3 x2 >= 4;\nmin: 1 x1;";
         let reader = Cursor::new(data);
-        let reader = BufReader::new(reader);
-        if let Ok(data) = parse_opb_data(reader, Options::default()) {
+        if let Ok(data) = parse_opb_data(&mut BufReader::new(reader), Options::default()) {
             assert_eq!(data.len(), 3);
             assert_eq!(data[0], OpbData::Cmt(String::from("* test\n")));
             assert!(matches!(data[1], OpbData::Constr(_)));
@@ -995,8 +994,7 @@ mod test {
         }
         let data = "* test\n5 x1 -3 x2 >= 4;\nmin: x1;";
         let reader = Cursor::new(data);
-        let reader = BufReader::new(reader);
-        assert!(parse_opb_data(reader, Options::default()).is_err());
+        assert!(parse_opb_data(&mut BufReader::new(reader), Options::default()).is_err());
     }
 
     #[test]
@@ -1009,7 +1007,7 @@ mod test {
 
         cursor.rewind().unwrap();
 
-        let (cnf, _) = super::parse_sat::<_, BasicVarManager>(cursor, Options::default())
+        let (cnf, _) = super::parse_sat::<_, BasicVarManager>(&mut cursor, Options::default())
             .unwrap()
             .into_cnf();
 
@@ -1024,7 +1022,7 @@ mod test {
 
         cursor.rewind().unwrap();
 
-        let parsed_inst: SatInstance = super::parse_sat(cursor, opts).unwrap();
+        let parsed_inst: SatInstance = super::parse_sat(&mut cursor, opts).unwrap();
 
         let (parsed_cnf, parsed_vm) = parsed_inst.into_cnf();
         let (true_cnf, true_vm) = true_inst.into_cnf();
diff --git a/src/instances/multiopt.rs b/src/instances/multiopt.rs
index 7673db92..7e926f16 100644
--- a/src/instances/multiopt.rs
+++ b/src/instances/multiopt.rs
@@ -502,7 +502,7 @@ impl<VM: ManageVars + Default> MultiOptInstance<VM> {
     /// # Errors
     ///
     /// Parsing errors from [`nom`] or [`io::Error`].
-    pub fn from_dimacs<R: io::BufRead>(reader: R) -> anyhow::Result<Self> {
+    pub fn from_dimacs<R: io::BufRead>(reader: &mut R) -> anyhow::Result<Self> {
         fio::dimacs::parse_mcnf(reader)
     }
 
@@ -513,8 +513,8 @@ impl<VM: ManageVars + Default> MultiOptInstance<VM> {
     ///
     /// Parsing errors from [`nom`] or [`io::Error`].
     pub fn from_dimacs_path<P: AsRef<Path>>(path: P) -> anyhow::Result<Self> {
-        let reader = fio::open_compressed_uncompressed_read(path)?;
-        Self::from_dimacs(reader)
+        let mut reader = fio::open_compressed_uncompressed_read(path)?;
+        Self::from_dimacs(&mut reader)
     }
 
     /// Parses an OPB instance from a reader object.
@@ -529,7 +529,10 @@ impl<VM: ManageVars + Default> MultiOptInstance<VM> {
     /// # Errors
     ///
     /// Parsing errors from [`nom`] or [`io::Error`].
-    pub fn from_opb<R: io::BufRead>(reader: R, opts: fio::opb::Options) -> anyhow::Result<Self> {
+    pub fn from_opb<R: io::BufRead>(
+        reader: &mut R,
+        opts: fio::opb::Options,
+    ) -> anyhow::Result<Self> {
         fio::opb::parse_multi_opt(reader, opts)
     }
 
@@ -541,8 +544,8 @@ impl<VM: ManageVars + Default> MultiOptInstance<VM> {
     ///
     /// Parsing errors from [`nom`] or [`io::Error`].
     pub fn from_opb_path<P: AsRef<Path>>(path: P, opts: fio::opb::Options) -> anyhow::Result<Self> {
-        let reader = fio::open_compressed_uncompressed_read(path)?;
-        Self::from_opb(reader, opts)
+        let mut reader = fio::open_compressed_uncompressed_read(path)?;
+        Self::from_opb(&mut reader, opts)
     }
 }
 
diff --git a/src/instances/opt.rs b/src/instances/opt.rs
index 381a459d..dd3a40e7 100644
--- a/src/instances/opt.rs
+++ b/src/instances/opt.rs
@@ -1427,7 +1427,7 @@ impl<VM: ManageVars + Default> Instance<VM> {
     /// # Errors
     ///
     /// Parsing errors from [`nom`] or [`io::Error`].
-    pub fn from_dimacs<R: io::BufRead>(reader: R) -> anyhow::Result<Self> {
+    pub fn from_dimacs<R: io::BufRead>(reader: &mut R) -> anyhow::Result<Self> {
         Self::from_dimacs_with_idx(reader, 0)
     }
 
@@ -1438,7 +1438,10 @@ impl<VM: ManageVars + Default> Instance<VM> {
     /// # Errors
     ///
     /// Parsing errors from [`nom`] or [`io::Error`].
-    pub fn from_dimacs_with_idx<R: io::BufRead>(reader: R, obj_idx: usize) -> anyhow::Result<Self> {
+    pub fn from_dimacs_with_idx<R: io::BufRead>(
+        reader: &mut R,
+        obj_idx: usize,
+    ) -> anyhow::Result<Self> {
         fio::dimacs::parse_wcnf_with_idx(reader, obj_idx)
     }
 
@@ -1450,8 +1453,8 @@ impl<VM: ManageVars + Default> Instance<VM> {
     ///
     /// Parsing errors from [`nom`] or [`io::Error`].
     pub fn from_dimacs_path<P: AsRef<Path>>(path: P) -> anyhow::Result<Self> {
-        let reader = fio::open_compressed_uncompressed_read(path)?;
-        Self::from_dimacs(reader)
+        let mut reader = fio::open_compressed_uncompressed_read(path)?;
+        Self::from_dimacs(&mut reader)
     }
 
     /// Parses a DIMACS instance from a file path. For more details see
@@ -1465,8 +1468,8 @@ impl<VM: ManageVars + Default> Instance<VM> {
         path: P,
         obj_idx: usize,
     ) -> anyhow::Result<Self> {
-        let reader = fio::open_compressed_uncompressed_read(path)?;
-        Self::from_dimacs_with_idx(reader, obj_idx)
+        let mut reader = fio::open_compressed_uncompressed_read(path)?;
+        Self::from_dimacs_with_idx(&mut reader, obj_idx)
     }
 
     /// Parses an OPB instance from a reader object.
@@ -1480,7 +1483,10 @@ impl<VM: ManageVars + Default> Instance<VM> {
     /// # Errors
     ///
     /// Parsing errors from [`nom`] or [`io::Error`].
-    pub fn from_opb<R: io::BufRead>(reader: R, opts: fio::opb::Options) -> anyhow::Result<Self> {
+    pub fn from_opb<R: io::BufRead>(
+        reader: &mut R,
+        opts: fio::opb::Options,
+    ) -> anyhow::Result<Self> {
         Self::from_opb_with_idx(reader, 0, opts)
     }
 
@@ -1492,7 +1498,7 @@ impl<VM: ManageVars + Default> Instance<VM> {
     ///
     /// Parsing errors from [`nom`] or [`io::Error`].
     pub fn from_opb_with_idx<R: io::BufRead>(
-        reader: R,
+        reader: &mut R,
         obj_idx: usize,
         opts: fio::opb::Options,
     ) -> anyhow::Result<Self> {
@@ -1507,8 +1513,8 @@ impl<VM: ManageVars + Default> Instance<VM> {
     ///
     /// Parsing errors from [`nom`] or [`io::Error`].
     pub fn from_opb_path<P: AsRef<Path>>(path: P, opts: fio::opb::Options) -> anyhow::Result<Self> {
-        let reader = fio::open_compressed_uncompressed_read(path)?;
-        Self::from_opb(reader, opts)
+        let mut reader = fio::open_compressed_uncompressed_read(path)?;
+        Self::from_opb(&mut reader, opts)
     }
 
     /// Parses an OPB instance from a file path, selecting the objective with
@@ -1525,8 +1531,8 @@ impl<VM: ManageVars + Default> Instance<VM> {
         obj_idx: usize,
         opts: fio::opb::Options,
     ) -> anyhow::Result<Self> {
-        let reader = fio::open_compressed_uncompressed_read(path)?;
-        Self::from_opb_with_idx(reader, obj_idx, opts)
+        let mut reader = fio::open_compressed_uncompressed_read(path)?;
+        Self::from_opb_with_idx(&mut reader, obj_idx, opts)
     }
 }
 
diff --git a/src/instances/sat.rs b/src/instances/sat.rs
index a2fa7b37..ef63d147 100644
--- a/src/instances/sat.rs
+++ b/src/instances/sat.rs
@@ -996,7 +996,7 @@ impl<VM: ManageVars + Default> Instance<VM> {
     /// # Errors
     ///
     /// Parsing errors from [`nom`] or [`io::Error`].
-    pub fn from_dimacs<R: io::BufRead>(reader: R) -> anyhow::Result<Self> {
+    pub fn from_dimacs<R: io::BufRead>(reader: &mut R) -> anyhow::Result<Self> {
         fio::dimacs::parse_cnf(reader)
     }
 
@@ -1008,9 +1008,9 @@ impl<VM: ManageVars + Default> Instance<VM> {
     ///
     /// Parsing errors from [`nom`] or [`io::Error`].
     pub fn from_dimacs_path<P: AsRef<Path>>(path: P) -> anyhow::Result<Self> {
-        let reader =
+        let mut reader =
             fio::open_compressed_uncompressed_read(path).context("failed to open reader")?;
-        Instance::from_dimacs(reader)
+        Instance::from_dimacs(&mut reader)
     }
 
     /// Parses an OPB instance from a reader object.
@@ -1024,7 +1024,10 @@ impl<VM: ManageVars + Default> Instance<VM> {
     /// # Errors
     ///
     /// Parsing errors from [`nom`] or [`io::Error`].
-    pub fn from_opb<R: io::BufRead>(reader: R, opts: fio::opb::Options) -> anyhow::Result<Self> {
+    pub fn from_opb<R: io::BufRead>(
+        reader: &mut R,
+        opts: fio::opb::Options,
+    ) -> anyhow::Result<Self> {
         fio::opb::parse_sat(reader, opts)
     }
 
@@ -1036,9 +1039,9 @@ impl<VM: ManageVars + Default> Instance<VM> {
     ///
     /// Parsing errors from [`nom`] or [`io::Error`].
     pub fn from_opb_path<P: AsRef<Path>>(path: P, opts: fio::opb::Options) -> anyhow::Result<Self> {
-        let reader =
+        let mut reader =
             fio::open_compressed_uncompressed_read(path).context("failed to open reader")?;
-        Instance::from_opb(reader, opts)
+        Instance::from_opb(&mut reader, opts)
     }
 }
 
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 `<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"),
         }
     }
 }
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<P: AsRef<Path>>(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<P: AsRef<Path>>(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 `<stdin>`
+    #[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<P: AsRef<Path>>(path: P) -> Self {
+        OutputVia(OutputViaInt::File(path.as_ref().to_path_buf()))
+    }
+
+    /// Process the solver output via a pipe from `<stdout>`
+    #[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("<path to solver binary>"),
+    ///     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("<path to solver binary>"),
+    ///     "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<super::SolverResult> {
+        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<crate::types::TernaryVal> {
+        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<Assignment> {
+        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<Clause> for Solver {
+    fn extend<T: IntoIterator<Item = Clause>>(&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<T: IntoIterator<Item = &'a Clause>>(&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<SolverOutput> {
+    // 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<process::ChildStdout>)> {
+                            // 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/src/types.rs b/src/types.rs
index 88c2fb1d..384be416 100644
--- a/src/types.rs
+++ b/src/types.rs
@@ -767,10 +767,10 @@ impl Assignment {
     /// - Invalid solver output: [`fio::SatSolverOutputError`]
     /// - Invalid v line: [`InvalidVLine`]
     pub fn from_solver_output_path<P: AsRef<Path>>(path: P) -> anyhow::Result<Self> {
-        let reader = std::io::BufReader::new(
+        let mut reader = std::io::BufReader::new(
             fio::open_compressed_uncompressed_read(path).context("failed to open reader")?,
         );
-        let output = fio::parse_sat_solver_output(reader)?;
+        let output = fio::parse_sat_solver_output(&mut reader)?;
         match output {
             SolverOutput::Sat(solution) => Ok(solution),
             _ => anyhow::bail!("solver output does not indicate satisfiability"),
diff --git a/tools/src/bin/cnf2opb.rs b/tools/src/bin/cnf2opb.rs
index 6242c3f9..89a95fff 100644
--- a/tools/src/bin/cnf2opb.rs
+++ b/tools/src/bin/cnf2opb.rs
@@ -32,7 +32,8 @@ fn main() -> anyhow::Result<()> {
     let inst: SatInstance = if let Some(in_path) = args.in_path {
         SatInstance::from_dimacs_path(in_path).context("error parsing the input file")?
     } else {
-        SatInstance::from_dimacs(io::BufReader::new(io::stdin())).context("error parsing input")?
+        SatInstance::from_dimacs(&mut io::BufReader::new(io::stdin()))
+            .context("error parsing input")?
     };
 
     if let Some(out_path) = args.out_path {
diff --git a/tools/src/bin/mcnf2opb.rs b/tools/src/bin/mcnf2opb.rs
index 345d06b4..c124a84e 100644
--- a/tools/src/bin/mcnf2opb.rs
+++ b/tools/src/bin/mcnf2opb.rs
@@ -32,7 +32,7 @@ fn main() -> anyhow::Result<()> {
     let inst: MultiOptInstance = if let Some(in_path) = args.in_path {
         MultiOptInstance::from_dimacs_path(in_path).context("error parsing the input file")?
     } else {
-        MultiOptInstance::from_dimacs(io::BufReader::new(io::stdin()))
+        MultiOptInstance::from_dimacs(&mut io::BufReader::new(io::stdin()))
             .context("error parsing input")?
     };
 
diff --git a/tools/src/bin/opb2cnf.rs b/tools/src/bin/opb2cnf.rs
index 0d8244f3..4b91c300 100644
--- a/tools/src/bin/opb2cnf.rs
+++ b/tools/src/bin/opb2cnf.rs
@@ -29,7 +29,7 @@ fn main() -> anyhow::Result<()> {
     let mut inst: SatInstance = if let Some(in_path) = args.in_path {
         SatInstance::from_opb_path(in_path, opb_opts).context("error parsing the input file")?
     } else {
-        SatInstance::from_opb(io::BufReader::new(io::stdin()), opb_opts)
+        SatInstance::from_opb(&mut io::BufReader::new(io::stdin()), opb_opts)
             .context("error parsing input")?
     };
 
diff --git a/tools/src/bin/opb2mcnf.rs b/tools/src/bin/opb2mcnf.rs
index 0bb9c873..e33e95df 100644
--- a/tools/src/bin/opb2mcnf.rs
+++ b/tools/src/bin/opb2mcnf.rs
@@ -30,7 +30,7 @@ fn main() -> anyhow::Result<()> {
         MultiOptInstance::from_opb_path(in_path, opb_opts)
             .context("error parsing the input file")?
     } else {
-        MultiOptInstance::from_opb(io::BufReader::new(io::stdin()), opb_opts)
+        MultiOptInstance::from_opb(&mut io::BufReader::new(io::stdin()), opb_opts)
             .context("error parsing input")?
     };
 
diff --git a/tools/src/bin/opb2wcnf.rs b/tools/src/bin/opb2wcnf.rs
index f2fdf3a0..e767e204 100644
--- a/tools/src/bin/opb2wcnf.rs
+++ b/tools/src/bin/opb2wcnf.rs
@@ -29,7 +29,7 @@ fn main() -> anyhow::Result<()> {
     let inst: OptInstance = if let Some(in_path) = args.in_path {
         OptInstance::from_opb_path(in_path, opb_opts).context("error parsing the input file")?
     } else {
-        OptInstance::from_opb(io::BufReader::new(io::stdin()), opb_opts)
+        OptInstance::from_opb(&mut io::BufReader::new(io::stdin()), opb_opts)
             .context("error parsing input")?
     };
 
diff --git a/tools/src/bin/wcnf2opb.rs b/tools/src/bin/wcnf2opb.rs
index 6be8aea7..a679586d 100644
--- a/tools/src/bin/wcnf2opb.rs
+++ b/tools/src/bin/wcnf2opb.rs
@@ -32,7 +32,8 @@ fn main() -> anyhow::Result<()> {
     let inst: OptInstance = if let Some(in_path) = args.in_path {
         OptInstance::from_dimacs_path(in_path).context("error parsing the input file")?
     } else {
-        OptInstance::from_dimacs(io::BufReader::new(io::stdin())).context("error parsing input")?
+        OptInstance::from_dimacs(&mut io::BufReader::new(io::stdin()))
+            .context("error parsing input")?
     };
 
     let (mut constr, mut obj) = inst.decompose();


Test patch:
diff --git a/solvertests/src/integration.rs b/solvertests/src/integration.rs
index ff8e81c2..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::<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,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();
@@ -206,7 +207,7 @@ pub fn phasing(input: MacroInput) -> TokenStream {
     ts.extend(quote! {
         #[test]
         #ignore
-        fn assumption_sequence() {
+        fn user_phases() {
             use rustsat::{
                 instances::{SatInstance},
                 lit,
@@ -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<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()?)
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
+    );
+}