Improve API ergonomics

cadical/src/lib.rs

@@ -351,6 +351,15 @@ impl Extend<Clause> for CaDiCaL<'_, '_> {
     }
 }
 
+impl<'a> Extend<&'a Clause> for CaDiCaL<'_, '_> {
+    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")
+        })
+    }
+}
+
 impl Solve for CaDiCaL<'_, '_> {
     fn signature(&self) -> &'static str {
         let c_chars = unsafe { ffi::ccadical_signature() };
@@ -427,7 +436,7 @@ impl Solve for CaDiCaL<'_, '_> {
         }
     }
 
-    fn add_clause(&mut self, clause: Clause) -> anyhow::Result<()> {
+    fn add_clause_ref(&mut self, clause: &Clause) -> anyhow::Result<()> {
         // Update wrapper-internal state
         self.stats.n_clauses += 1;
         self.stats.avg_clause_len =
@@ -436,7 +445,7 @@ impl Solve for CaDiCaL<'_, '_> {
         self.state = InternalSolverState::Input;
         // Call CaDiCaL backend
         clause
-            .into_iter()
+            .iter()
             .for_each(|l| unsafe { ffi::ccadical_add(self.handle, l.to_ipasir()) });
         unsafe { ffi::ccadical_add(self.handle, 0) };
         Ok(())

data/tiny-single-opt.opb

@@ -0,0 +1,6 @@
+* #variable= 4 #constraint= 3
+* A handwritten OPB sat instance for basic testing
+min: 1 x1 2 x2;
+5 x1 -3 x2 >= 4;
+5 x3 -3 x4 >= 2;
+5 ~x4 >= 4;

docs/0-5-0-migration-guide.md

@@ -0,0 +1,47 @@
+# Migration Guide for Breaking Changes in v0.5.0
+
+This document gives an overview of the breaking API changes in v0.5.0 and how
+to update your code accordingly. Mostly, follow the error messages the compiler
+will give you after updating to the new RustSAT version.
+
+## Error Handling
+
+Error handling in the `Solve` trait, and file parsers now uses the
+[`anyhow`](https://docs.rs/anyhow/latest/anyhow/) crate. This allows for better
+error messages, and better tracing. In the process, some of the error types or
+variants that are not needed any more have been removed:
+
+- `rustsat::solvers::SolverError` has been removed and only
+  `rustsat::solvers::StateError` remains
+- `rustsat::instances::fio::opb::Error` has been removed
+- `rustsat::instances::fio::dimacs::Error` has been removed
+- `rustsat::instances::fio::ParsingError` has been removed
+- `rustsat::solvers::SolverState::Error` has also been removed as no error
+  state is needed with proper error returns
+
+If you need to handle a specific error, you can use `anyhow`'s
+[`downcast`](https://docs.rs/anyhow/latest/anyhow/struct.Error.html#method.downcast)
+(e.g., on `solvers::StateError`), but I imagine most often these errors are
+anyhow just propagated outwards and displayed.
+
+## Changes to Improve API Ergonomics
+
+There have been some API changes to improve usability, even though they are breaking.
+
+- File writing methods: all file writing methods (on `SatInstance`,
+  `OptInstance` and `MultiOptInstance`) are now called `write_` instead of `to_`.
+  Furthermore they take references instead of values and will return an error if
+  a specific format of the instance is expected but the instance does not satisfy
+  this requirement.
+- File reading methods: all file reading methods (DIMACS and OPB, on
+  `SatInsatnce`, etc) now require a `BufRead` type as input. Previously, the
+  reader was internally wrapped in a
+  [`BufReader`](https://doc.rust-lang.org/stable/std/io/struct.BufReader.html)
+  object. This now has to be done externally to avoid potentially double
+  buffering.
+- "Heavy" conversion function (e.g., `SatInstance::to_cnf`) are now called
+  `into_`. Additionally, inplace converter functions named `convert_to_` are also
+  provided.
+- Methods providing references to internal data are now named `_ref` and `_mut`
+  if mutability is allowed. If only a non-mutable accessor is present, the `_ref`
+  suffix is omitted (e.g., for `SatInstance::cnf`).

glucose/src/core.rs

@@ -82,6 +82,15 @@ impl Extend<Clause> for Glucose {
     }
 }
 
+impl<'a> Extend<&'a Clause> for Glucose {
+    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")
+        })
+    }
+}
+
 impl Solve for Glucose {
     fn signature(&self) -> &'static str {
         let c_chars = unsafe { ffi::cglucose4_signature() };
@@ -150,15 +159,15 @@ impl Solve for Glucose {
         }
     }
 
-    fn add_clause(&mut self, clause: Clause) -> anyhow::Result<()> {
+    fn add_clause_ref(&mut self, clause: &Clause) -> anyhow::Result<()> {
         // Update wrapper-internal state
         self.stats.n_clauses += 1;
         self.stats.avg_clause_len =
             (self.stats.avg_clause_len * ((self.stats.n_clauses - 1) as f32) + clause.len() as f32)
                 / self.stats.n_clauses as f32;
         self.state = InternalSolverState::Input;
         // Call glucose backend
-        clause.into_iter().for_each(|l| unsafe {
+        clause.iter().for_each(|l| unsafe {
             ffi::cglucose4_add(self.handle, l.to_ipasir());
         });
         unsafe { ffi::cglucose4_add(self.handle, 0) };

glucose/src/simp.rs

@@ -90,6 +90,15 @@ impl Extend<Clause> for Glucose {
     }
 }
 
+impl<'a> Extend<&'a Clause> for Glucose {
+    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")
+        })
+    }
+}
+
 impl Solve for Glucose {
     fn signature(&self) -> &'static str {
         let c_chars = unsafe { ffi::cglucose4_signature() };
@@ -158,15 +167,15 @@ impl Solve for Glucose {
         }
     }
 
-    fn add_clause(&mut self, clause: Clause) -> anyhow::Result<()> {
+    fn add_clause_ref(&mut self, clause: &Clause) -> anyhow::Result<()> {
         // Update wrapper-internal state
         self.stats.n_clauses += 1;
         self.stats.avg_clause_len =
             (self.stats.avg_clause_len * ((self.stats.n_clauses - 1) as f32) + clause.len() as f32)
                 / self.stats.n_clauses as f32;
         self.state = InternalSolverState::Input;
         // Call glucose backend
-        clause.into_iter().for_each(|l| unsafe {
+        clause.iter().for_each(|l| unsafe {
             ffi::cglucosesimp4_add(self.handle, l.to_ipasir());
         });
         unsafe { ffi::cglucosesimp4_add(self.handle, 0) };

ipasir/src/lib.rs

@@ -186,7 +186,7 @@ impl Solve for IpasirSolver<'_, '_> {
         }
     }
 
-    fn add_clause(&mut self, clause: Clause) -> anyhow::Result<()> {
+    fn add_clause_ref(&mut self, clause: &Clause) -> anyhow::Result<()> {
         // Update wrapper-internal state
         self.stats.n_clauses += 1;
         clause.iter().for_each(|l| match self.stats.max_var {
@@ -202,7 +202,7 @@ impl Solve for IpasirSolver<'_, '_> {
                 / self.stats.n_clauses as f32;
         self.state = InternalSolverState::Input;
         // Call IPASIR backend
-        for lit in &clause {
+        for lit in clause {
             unsafe { ffi::ipasir_add(self.handle, lit.to_ipasir()) }
         }
         unsafe { ffi::ipasir_add(self.handle, 0) };
@@ -369,6 +369,15 @@ impl Extend<Clause> for IpasirSolver<'_, '_> {
     }
 }
 
+impl<'a> Extend<&'a Clause> for IpasirSolver<'_, '_> {
+    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")
+        })
+    }
+}
+
 /// cbindgen:ignore
 mod ffi {
     use super::{LearnCallbackPtr, TermCallbackPtr};

kissat/src/lib.rs

@@ -188,6 +188,15 @@ impl Extend<Clause> for Kissat<'_> {
     }
 }
 
+impl<'a> Extend<&'a Clause> for Kissat<'_> {
+    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")
+        })
+    }
+}
+
 impl Solve for Kissat<'_> {
     fn signature(&self) -> &'static str {
         let c_chars = unsafe { ffi::kissat_signature() };
@@ -260,7 +269,7 @@ impl Solve for Kissat<'_> {
         }
     }
 
