Refactor the trait on ClauseDB

src/assign/propagate.rs

@@ -2,7 +2,12 @@
 // This version can handle Chronological and Non Chronological Backtrack.
 use {
     super::{AssignStack, VarManipulateIF},
-    crate::{cdb::ClauseDBIF, types::*, vam::VarActivityManager, var_vector::*},
+    crate::{
+        cdb::{ClauseDB, ClauseDBIF},
+        types::*,
+        vam::VarActivityManager,
+        var_vector::*,
+    },
 };
 
 #[cfg(feature = "trail_saving")]
@@ -38,11 +43,11 @@ pub trait PropagateIF {
     /// execute backjump in vivification sandbox
     fn backtrack_sandbox(&mut self);
     /// execute *boolean constraint propagation* or *unit propagation*.
-    fn propagate(&mut self, cdb: &mut impl ClauseDBIF) -> PropagationResult;
+    fn propagate(&mut self, cdb: &mut ClauseDB) -> PropagationResult;
     /// `propagate` for vivification, which allows dead clauses.
-    fn propagate_sandbox(&mut self, cdb: &mut impl ClauseDBIF) -> PropagationResult;
+    fn propagate_sandbox(&mut self, cdb: &mut ClauseDB) -> PropagationResult;
     /// propagate then clear asserted literals
-    fn clear_asserted_literals(&mut self, cdb: &mut impl ClauseDBIF) -> MaybeInconsistent;
+    fn clear_asserted_literals(&mut self, cdb: &mut ClauseDB) -> MaybeInconsistent;
 }
 
 impl PropagateIF for AssignStack {
@@ -264,7 +269,7 @@ impl PropagateIF for AssignStack {
     ///    So Eliminator should call `garbage_collect` before me.
     ///  - The order of literals in binary clauses will be modified to hold
     ///    propagation order.
-    fn propagate(&mut self, cdb: &mut impl ClauseDBIF) -> PropagationResult {
+    fn propagate(&mut self, cdb: &mut ClauseDB) -> PropagationResult {
         #[cfg(feature = "boundary_check")]
         macro_rules! check_in {
             ($cid: expr, $tag :expr) => {
@@ -510,7 +515,7 @@ impl PropagateIF for AssignStack {
     // 1. (allow dead clauses)
     // 1. (allow eliminated vars)
     //
-    fn propagate_sandbox(&mut self, cdb: &mut impl ClauseDBIF) -> PropagationResult {
+    fn propagate_sandbox(&mut self, cdb: &mut ClauseDB) -> PropagationResult {
         #[cfg(feature = "boundary_check")]
         macro_rules! check_in {
             ($cid: expr, $tag :expr) => {
@@ -675,7 +680,7 @@ impl PropagateIF for AssignStack {
         }
         Ok(())
     }
-    fn clear_asserted_literals(&mut self, cdb: &mut impl ClauseDBIF) -> MaybeInconsistent {
+    fn clear_asserted_literals(&mut self, cdb: &mut ClauseDB) -> MaybeInconsistent {
         debug_assert_eq!(self.decision_level(), self.root_level);
         loop {
             if self.remains() {
@@ -705,7 +710,7 @@ impl AssignStack {
         assert_ne!(VarRef::lit_assigned(b1), Some(false));
     }
     /// simplify clauses by propagating literals at root level.
-    fn propagate_at_root_level(&mut self, cdb: &mut impl ClauseDBIF) -> MaybeInconsistent {
+    fn propagate_at_root_level(&mut self, cdb: &mut ClauseDB) -> MaybeInconsistent {
         let mut num_propagated = 0;
         while num_propagated < self.trail.len() {
             num_propagated = self.trail.len();

src/cdb/db.rs

@@ -278,23 +278,63 @@ impl Instantiate for ClauseDB {
     }
 }
 
-impl ClauseDBIF for ClauseDB {
-    fn len(&self) -> usize {
+impl ClauseDB {
+    /// return the length of `clause`.
+    pub fn len(&self) -> usize {
         self.clause.len()
     }
-    fn is_empty(&self) -> bool {
+    /// return true if it's empty.
+    pub fn is_empty(&self) -> bool {
         self.clause.is_empty()
     }
-    fn iter(&self) -> Iter<'_, Clause> {
+    /// return an iterator.
+    pub fn iter(&self) -> Iter<'_, Clause> {
         self.clause.iter()
     }
-    fn iter_mut(&mut self) -> IterMut<'_, Clause> {
-        self.clause.iter_mut()
-    }
+
+    //
+    //## interface to binary links
+    //
+
+    /// return binary links: `BinaryLinkList` connected with a `Lit`.
     #[inline]
-    fn binary_links(&self, l: Lit) -> &BinaryLinkList {
+    pub fn binary_links(&self, l: Lit) -> &BinaryLinkList {
         self.binary_link.connect_with(l)
     }
+    /// check the number of clauses
+    /// * `Err(SolverError::OutOfMemory)` -- the db size is over the limit.
+    /// * `Ok(true)` -- enough small
+    /// * `Ok(false)` -- close to the limit
+    pub fn check_size(&self) -> Result<bool, SolverError> {
+        if self.soft_limit == 0 || self.num_clause <= self.soft_limit {
+            let nc = self.derefer(property::Tusize::NumClause);
+            Ok(0 == self.soft_limit || 4 * nc < 3 * self.soft_limit)
+        } else {
+            Err(SolverError::OutOfMemory)
+        }
+    }
+    /// returns None if the given assignment is a model of a problem.
+    /// Otherwise returns a clause which is not satisfiable under a given assignment.
+    /// Clauses with an unassigned literal are treated as falsified in `strict` mode.
+    pub fn validate(&self, model: &[Option<bool>], strict: bool) -> Option<ClauseId> {
+        for (i, c) in self.clause.iter().enumerate().skip(1) {
+            if c.is_dead() || (strict && c.is(FlagClause::LEARNT)) {
+                continue;
+            }
+            match c.evaluate(model) {
+                Some(false) => return Some(ClauseId::from(i)),
+                None if strict => return Some(ClauseId::from(i)),
+                _ => (),
+            }
+        }
+        None
+    }
+}
+
+impl ClauseDBIF for ClauseDB {
+    fn iter_mut(&mut self) -> IterMut<'_, Clause> {
+        self.clause.iter_mut()
+    }
     // watch_cache_IF
     fn fetch_watch_cache_entry(&self, lit: Lit, wix: WatchCacheProxy) -> (ClauseId, Lit) {
         self.watch_cache[lit][wix]
@@ -1119,27 +1159,6 @@ impl ClauseDBIF for ClauseDB {
     fn certificate_save(&mut self) {
         self.certification_store.close();
     }
-    fn check_size(&self) -> Result<bool, SolverError> {
-        if self.soft_limit == 0 || self.num_clause <= self.soft_limit {
-            let nc = self.derefer(property::Tusize::NumClause);
-            Ok(0 == self.soft_limit || 4 * nc < 3 * self.soft_limit)
-        } else {
-            Err(SolverError::OutOfMemory)
-        }
-    }
-    fn validate(&self, model: &[Option<bool>], strict: bool) -> Option<ClauseId> {
-        for (i, c) in self.clause.iter().enumerate().skip(1) {
-            if c.is_dead() || (strict && c.is(FlagClause::LEARNT)) {
-                continue;
-            }
-            match c.evaluate(model) {
-                Some(false) => return Some(ClauseId::from(i)),
-                None if strict => return Some(ClauseId::from(i)),
-                _ => (),
-            }
-        }
-        None
-    }
     #[allow(clippy::unnecessary_cast)]
     fn minimize_with_bi_clauses(&mut self, vec: &mut Vec<Lit>) {
         if vec.len() <= 1 {

src/cdb/mod.rs

@@ -26,10 +26,7 @@ pub use self::{
 
 use {
     crate::{assign::AssignStack, types::*},
-    std::{
-        ops::IndexMut,
-        slice::{Iter, IterMut},
-    },
+    std::{ops::IndexMut, slice::IterMut},
     watch_cache::{WatchCache, WatchCacheIterator, WatchCacheProxy},
 };
 
@@ -55,22 +52,9 @@ pub trait ClauseDBIF:
     + PropertyDereference<property::Tusize, usize>
     + PropertyDereference<property::Tf64, f64>
 {
-    /// return the length of `clause`.
-    fn len(&self) -> usize;
-    /// return true if it's empty.
-    fn is_empty(&self) -> bool;
-    /// return an iterator.
-    fn iter(&self) -> Iter<'_, Clause>;
     /// return a mutable iterator.
     fn iter_mut(&mut self) -> IterMut<'_, Clause>;
 
-    //
-    //## interface to binary links
-    //
-
-    /// return binary links: `BinaryLinkList` connected with a `Lit`.
-    fn binary_links(&self, l: Lit) -> &BinaryLinkList;
-
     //
     //## abstraction to watch_cache
     //
@@ -128,15 +112,6 @@ pub trait ClauseDBIF:
     fn certificate_add_assertion(&mut self, lit: Lit);
     /// save the certification record to a file.
     fn certificate_save(&mut self);
-    /// check the number of clauses
-    /// * `Err(SolverError::OutOfMemory)` -- the db size is over the limit.
-    /// * `Ok(true)` -- enough small
-    /// * `Ok(false)` -- close to the limit
-    fn check_size(&self) -> Result<bool, SolverError>;
-    /// returns None if the given assignment is a model of a problem.
-    /// Otherwise returns a clause which is not satisfiable under a given assignment.
-    /// Clauses with an unassigned literal are treated as falsified in `strict` mode.
-    fn validate(&self, model: &[Option<bool>], strict: bool) -> Option<ClauseId>;
     /// minimize a clause.
     fn minimize_with_bi_clauses(&mut self, vec: &mut Vec<Lit>);
     /// complete bi-clause network

src/processor/eliminate.rs

@@ -3,7 +3,7 @@ use {
     super::Eliminator,
     crate::{
         assign::{AssignStack, PropagateIF},
-        cdb::ClauseDBIF,
+        cdb::{ClauseDB, ClauseDBIF},
         solver::SolverEvent,
         state::State,
         types::*,
@@ -16,7 +16,7 @@ const COMBINATION_LIMIT: f64 = 32.0;
 
 pub fn eliminate_var(
     asg: &mut AssignStack,
-    cdb: &mut impl ClauseDBIF,
+    cdb: &mut ClauseDB,
     elim: &mut Eliminator,
     state: &mut State,
     vi: VarId,
@@ -142,7 +142,7 @@ pub fn eliminate_var(
 
 /// returns `true` if elimination is impossible.
 fn skip_var_elimination(
-    cdb: &impl ClauseDBIF,
+    cdb: &ClauseDB,
     pos: &[ClauseId],
     neg: &[ClauseId],
     v: VarId,
@@ -181,7 +181,7 @@ fn skip_var_elimination(
 /// Returns the the-size-of-clause-being-generated.
 /// - `(false, -)` if one of the clauses is always satisfied.
 /// - `(true, n)` if they are merge-able to a n-literal clause.
-fn merge_cost(cdb: &impl ClauseDBIF, cp: ClauseId, cq: ClauseId, vi: VarId) -> Option<usize> {
+fn merge_cost(cdb: &ClauseDB, cp: ClauseId, cq: ClauseId, vi: VarId) -> Option<usize> {
     let c_p = &cdb[cp];
     let c_q = &cdb[cq];
     let mut cond: Option<Lit> = None;
@@ -222,13 +222,7 @@ fn merge_cost(cdb: &impl ClauseDBIF, cp: ClauseId, cq: ClauseId, vi: VarId) -> O
 
 /// Return the real length of the generated clause by merging two clauses.
 /// Return **zero** if one of the clauses is always satisfied. (merge_vec should not be used.)
-fn merge(
-    cdb: &mut impl ClauseDBIF,
-    cip: ClauseId,
-    ciq: ClauseId,
-    vi: VarId,
-    vec: &mut Vec<Lit>,
-) -> usize {
+fn merge(cdb: &mut ClauseDB, cip: ClauseId, ciq: ClauseId, vi: VarId, vec: &mut Vec<Lit>) -> usize {
     vec.clear();
     let pqb = &cdb[cip];
     let qpb = &cdb[ciq];
@@ -259,7 +253,7 @@ fn merge(
 }
 
 fn make_eliminated_clauses(
-    cdb: &mut impl ClauseDBIF,
+    cdb: &mut ClauseDB,
     store: &mut Vec<Lit>,
     v: VarId,
     pos: &[ClauseId],
@@ -287,12 +281,7 @@ fn make_eliminating_unit_clause(store: &mut Vec<Lit>, x: Lit) {
     store.push(Lit::from(1usize));
 }
 
-fn make_eliminated_clause(
-    cdb: &mut impl ClauseDBIF,
-    store: &mut Vec<Lit>,
-    vi: VarId,
-    cid: ClauseId,
-) {
+fn make_eliminated_clause(cdb: &mut ClauseDB, store: &mut Vec<Lit>, vi: VarId, cid: ClauseId) {
     let first = store.len();
     // Copy clause to the vector. Remember the position where the variable 'v' occurs:
     let c = &cdb[cid];

src/processor/mod.rs

@@ -28,7 +28,7 @@ mod subsume;
 use {
     crate::{
         assign::AssignStack,
-        cdb::ClauseDBIF,
+        cdb::ClauseDB,
         processor::heap::{LitOccurs, VarOccHeap},
         state::State,
         types::*,
@@ -51,7 +51,7 @@ pub trait EliminateIF: Instantiate {
     /// check if the eliminator is running.
     fn is_running(&self) -> bool;
     /// rebuild occur lists.
-    fn prepare(&mut self, cdb: &mut impl ClauseDBIF, force: bool);
+    fn prepare(&mut self, cdb: &mut ClauseDB, force: bool);
     /// enqueue a var into eliminator's var queue.
     fn enqueue_var(&mut self, vi: VarId, upward: bool);
     /// simplify database by:
@@ -66,7 +66,7 @@ pub trait EliminateIF: Instantiate {
     fn simplify(
         &mut self,
         asg: &mut AssignStack,
-        cdb: &mut impl ClauseDBIF,
+        cdb: &mut ClauseDB,
         state: &mut State,
         force_run: bool,
     ) -> MaybeInconsistent;

src/processor/simplify.rs

@@ -6,7 +6,7 @@ use {
     },
     crate::{
         assign::{self, AssignStack, PropagateIF},
-        cdb::{self, ClauseDBIF},
+        cdb::{self, ClauseDB, ClauseDBIF},
         state::{self, State, StateIF},
         types::*,
         var_vector::*,
@@ -220,7 +220,7 @@ impl EliminateIF for Eliminator {
     fn is_running(&self) -> bool {
         self.enable && self.mode == EliminatorMode::Running
     }
-    fn prepare(&mut self, cdb: &mut impl ClauseDBIF, force: bool) {
+    fn prepare(&mut self, cdb: &mut ClauseDB, force: bool) {
         if !self.enable {
             return;
         }
@@ -261,7 +261,7 @@ impl EliminateIF for Eliminator {
     fn simplify(
         &mut self,
         asg: &mut AssignStack,
-        cdb: &mut impl ClauseDBIF,
+        cdb: &mut ClauseDB,
         state: &mut State,
         force_run: bool,
     ) -> MaybeInconsistent {
@@ -409,7 +409,7 @@ impl Eliminator {
     pub fn backward_subsumption_check(
         &mut self,
         asg: &mut AssignStack,
-        cdb: &mut impl ClauseDBIF,
+        cdb: &mut ClauseDB,
         timedout: &mut usize,
     ) -> MaybeInconsistent {
         debug_assert_eq!(asg.decision_level(), 0);
@@ -503,7 +503,7 @@ impl Eliminator {
     fn eliminate(
         &mut self,
         asg: &mut AssignStack,
-        cdb: &mut impl ClauseDBIF,
+        cdb: &mut ClauseDB,
         state: &mut State,
     ) -> MaybeInconsistent {
         let start = state.elapsed().unwrap_or(0.0);
@@ -530,7 +530,7 @@ impl Eliminator {
     fn eliminate_main(
         &mut self,
         asg: &mut AssignStack,
-        cdb: &mut impl ClauseDBIF,
+        cdb: &mut ClauseDB,
         state: &mut State,
     ) -> MaybeInconsistent {
         debug_assert!(asg.decision_level() == 0);
@@ -628,7 +628,7 @@ impl Eliminator {
 }
 
 #[allow(dead_code)]
-fn check_eliminator(cdb: &impl ClauseDBIF, elim: &Eliminator) -> bool {
+fn check_eliminator(cdb: &ClauseDB, elim: &Eliminator) -> bool {
     // clause_queue should be clear.
     // all elements in occur_lists exist.
     // for v in asg {

src/solver/validate.rs

@@ -1,7 +1,6 @@
 //! Crate `validator` implements a model checker.
 use crate::{
     assign::PropagateIF,
-    cdb::ClauseDBIF,
     solver::Solver,
     types::{Lit, MaybeInconsistent, SolverError},
 };