feat: Extend<&Clause> for solvers

chrjabs · Apr 15, 2024 · f5921f4 · f5921f4
1 parent 887cae1
commit f5921f4
Show file tree

Hide file tree

Showing 8 changed files with 64 additions and 1 deletion.
diff --git a/cadical/src/lib.rs b/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() };

diff --git a/glucose/src/core.rs b/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() };

diff --git a/glucose/src/simp.rs b/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() };

diff --git a/ipasir/src/lib.rs b/ipasir/src/lib.rs
@@ -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};

diff --git a/kissat/src/lib.rs b/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() };

diff --git a/minisat/src/core.rs b/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() };

diff --git a/minisat/src/simp.rs b/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() };

diff --git a/rustsat/src/solvers.rs b/rustsat/src/solvers.rs
@@ -96,7 +96,7 @@ use thiserror::Error;
 /// 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.
-pub trait Solve: Extend<Clause> {
+pub trait Solve: Extend<Clause> + for<'a> Extend<&'a Clause> {
     /// Gets a signature of the solver implementation
     fn signature(&self) -> &'static str;
     /// Reserves memory in the solver until a maximum variables, if the solver