-    fn add_clause(&mut self, clause: Clause) -> anyhow::Result<()> {
+    fn add_clause_ref(&mut self, clause: &Clause) -> anyhow::Result<()> {
         // Kissat is non-incremental, so only add if in input or configuring state
         if !matches!(
             self.state,
@@ -288,7 +297,7 @@ impl Solve for Kissat<'_> {
         self.state = InternalSolverState::Input;
         // Call Kissat backend
         clause
-            .into_iter()
+            .iter()
             .for_each(|l| unsafe { ffi::kissat_add(self.handle, l.to_ipasir()) });
         unsafe { ffi::kissat_add(self.handle, 0) };
         Ok(())

minisat/src/core.rs

@@ -82,6 +82,15 @@ impl Extend<Clause> for Minisat {
     }
 }
 
+impl<'a> Extend<&'a Clause> for Minisat {
+    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")
+        })
+    }
+}
+
 impl Solve for Minisat {
     fn signature(&self) -> &'static str {
         let c_chars = unsafe { ffi::cminisat_signature() };
@@ -150,15 +159,15 @@ impl Solve for Minisat {
         }
     }
 
-    fn add_clause(&mut self, clause: Clause) -> anyhow::Result<()> {
+    fn add_clause_ref(&mut self, clause: &Clause) -> anyhow::Result<()> {
         // Update wrapper-internal state
         self.stats.n_clauses += 1;
         self.stats.avg_clause_len =
             (self.stats.avg_clause_len * ((self.stats.n_clauses - 1) as f32) + clause.len() as f32)
                 / self.stats.n_clauses as f32;
         self.state = InternalSolverState::Input;
         // Call minisat backend
-        clause.into_iter().for_each(|l| unsafe {
+        clause.iter().for_each(|l| unsafe {
             ffi::cminisat_add(self.handle, l.to_ipasir());
         });
         unsafe { ffi::cminisat_add(self.handle, 0) };

minisat/src/simp.rs

@@ -90,6 +90,15 @@ impl Extend<Clause> for Minisat {
     }
 }
 
+impl<'a> Extend<&'a Clause> for Minisat {
+    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")
+        })
+    }
+}
+
 impl Solve for Minisat {
     fn signature(&self) -> &'static str {
         let c_chars = unsafe { ffi::cminisat_signature() };
@@ -158,15 +167,15 @@ impl Solve for Minisat {
         }
     }
 
