feat: Cl as light-weight DST for clauses

`Cl` is to `Clause` what `str` is to `String`
chrjabs · Jul 17, 2024 · 92bd34a · 92bd34a
1 parent 4941657
commit 92bd34a
Show file tree

Hide file tree

Showing 15 changed files with 393 additions and 176 deletions.
diff --git a/Cargo.toml b/Cargo.toml
@@ -33,6 +33,7 @@ flate2 = { version = "1.0.30", features = [
 ], default-features = false }
 git2 = "0.19.0"
 glob = "0.3.1"
+itertools = "0.13.0"
 nom = "7.1.3"
 termcolor = "1.4.1"
 thiserror = "1.0.61"
@@ -68,6 +69,7 @@ thiserror.workspace = true
 visibility.workspace = true
 bzip2 = { workspace = true, optional = true }
 flate2 = { workspace = true, optional = true }
+itertools.workspace = true
 rand = { workspace = true, optional = true }
 rustc-hash = { workspace = true, optional = true }
 tempfile.workspace = true

diff --git a/batsat/src/lib.rs b/batsat/src/lib.rs
@@ -17,7 +17,7 @@ use batsat::{intmap::AsIndex, lbool, Callbacks, SolverInterface};
 use cpu_time::ProcessTime;
 use rustsat::{
     solvers::{Solve, SolveIncremental, SolveStats, SolverResult, SolverStats},
-    types::{Clause, Lit, TernaryVal, Var},
+    types::{Cl, Clause, Lit, TernaryVal, Var},
 };
 
 /// RustSAT wrapper for [`batsat::BasicSolver`]
@@ -49,7 +49,7 @@ impl<Cb: Callbacks> Solver<Cb> {
 
     #[allow(clippy::cast_precision_loss)]
     #[inline]
-    fn update_avg_clause_len(&mut self, clause: &Clause) {
+    fn update_avg_clause_len(&mut self, clause: &Cl) {
         self.avg_clause_len = (self.avg_clause_len * ((self.n_clauses()) as f32)
             + clause.len() as f32)
             / (self.n_clauses() + 1) as f32;
@@ -89,8 +89,12 @@ impl<Cb: Callbacks> Extend<Clause> for Solver<Cb> {
     }
 }
 
-impl<'a, Cb: Callbacks> Extend<&'a Clause> for Solver<Cb> {
-    fn extend<T: IntoIterator<Item = &'a Clause>>(&mut self, iter: T) {
+impl<'a, C, Cb> Extend<&'a C> for Solver<Cb>
+where
+    C: AsRef<Cl> + ?Sized,
+    Cb: Callbacks,
+{
+    fn extend<T: IntoIterator<Item = &'a C>>(&mut self, iter: T) {
         iter.into_iter().for_each(|cl| {
             self.add_clause_ref(cl)
                 .expect("Error adding clause in extend");
@@ -118,13 +122,17 @@ impl<Cb: Callbacks> Solve for Solver<Cb> {
         }
     }
 
-    fn add_clause_ref(&mut self, clause: &Clause) -> anyhow::Result<()> {
+    fn add_clause_ref<C>(&mut self, clause: &C) -> anyhow::Result<()>
+    where
+        C: AsRef<Cl> + ?Sized,
+    {
+        let clause = clause.as_ref();
         self.update_avg_clause_len(clause);
 
-        let mut c: Vec<batsat::Lit> = clause
+        let mut c: Vec<_> = clause
             .iter()
             .map(|l| batsat::Lit::new(self.internal.var_of_int(l.vidx32() + 1), l.is_pos()))
-            .collect::<Vec<batsat::Lit>>();
+            .collect();
 
         self.internal.add_clause_reuse(&mut c);
 

diff --git a/cadical/src/lib.rs b/cadical/src/lib.rs
@@ -32,7 +32,7 @@ use rustsat::solvers::{
     LimitDecisions, PhaseLit, Propagate, PropagateResult, Solve, SolveIncremental, SolveStats,
     SolverResult, SolverState, SolverStats, StateError, Terminate,
 };
-use rustsat::types::{Clause, Lit, TernaryVal, Var};
+use rustsat::types::{Cl, Clause, Lit, TernaryVal, Var};
 use thiserror::Error;
 
 macro_rules! handle_oom {
@@ -142,7 +142,7 @@ impl CaDiCaL<'_, '_> {
 
     #[allow(clippy::cast_precision_loss)]
     #[inline]
-    fn update_avg_clause_len(&mut self, clause: &Clause) {
+    fn update_avg_clause_len(&mut self, clause: &Cl) {
         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;
@@ -158,7 +158,11 @@ impl CaDiCaL<'_, '_> {
     /// # Errors
     ///
     /// Returns [`rustsat::OutOfMemory`] if CaDiCaL throws `std::bad_alloc`.
-    pub fn add_tmp_clause(&mut self, clause: &Clause) -> Result<(), rustsat::OutOfMemory> {
+    pub fn add_tmp_clause<C>(&mut self, clause: &C) -> Result<(), rustsat::OutOfMemory>
+    where
+        C: AsRef<Cl> + ?Sized,
+    {
+        let clause = clause.as_ref();
         // Update wrapper-internal state
         self.stats.n_clauses += 1;
         self.update_avg_clause_len(clause);
@@ -449,8 +453,11 @@ impl Extend<Clause> for CaDiCaL<'_, '_> {
     }
 }
 
-impl<'a> Extend<&'a Clause> for CaDiCaL<'_, '_> {
-    fn extend<T: IntoIterator<Item = &'a Clause>>(&mut self, iter: T) {
+impl<'a, C> Extend<&'a C> for CaDiCaL<'_, '_>
+where
+    C: AsRef<Cl> + ?Sized,
+{
+    fn extend<T: IntoIterator<Item = &'a C>>(&mut self, iter: T) {
         iter.into_iter().for_each(|cl| {
             self.add_clause_ref(cl)
                 .expect("Error adding clause in extend");
@@ -534,7 +541,11 @@ impl Solve for CaDiCaL<'_, '_> {
         }
     }
 
-    fn add_clause_ref(&mut self, clause: &Clause) -> anyhow::Result<()> {
+    fn add_clause_ref<C>(&mut self, clause: &C) -> anyhow::Result<()>
+    where
+        C: AsRef<Cl> + ?Sized,
+    {
+        let clause = clause.as_ref();
         // Update wrapper-internal state
         self.stats.n_clauses += 1;
         self.update_avg_clause_len(clause);

diff --git a/glucose/src/core.rs b/glucose/src/core.rs
@@ -12,7 +12,7 @@ use rustsat::{
         Propagate, PropagateResult, Solve, SolveIncremental, SolveStats, SolverResult, SolverState,
         SolverStats, StateError,
     },
-    types::{Clause, Lit, TernaryVal, Var},
+    types::{Cl, Clause, Lit, TernaryVal, Var},
 };
 
 use super::{ffi, handle_oom, InternalSolverState, InvalidApiReturn, Limit};
@@ -61,7 +61,7 @@ impl Glucose {
 
     #[allow(clippy::cast_precision_loss)]
     #[inline]
-    fn update_avg_clause_len(&mut self, clause: &Clause) {
+    fn update_avg_clause_len(&mut self, clause: &Cl) {
         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;
@@ -98,8 +98,11 @@ impl Extend<Clause> for Glucose {
     }
 }
 
-impl<'a> Extend<&'a Clause> for Glucose {
-    fn extend<T: IntoIterator<Item = &'a Clause>>(&mut self, iter: T) {
+impl<'a, C> Extend<&'a C> for Glucose
+where
+    C: AsRef<Cl> + ?Sized,
+{
+    fn extend<T: IntoIterator<Item = &'a C>>(&mut self, iter: T) {
         iter.into_iter().for_each(|cl| {
             self.add_clause_ref(cl)
                 .expect("Error adding clause in extend");
@@ -175,7 +178,11 @@ impl Solve for Glucose {
         }
     }
 
-    fn add_clause_ref(&mut self, clause: &Clause) -> anyhow::Result<()> {
+    fn add_clause_ref<C>(&mut self, clause: &C) -> anyhow::Result<()>
+    where
+        C: AsRef<Cl> + ?Sized,
+    {
+        let clause = clause.as_ref();
         // Update wrapper-internal state
         self.stats.n_clauses += 1;
         self.update_avg_clause_len(clause);

diff --git a/glucose/src/simp.rs b/glucose/src/simp.rs
@@ -12,7 +12,7 @@ use rustsat::{
         PhaseLit, Propagate, PropagateResult, Solve, SolveIncremental, SolveStats, SolverResult,
         SolverState, SolverStats, StateError,
     },
-    types::{Clause, Lit, TernaryVal, Var},
+    types::{Cl, Clause, Lit, TernaryVal, Var},
 };
 
 use super::{ffi, handle_oom, AssumpEliminated, InternalSolverState, InvalidApiReturn, Limit};
@@ -60,7 +60,7 @@ impl Glucose {
     }
 
     #[allow(clippy::cast_precision_loss)]
-    fn update_avg_clause_len(&mut self, clause: &Clause) {
+    fn update_avg_clause_len(&mut self, clause: &Cl) {
         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;
@@ -104,8 +104,11 @@ impl Extend<Clause> for Glucose {
     }
 }
 
-impl<'a> Extend<&'a Clause> for Glucose {
-    fn extend<T: IntoIterator<Item = &'a Clause>>(&mut self, iter: T) {
+impl<'a, C> Extend<&'a C> for Glucose
+where
+    C: AsRef<Cl> + ?Sized,
+{
+    fn extend<T: IntoIterator<Item = &'a C>>(&mut self, iter: T) {
         iter.into_iter().for_each(|cl| {
             self.add_clause_ref(cl)
                 .expect("Error adding clause in extend");
@@ -181,7 +184,11 @@ impl Solve for Glucose {
         }
     }
 
-    fn add_clause_ref(&mut self, clause: &Clause) -> anyhow::Result<()> {
+    fn add_clause_ref<C>(&mut self, clause: &C) -> anyhow::Result<()>
+    where
+        C: AsRef<Cl> + ?Sized,
+    {
+        let clause = clause.as_ref();
         // Update wrapper-internal state
         self.stats.n_clauses += 1;
         self.update_avg_clause_len(clause);

diff --git a/ipasir/src/lib.rs b/ipasir/src/lib.rs
@@ -39,7 +39,7 @@ use rustsat::{
         ControlSignal, Learn, Solve, SolveIncremental, SolveStats, SolverResult, SolverState,
         SolverStats, StateError, Terminate,
     },
-    types::{Clause, Lit, TernaryVal},
+    types::{Cl, Clause, Lit, TernaryVal},
 };
 use thiserror::Error;
 
@@ -123,7 +123,7 @@ impl IpasirSolver<'_, '_> {
 
     #[allow(clippy::cast_precision_loss)]
     #[inline]
-    fn update_avg_clause_len(&mut self, clause: &Clause) {
+    fn update_avg_clause_len(&mut self, clause: &Cl) {
         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;
@@ -198,7 +198,11 @@ impl Solve for IpasirSolver<'_, '_> {
         }
     }
 
-    fn add_clause_ref(&mut self, clause: &Clause) -> anyhow::Result<()> {
+    fn add_clause_ref<C>(&mut self, clause: &C) -> anyhow::Result<()>
+    where
+        C: AsRef<Cl> + ?Sized,
+    {
+        let clause = clause.as_ref();
         // Update wrapper-internal state
         self.stats.n_clauses += 1;
         clause.iter().for_each(|l| match self.stats.max_var {
@@ -381,8 +385,11 @@ impl Extend<Clause> for IpasirSolver<'_, '_> {
     }
 }
 
-impl<'a> Extend<&'a Clause> for IpasirSolver<'_, '_> {
-    fn extend<T: IntoIterator<Item = &'a Clause>>(&mut self, iter: T) {
+impl<'a, C> Extend<&'a C> for IpasirSolver<'_, '_>
+where
+    C: AsRef<Cl> + ?Sized,
+{
+    fn extend<T: IntoIterator<Item = &'a C>>(&mut self, iter: T) {
         iter.into_iter().for_each(|cl| {
             self.add_clause_ref(cl)
                 .expect("Error adding clause in extend");

diff --git a/kissat/src/lib.rs b/kissat/src/lib.rs
@@ -35,7 +35,7 @@ use rustsat::{
         ControlSignal, Interrupt, InterruptSolver, Solve, SolveStats, SolverResult, SolverState,
         SolverStats, StateError, Terminate,
     },
-    types::{Clause, Lit, TernaryVal, Var},
+    types::{Cl, Clause, Lit, TernaryVal, Var},
 };
 use thiserror::Error;
 
@@ -98,7 +98,7 @@ impl Default for Kissat<'_> {
 impl Kissat<'_> {
     #[allow(clippy::cast_precision_loss)]
     #[inline]
-    fn update_avg_clause_len(&mut self, clause: &Clause) {
+    fn update_avg_clause_len(&mut self, clause: &Cl) {
         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;
@@ -224,8 +224,11 @@ impl Extend<Clause> for Kissat<'_> {
     }
 }
 
-impl<'a> Extend<&'a Clause> for Kissat<'_> {
-    fn extend<T: IntoIterator<Item = &'a Clause>>(&mut self, iter: T) {
+impl<'a, C> Extend<&'a C> for Kissat<'_>
+where
+    C: AsRef<Cl> + ?Sized,
+{
+    fn extend<T: IntoIterator<Item = &'a C>>(&mut self, iter: T) {
         iter.into_iter().for_each(|cl| {
             self.add_clause_ref(cl)
                 .expect("Error adding clause in extend");
@@ -305,7 +308,10 @@ impl Solve for Kissat<'_> {
         }
     }
 
-    fn add_clause_ref(&mut self, clause: &Clause) -> anyhow::Result<()> {
+    fn add_clause_ref<C>(&mut self, clause: &C) -> anyhow::Result<()>
+    where
+        C: AsRef<Cl> + ?Sized,
+    {
         // Kissat is non-incremental, so only add if in input or configuring state
         if !matches!(
             self.state,
@@ -317,6 +323,7 @@ impl Solve for Kissat<'_> {
             }
             .into());
         }
+        let clause = clause.as_ref();
         // Update wrapper-internal state
         self.stats.n_clauses += 1;
         self.update_avg_clause_len(clause);

diff --git a/minisat/src/core.rs b/minisat/src/core.rs
@@ -12,7 +12,7 @@ use rustsat::{
         Propagate, PropagateResult, Solve, SolveIncremental, SolveStats, SolverResult, SolverState,
         SolverStats, StateError,
     },
-    types::{Clause, Lit, TernaryVal, Var},
+    types::{Cl, Clause, Lit, TernaryVal, Var},
 };
 
 use super::{ffi, handle_oom, InternalSolverState, InvalidApiReturn, Limit};
@@ -61,7 +61,7 @@ impl Minisat {
 
     #[allow(clippy::cast_precision_loss)]
     #[inline]
-    fn update_avg_clause_len(&mut self, clause: &Clause) {
+    fn update_avg_clause_len(&mut self, clause: &Cl) {
         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;
@@ -98,8 +98,11 @@ impl Extend<Clause> for Minisat {
     }
 }
 
-impl<'a> Extend<&'a Clause> for Minisat {
-    fn extend<T: IntoIterator<Item = &'a Clause>>(&mut self, iter: T) {
+impl<'a, C> Extend<&'a C> for Minisat
+where
+    C: AsRef<Cl> + ?Sized,
+{
+    fn extend<T: IntoIterator<Item = &'a C>>(&mut self, iter: T) {
         iter.into_iter().for_each(|cl| {
             self.add_clause_ref(cl)
                 .expect("Error adding clause in extend");
@@ -175,7 +178,11 @@ impl Solve for Minisat {
         }
     }
 
-    fn add_clause_ref(&mut self, clause: &Clause) -> anyhow::Result<()> {
+    fn add_clause_ref<C>(&mut self, clause: &C) -> anyhow::Result<()>
+    where
+        C: AsRef<Cl> + ?Sized,
+    {
+        let clause = clause.as_ref();
         // Update wrapper-internal state
         self.stats.n_clauses += 1;
         self.update_avg_clause_len(clause);