-    fn add_clause(&mut self, clause: Clause) -> anyhow::Result<()> {
+    fn add_clause_ref(&mut self, clause: &Clause) -> anyhow::Result<()> {
         // Update wrapper-internal state
         self.stats.n_clauses += 1;
         self.stats.avg_clause_len =
             (self.stats.avg_clause_len * ((self.stats.n_clauses - 1) as f32) + clause.len() as f32)
                 / self.stats.n_clauses as f32;
         self.state = InternalSolverState::Input;
         // Call minisat backend
-        clause.into_iter().for_each(|l| unsafe {
+        clause.iter().for_each(|l| unsafe {
             ffi::cminisatsimp_add(self.handle, l.to_ipasir());
         });
         unsafe { ffi::cminisatsimp_add(self.handle, 0) };

rustsat/.gitignore

@@ -0,0 +1,4 @@
+rustsat-test.opb
+rustsat-test.cnf
+rustsat-test.wcnf
+rustsat-test.mcnf

rustsat/src/encodings/card.rs

@@ -356,7 +356,7 @@ pub fn encode_cardinality_constraint<CE: BoundBoth + FromIterator<Lit>, Col: Col
         return;
     }
     if constr.is_clause() {
-        collector.extend([constr.as_clause().unwrap()]);
+        collector.extend([constr.into_clause().unwrap()]);
         return;
     }
     CE::encode_constr(constr, collector, var_manager).unwrap()

rustsat/src/encodings/nodedb.rs

@@ -291,6 +291,7 @@ impl NodeCon {
 }
 
 /// Trait for a database managing [`NodeLike`]s by their [`NodeId`]s
+#[allow(dead_code)]
 pub trait NodeById: IndexMut<NodeId, Output = Self::Node> {
     /// The type of node in the database
     type Node: NodeLike;

rustsat/src/encodings/pb.rs

@@ -405,11 +405,11 @@ pub fn encode_pb_constraint<PBE: BoundBoth + FromIterator<(Lit, usize)>, Col: Co
         return;
     }
     if constr.is_clause() {
-        collector.extend([constr.as_clause().unwrap()]);
+        collector.extend([constr.into_clause().unwrap()]);
         return;
     }
     if constr.is_card() {
-        let card = constr.as_card_constr().unwrap();
+        let card = constr.into_card_constr().unwrap();
         return card::default_encode_cardinality_constraint(card, collector, var_manager);
     }
     PBE::encode_constr(constr, collector, var_manager).unwrap()

rustsat/src/instances/fio.rs

@@ -17,29 +17,35 @@ pub struct ObjNoExist(usize);
 
 /// Opens a reader for the file at Path.
 /// With feature `compression` supports bzip2 and gzip compression.
-pub(crate) fn open_compressed_uncompressed_read<P: AsRef<Path>>(
+pub fn open_compressed_uncompressed_read<P: AsRef<Path>>(
     path: P,
-) -> Result<Box<dyn io::Read>, io::Error> {
+) -> Result<Box<dyn io::BufRead>, io::Error> {
     let path = path.as_ref();
     let raw_reader = File::open(path)?;
     #[cfg(feature = "compression")]
     if let Some(ext) = path.extension() {
         if ext.eq_ignore_ascii_case(std::ffi::OsStr::new("bz2")) {
-            return Ok(Box::new(bzip2::read::BzDecoder::new(raw_reader)));
+            return Ok(Box::new(io::BufReader::new(bzip2::read::BzDecoder::new(
+                raw_reader,
+            ))));
         }
         if ext.eq_ignore_ascii_case(std::ffi::OsStr::new("gz")) {
-            return Ok(Box::new(flate2::read::GzDecoder::new(raw_reader)));
+            return Ok(Box::new(io::BufReader::new(flate2::read::GzDecoder::new(
+                raw_reader,
+            ))));
         }
         if ext.eq_ignore_ascii_case(std::ffi::OsStr::new("xz")) {
-            return Ok(Box::new(xz2::read::XzDecoder::new(raw_reader)));
+            return Ok(Box::new(io::BufReader::new(xz2::read::XzDecoder::new(
+                raw_reader,
+            ))));
         }
     }
-    Ok(Box::new(raw_reader))
+    Ok(Box::new(io::BufReader::new(raw_reader)))
 }
 
 /// Opens a writer for the file at Path.
 /// With feature `compression` supports bzip2 and gzip compression.
-pub(crate) fn open_compressed_uncompressed_write<P: AsRef<Path>>(
+pub fn open_compressed_uncompressed_write<P: AsRef<Path>>(
     path: P,
 ) -> Result<Box<dyn io::Write>, io::Error> {
     let path = path.as_ref();