From a882f92c0c69ee9d73bc79bba55f331797dc39d9 Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Tue, 14 Mar 2023 01:10:33 +0900
Subject: [PATCH 01/19] adapt to bitflags-2.0

---
 Cargo.toml   |  2 +-
 src/types.rs | 11 ++++-------
 2 files changed, 5 insertions(+), 8 deletions(-)

diff --git a/Cargo.toml b/Cargo.toml
index 9b876dea6..70649cff1 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -14,7 +14,7 @@ default-run = "splr"
 rust-version = "1.65"
 
 [dependencies]
-bitflags = "^1.3"
+bitflags = "^2.0"
 
 [features]
 default = [
diff --git a/src/types.rs b/src/types.rs
index 550268450..3d088a6c3 100644
--- a/src/types.rs
+++ b/src/types.rs
@@ -398,9 +398,10 @@ impl fmt::Display for SolverError {
 pub type MaybeInconsistent = Result<(), SolverError>;
 
 /// CNF locator
-#[derive(Clone, Debug)]
+#[derive(Clone, Debug, Default)]
 pub enum CNFIndicator {
     /// not specified
+    #[default]
     Void,
     /// from a file
     File(String),
@@ -408,12 +409,6 @@ pub enum CNFIndicator {
     LitVec(usize),
 }
 
-impl Default for CNFIndicator {
-    fn default() -> Self {
-        CNFIndicator::Void
-    }
-}
-
 impl fmt::Display for CNFIndicator {
     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
         match self {
@@ -570,6 +565,7 @@ pub trait FlagIF {
 
 bitflags! {
     /// Misc flags used by [`Clause`](`crate::cdb::Clause`).
+    #[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord)]
     pub struct FlagClause: u8 {
         /// a clause is a generated clause by conflict analysis and is removable.
         const LEARNT       = 0b0000_0001;
@@ -586,6 +582,7 @@ bitflags! {
 
 bitflags! {
     /// Misc flags used by [`Var`](`crate::assign::Var`).
+    #[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord)]
     pub struct FlagVar: u8 {
         /// * the previous assigned value of a Var.
         const PHASE        = 0b0000_0001;

From ca78c5aff36f80bebba2a7de4f9d3dbd17396df2 Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Tue, 14 Mar 2023 01:12:34 +0900
Subject: [PATCH 02/19] modified:   README.md

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 243d02c1e..3428f2b69 100644
--- a/README.md
+++ b/README.md
@@ -419,4 +419,4 @@ file, You can obtain one at http://mozilla.org/MPL/2.0/.
 
 ---
 
-2020-2022, Narazaki Shuji
+2020-2023, Narazaki Shuji

From a4a8631d27c67e03e10ab8dbd0e49c180202d64d Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Tue, 14 Mar 2023 01:17:23 +0900
Subject: [PATCH 03/19] bump version to 0.18.0-alpha.0

---
 Cargo.toml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cargo.toml b/Cargo.toml
index 70649cff1..25aa1b22c 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "splr"
-version = "0.17.0"
+version = "0.18.0-alpha.1"
 authors = ["Narazaki Shuji <shujinarazaki@protonmail.com>"]
 description = "A modern CDCL SAT solver in Rust"
 edition = "2021"

From d695196459469079af7cb2122e722fe90a490850 Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Fri, 7 Apr 2023 00:53:12 +0900
Subject: [PATCH 04/19] modified:   Cargo.toml

---
 Cargo.toml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cargo.toml b/Cargo.toml
index 25aa1b22c..b93a18c2a 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -14,7 +14,7 @@ default-run = "splr"
 rust-version = "1.65"
 
 [dependencies]
-bitflags = "^2.0"
+bitflags = "^2.1"
 
 [features]
 default = [

From 9919e738913aba343d999808623310b8136b81e5 Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Sat, 15 Apr 2023 09:26:48 +0900
Subject: [PATCH 05/19] rayon-propagete as 0.18.0-alpha.2

---
 Cargo.toml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Cargo.toml b/Cargo.toml
index b93a18c2a..7c7440325 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "splr"
-version = "0.18.0-alpha.1"
+version = "0.18.0-alpha.2"
 authors = ["Narazaki Shuji <shujinarazaki@protonmail.com>"]
 description = "A modern CDCL SAT solver in Rust"
 edition = "2021"
@@ -15,6 +15,7 @@ rust-version = "1.65"
 
 [dependencies]
 bitflags = "^2.1"
+rayon = "^1.7"
 
 [features]
 default = [

From 3f9727bd2e9b4b2524320330c8d202b57588e5b3 Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Sat, 15 Apr 2023 23:54:36 +0900
Subject: [PATCH 06/19] a snapshot under construction

---
 src/assign/propagate.rs | 295 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 295 insertions(+)

diff --git a/src/assign/propagate.rs b/src/assign/propagate.rs
index b2a432558..e2d30a7a3 100644
--- a/src/assign/propagate.rs
+++ b/src/assign/propagate.rs
@@ -39,6 +39,7 @@ pub trait PropagateIF {
     fn backtrack_sandbox(&mut self);
     /// execute *boolean constraint propagation* or *unit propagation*.
     fn propagate(&mut self, cdb: &mut impl ClauseDBIF) -> PropagationResult;
+    fn propagate_p(&mut self, cdb: &mut impl ClauseDBIF) -> PropagationResult;
     /// `propagate` for vivification, which allows dead clauses.
     fn propagate_sandbox(&mut self, cdb: &mut impl ClauseDBIF) -> PropagationResult;
     /// propagate then clear asserted literals
@@ -110,6 +111,13 @@ macro_rules! unset_assign {
     };
 }
 
+enum PropagationContext {
+    Conflict(ClauseId, bool, Option<Lit>),
+    Satisfied(ClauseId),
+    UnitPropagation(ClauseId, Lit, bool, Option<Lit>),
+    UpdateWatch(ClauseId, Lit, usize, usize),
+}
+
 impl PropagateIF for AssignStack {
     fn assign_at_root_level(&mut self, l: Lit) -> MaybeInconsistent {
         self.cancel_until(self.root_level);
@@ -325,6 +333,9 @@ 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_p(&mut self, cdb: &mut impl ClauseDBIF) -> PropagationResult {
+        self.propagate_parallel(cdb)
+    }
     fn propagate(&mut self, cdb: &mut impl ClauseDBIF) -> PropagationResult {
         #[cfg(feature = "boundary_check")]
         macro_rules! check_in {
@@ -760,6 +771,290 @@ impl PropagateIF for AssignStack {
 }
 
 impl AssignStack {
+    fn propagate_parallel(&mut self, cdb: &mut impl ClauseDBIF) -> PropagationResult {
+        #[cfg(feature = "boundary_check")]
+        macro_rules! check_in {
+            ($cid: expr, $tag :expr) => {
+                cdb[$cid].moved_at = $tag;
+            };
+        }
+        #[cfg(not(feature = "boundary_check"))]
+        macro_rules! check_in {
+            ($cid: expr, $tag :expr) => {};
+        }
+
+        macro_rules! conflict_path {
+            ($lit: expr, $reason: expr) => {
+                self.dpc_ema.update(self.num_decision);
+                self.ppc_ema.update(self.num_propagation);
+                self.num_conflict += 1;
+                return Err(($lit, $reason));
+            };
+        }
+
+        #[cfg(feature = "suppress_reason_chain")]
+        macro_rules! minimized_reason {
+            ($lit: expr) => {
+                if let r @ AssignReason::BinaryLink(_) = self.reason[$lit.vi()] {
+                    r
+                } else {
+                    AssignReason::BinaryLink($lit)
+                }
+            };
+        }
+        #[cfg(not(feature = "suppress_reason_chain"))]
+        macro_rules! minimized_reason {
+            ($lit: expr) => {
+                AssignReason::BinaryLink($lit)
+            };
+        }
+
+        #[cfg(feature = "trail_saving")]
+        macro_rules! from_saved_trail {
+            () => {
+                if let cc @ Err(_) = self.reuse_saved_trail(cdb) {
+                    self.num_propagation += 1;
+                    self.num_conflict += 1;
+                    self.num_reconflict += 1;
+                    self.dpc_ema.update(self.num_decision);
+                    self.ppc_ema.update(self.num_propagation);
+                    return cc;
+                }
+            };
+        }
+        #[cfg(not(feature = "trail_saving"))]
+        macro_rules! from_saved_trail {
+            () => {};
+        }
+
+        let dl = self.decision_level();
+        from_saved_trail!();
+        while let Some(p) = self.trail.get(self.q_head) {
+            self.num_propagation += 1;
+            self.q_head += 1;
+            #[cfg(feature = "debug_propagation")]
+            {
+                assert!(!self.var[p.vi()].is(FlagVar::PROPAGATED));
+                self.var[p.vi()].turn_on(FlagVar::PROPAGATED);
+            }
+            let propagating = Lit::from(usize::from(*p));
+            let false_lit = !*p;
+
+            #[cfg(feature = "boundary_check")]
+            {
+                self.var[p.vi()].propagated_at = self.num_conflict;
+                self.var[p.vi()].state = VarState::Propagated(self.num_conflict);
+            }
+            // we have to drop `p` here to use self as a mutable reference again later.
+
+            //
+            //## binary loop
+            //
+            // Note: bi_clause_map contains clauses themselves,
+            // while the key of watch_cache is watching literals.
+            // Therefore keys to access appropriate targets have the opposite phases.
+            //
+            for (blocker, cid) in cdb.binary_links(false_lit).iter().copied() {
+                debug_assert!(!cdb[cid].is_dead());
+                debug_assert!(!self.var[blocker.vi()].is(FlagVar::ELIMINATED));
+                debug_assert_ne!(blocker, false_lit);
+                debug_assert_eq!(cdb[cid].len(), 2);
+                match lit_assign!(self, blocker) {
+                    Some(true) => (),
+                    Some(false) => {
+                        check_in!(cid, Propagate::EmitConflict(self.num_conflict + 1, blocker));
+                        conflict_path!(blocker, minimized_reason!(propagating));
+                    }
+                    None => {
+                        debug_assert!(cdb[cid].lit0() == false_lit || cdb[cid].lit1() == false_lit);
+                        self.assign_by_implication(
+                            blocker,
+                            minimized_reason!(propagating),
+                            #[cfg(feature = "chrono_BT")]
+                            self.level[propagating.vi()],
+                        );
+                    }
+                }
+            }
+            //
+            //## normal clause loop
+            //
+            let mut source = cdb.watch_cache_iter(propagating);
+            while let Some((cid, cached)) = source
+                .next()
+                .map(|index| cdb.fetch_watch_cache_entry(propagating, index))
+            {
+                let c = &cdb[cid];
+                match self.build_propagatation_context(false_lit, cid, c, cached) {
+                    PropagationContext::Conflict(cid, flip_watches, cache) => {
+                        if flip_watches {
+                            cdb.swap_watch(cid);
+                        }
+                        cdb.transform_by_restoring_watch_cache(propagating, &mut source, cache);
+                        check_in!(cid, Propagate::EmitConflict(self.num_conflict + 1, cached));
+                        conflict_path!(cached, AssignReason::Implication(cid));
+                    }
+                    PropagationContext::Satisfied(_cid) => {
+                        // The following doesn't need an ID but the internal pointer in the iterator
+                        cdb.transform_by_restoring_watch_cache(propagating, &mut source, None);
+                        check_in!(cid, Propagate::CacheSatisfied(self.num_conflict));
+                    }
+                    PropagationContext::UnitPropagation(cid, cached, flip_watches, cache) => {
+                        if flip_watches {
+                            cdb.swap_watch(cid);
+                        }
+                        cdb.transform_by_restoring_watch_cache(propagating, &mut source, cache);
+                        debug_assert_eq!(cdb[cid].lit0(), cached);
+                        debug_assert_eq!(self.assigned(cached), None);
+                        // debug_assert!(other_watch_value.is_none());
+                        self.assign_by_implication(cached, AssignReason::Implication(cid));
+                        check_in!(cid, Propagate::BecameUnit(self.num_conflict, cached));
+                    }
+                    PropagationContext::UpdateWatch(cid, new_watch, k, false_watch_pos) => {
+                        cdb.detach_watch_cache(propagating, &mut source);
+                        cdb.transform_by_updating_watch(cid, false_watch_pos, k, true);
+                        cdb[cid].search_from = (k + 1) as u16;
+                        debug_assert_ne!(self.assigned(new_watch), Some(true));
+                        check_in!(
+                            cid,
+                            Propagate::FindNewWatch(self.num_conflict, propagating, new_watch)
+                        );
+                    }
+                }
+            }
+            from_saved_trail!();
+        }
+        let na = self.q_head + self.num_eliminated_vars + self.num_asserted_vars;
+        if self.num_best_assign <= na && 0 < dl {
+            self.best_assign = true;
+            self.num_best_assign = na;
+        }
+        Ok(())
+    }
+    // NOTE: doesn't support chronoBT
+    fn build_propagatation_context(
+        &self,
+        false_lit: Lit,
+        cid: ClauseId,
+        c: &Clause,
+        mut cached: Lit,
+    ) -> PropagationContext {
+        #[cfg(feature = "boundary_check")]
+        debug_assert!(
+            !cdb[cid].is_dead(),
+            "dead clause in propagation: {:?}",
+            cdb.is_garbage_collected(cid),
+        );
+        debug_assert!(!self.var[cached.vi()].is(FlagVar::ELIMINATED));
+        #[cfg(feature = "maintain_watch_cache")]
+        debug_assert!(
+            cached == cdb[cid].lit0() || cached == cdb[cid].lit1(),
+            "mismatch watch literal and its cache {}: l0 {}  l1 {}, timestamp: {:?}",
+            cached,
+            cdb[cid].lit0(),
+            cdb[cid].lit1(),
+            cdb[cid].timestamp(),
+        );
+        // assert_ne!(other_watch.vi(), false_lit.vi());
+        // assert!(other_watch == cdb[cid].lit0() || other_watch == cdb[cid].lit1());
+        let mut other_watch_value = lit_assign!(self, cached);
+        let mut updated_cache: Option<Lit> = None;
+        if Some(true) == other_watch_value {
+            #[cfg(feature = "maintain_watch_cache")]
+            debug_assert!(cdb[cid].lit0() == cached || cdb[cid].lit1() == cached);
+
+            // In this path, we use only `AssignStack::assign`.
+            // assert!(w.blocker == cdb[w.c].lits[0] || w.blocker == cdb[w.c].lits[1]);
+
+            // FIXME:
+            // cdb.transform_by_restoring_watch_cache(propagating, &mut source, None);
+            // check_in!(cid, Propagate::CacheSatisfied(self.num_conflict));
+            // continue 'next_clause;
+            return PropagationContext::Satisfied(cid);
+        }
+
+        // let c = &cdb[cid];
+        let lit0 = c.lit0();
+        let lit1 = c.lit1();
+        let (false_watch_pos, other) = if false_lit == lit1 {
+            (1, lit0)
+        } else {
+            (0, lit1)
+        };
+
+        if cached != other {
+            cached = other;
+            other_watch_value = lit_assign!(self, other);
+            if Some(true) == other_watch_value {
+                debug_assert!(!self.var[other.vi()].is(FlagVar::ELIMINATED));
+                // In this path, we use only `AssignStack::assign`.
+
+                // FIXME:
+                // cdb.transform_by_restoring_watch_cache(propagating, &mut source, Some(other));
+                // check_in!(cid, Propagate::CacheSatisfied(self.num_conflict));
+                // continue 'next_clause;
+                return PropagationContext::Satisfied(cid);
+            }
+            updated_cache = Some(other);
+        }
+        // let c = &cdb[cid];
+        // debug_assert!(lit0 == false_lit || lit1 == false_lit);
+        //
+        //## Search an un-falsified literal
+        //
+        // Gathering good literals at the beginning of lits.
+        let start = c.search_from;
+        for (k, lk) in c
+            .iter()
+            .enumerate()
+            .skip(start as usize)
+            .chain(c.iter().enumerate().skip(2).take(start as usize - 2))
+        {
+            if lit_assign!(self, *lk) != Some(false) {
+                let new_watch = !*lk;
+                // FIXME:
+                // cdb.detach_watch_cache(propagating, &mut source);
+                // cdb.transform_by_updating_watch(cid, false_watch_pos, k, true);
+                // cdb[cid].search_from = (k + 1) as u16;
+                // debug_assert_ne!(self.assigned(new_watch), Some(true));
+                // check_in!(
+                //     cid,
+                //     Propagate::FindNewWatch(self.num_conflict, propagating, new_watch)
+                // );
+                // continue 'next_clause;
+                return PropagationContext::UpdateWatch(cid, new_watch, k, false_watch_pos);
+            }
+        }
+        // if false_watch_pos == 0 {
+        //     cdb.swap_watch(cid);
+        // }
+
+        // FIXME:
+        // cdb.transform_by_restoring_watch_cache(propagating, &mut source, updated_cache);
+        if other_watch_value == Some(false) {
+            // FIXME:
+            // check_in!(cid, Propagate::EmitConflict(self.num_conflict + 1, cached));
+            // conflict_path!(cached, AssignReason::Implication(cid));
+            return PropagationContext::Conflict(cid, false_watch_pos == 0, updated_cache);
+        }
+
+        // debug_assert_eq!(cdb[cid].lit0(), cached);
+        debug_assert_eq!(self.assigned(cached), None);
+        debug_assert!(other_watch_value.is_none());
+
+        // FIXME:
+        // self.assign_by_implication(
+        //     cached,
+        //     AssignReason::Implication(cid),
+        //     #[cfg(feature = "chrono_BT")]
+        //     dl,
+        // );
+        // check_in!(cid, Propagate::BecameUnit(self.num_conflict, cached));
+        // from_saved_trail!();
+
+        PropagationContext::UnitPropagation(cid, cached, false_watch_pos == 0, updated_cache)
+    }
+
     #[allow(dead_code)]
     fn check(&self, (b0, b1): (Lit, Lit)) {
         assert_ne!(self.assigned(b0), Some(false));

From c19bde9c32fafe480b92d419f562b07aa28743f5 Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Sun, 16 Apr 2023 03:03:09 +0900
Subject: [PATCH 07/19] fix conversion bugs

---
 src/assign/propagate.rs | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

diff --git a/src/assign/propagate.rs b/src/assign/propagate.rs
index e2d30a7a3..80d4fceda 100644
--- a/src/assign/propagate.rs
+++ b/src/assign/propagate.rs
@@ -112,8 +112,8 @@ macro_rules! unset_assign {
 }
 
 enum PropagationContext {
-    Conflict(ClauseId, bool, Option<Lit>),
-    Satisfied(ClauseId),
+    Conflict(ClauseId, Lit, bool, Option<Lit>),
+    Satisfied(ClauseId, Option<Lit>),
     UnitPropagation(ClauseId, Lit, bool, Option<Lit>),
     UpdateWatch(ClauseId, Lit, usize, usize),
 }
@@ -333,10 +333,10 @@ 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_p(&mut self, cdb: &mut impl ClauseDBIF) -> PropagationResult {
+    fn propagate(&mut self, cdb: &mut impl ClauseDBIF) -> PropagationResult {
         self.propagate_parallel(cdb)
     }
-    fn propagate(&mut self, cdb: &mut impl ClauseDBIF) -> PropagationResult {
+    fn propagate_p(&mut self, cdb: &mut impl ClauseDBIF) -> PropagationResult {
         #[cfg(feature = "boundary_check")]
         macro_rules! check_in {
             ($cid: expr, $tag :expr) => {
@@ -886,7 +886,7 @@ impl AssignStack {
             {
                 let c = &cdb[cid];
                 match self.build_propagatation_context(false_lit, cid, c, cached) {
-                    PropagationContext::Conflict(cid, flip_watches, cache) => {
+                    PropagationContext::Conflict(cid, cached, flip_watches, cache) => {
                         if flip_watches {
                             cdb.swap_watch(cid);
                         }
@@ -894,9 +894,9 @@ impl AssignStack {
                         check_in!(cid, Propagate::EmitConflict(self.num_conflict + 1, cached));
                         conflict_path!(cached, AssignReason::Implication(cid));
                     }
-                    PropagationContext::Satisfied(_cid) => {
+                    PropagationContext::Satisfied(_cid, cached) => {
                         // The following doesn't need an ID but the internal pointer in the iterator
-                        cdb.transform_by_restoring_watch_cache(propagating, &mut source, None);
+                        cdb.transform_by_restoring_watch_cache(propagating, &mut source, cached);
                         check_in!(cid, Propagate::CacheSatisfied(self.num_conflict));
                     }
                     PropagationContext::UnitPropagation(cid, cached, flip_watches, cache) => {
@@ -970,7 +970,7 @@ impl AssignStack {
             // cdb.transform_by_restoring_watch_cache(propagating, &mut source, None);
             // check_in!(cid, Propagate::CacheSatisfied(self.num_conflict));
             // continue 'next_clause;
-            return PropagationContext::Satisfied(cid);
+            return PropagationContext::Satisfied(cid, updated_cache);
         }
 
         // let c = &cdb[cid];
@@ -985,6 +985,7 @@ impl AssignStack {
         if cached != other {
             cached = other;
             other_watch_value = lit_assign!(self, other);
+            updated_cache = Some(other);
             if Some(true) == other_watch_value {
                 debug_assert!(!self.var[other.vi()].is(FlagVar::ELIMINATED));
                 // In this path, we use only `AssignStack::assign`.
@@ -993,9 +994,8 @@ impl AssignStack {
                 // cdb.transform_by_restoring_watch_cache(propagating, &mut source, Some(other));
                 // check_in!(cid, Propagate::CacheSatisfied(self.num_conflict));
                 // continue 'next_clause;
-                return PropagationContext::Satisfied(cid);
+                return PropagationContext::Satisfied(cid, updated_cache);
             }
-            updated_cache = Some(other);
         }
         // let c = &cdb[cid];
         // debug_assert!(lit0 == false_lit || lit1 == false_lit);
@@ -1035,7 +1035,7 @@ impl AssignStack {
             // FIXME:
             // check_in!(cid, Propagate::EmitConflict(self.num_conflict + 1, cached));
             // conflict_path!(cached, AssignReason::Implication(cid));
-            return PropagationContext::Conflict(cid, false_watch_pos == 0, updated_cache);
+            return PropagationContext::Conflict(cid, cached, false_watch_pos == 0, updated_cache);
         }
 
         // debug_assert_eq!(cdb[cid].lit0(), cached);

From 898729111453174809c7101c086bbd8f06192386 Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Sun, 16 Apr 2023 09:00:43 +0900
Subject: [PATCH 08/19] redesign `WatchCacheIterator::{next, current}`;
 `transform_by_updating_watch` updates `start_from`

---
 src/assign/propagate.rs |  7 ++-----
 src/cdb/db.rs           |  2 +-
 src/cdb/watch_cache.rs  | 12 +++++++++++-
 3 files changed, 14 insertions(+), 7 deletions(-)

diff --git a/src/assign/propagate.rs b/src/assign/propagate.rs
index 80d4fceda..ea1557251 100644
--- a/src/assign/propagate.rs
+++ b/src/assign/propagate.rs
@@ -446,7 +446,7 @@ impl PropagateIF for AssignStack {
             //
             let mut source = cdb.watch_cache_iter(propagating);
             'next_clause: while let Some((cid, mut cached)) = source
-                .next()
+                .current()
                 .map(|index| cdb.fetch_watch_cache_entry(propagating, index))
             {
                 #[cfg(feature = "boundary_check")]
@@ -522,7 +522,6 @@ impl PropagateIF for AssignStack {
                             let new_watch = !*lk;
                             cdb.detach_watch_cache(propagating, &mut source);
                             cdb.transform_by_updating_watch(cid, false_watch_pos, k, true);
-                            cdb[cid].search_from = (k + 1) as u16;
                             debug_assert_ne!(self.assigned(new_watch), Some(true));
                             check_in!(
                                 cid,
@@ -643,7 +642,7 @@ impl PropagateIF for AssignStack {
             //
             let mut source = cdb.watch_cache_iter(propagating);
             'next_clause: while let Some((cid, mut cached)) = source
-                .next()
+                .current()
                 .map(|index| cdb.fetch_watch_cache_entry(propagating, index))
             {
                 if cdb[cid].is_dead() {
@@ -696,7 +695,6 @@ impl PropagateIF for AssignStack {
                             let new_watch = !*lk;
                             cdb.detach_watch_cache(propagating, &mut source);
                             cdb.transform_by_updating_watch(cid, false_watch_pos, k, true);
-                            cdb[cid].search_from = (k as u16).saturating_add(1);
                             debug_assert!(
                                 self.assigned(!new_watch) == Some(true)
                                     || self.assigned(!new_watch).is_none()
@@ -913,7 +911,6 @@ impl AssignStack {
                     PropagationContext::UpdateWatch(cid, new_watch, k, false_watch_pos) => {
                         cdb.detach_watch_cache(propagating, &mut source);
                         cdb.transform_by_updating_watch(cid, false_watch_pos, k, true);
-                        cdb[cid].search_from = (k + 1) as u16;
                         debug_assert_ne!(self.assigned(new_watch), Some(true));
                         check_in!(
                             cid,
diff --git a/src/cdb/db.rs b/src/cdb/db.rs
index 26c7e96d1..3be96bd1d 100644
--- a/src/cdb/db.rs
+++ b/src/cdb/db.rs
@@ -922,7 +922,7 @@ impl ClauseDBIF for ClauseDB {
         }
 
         c.lits.swap(old, new);
-
+        c.search_from = (new + 1) as u16;
         // maintain_watch_literal \\ assert!(watch_cache[!c.lits[0]].iter().any(|wc| wc.0 == cid && wc.1 == c.lits[1]));
         // maintain_watch_literal \\ assert!(watch_cache[!c.lits[1]].iter().any(|wc| wc.0 == cid && wc.1 == c.lits[0]));
     }
diff --git a/src/cdb/watch_cache.rs b/src/cdb/watch_cache.rs
index 87c2b1e2a..d330f7981 100644
--- a/src/cdb/watch_cache.rs
+++ b/src/cdb/watch_cache.rs
@@ -96,6 +96,7 @@ impl IndexMut<Lit> for Vec<WatchCache> {
 
 pub type WatchCacheProxy = usize;
 
+#[derive(Clone, Debug)]
 pub struct WatchCacheIterator {
     pub index: usize,
     end_at: usize,
@@ -109,7 +110,9 @@ impl Iterator for WatchCacheIterator {
         (self.index < self.end_at).then_some({
             // assert!(0 < self.checksum);
             // self.checksum -= 1;
-            self.index
+            let current = self.index;
+            self.index += 1;
+            current
         })
     }
 }
@@ -122,6 +125,13 @@ impl WatchCacheIterator {
             // checksum: len,
         }
     }
+    pub fn current(&mut self) -> Option<WatchCacheProxy> {
+        (self.index < self.end_at).then_some({
+            // assert!(0 < self.checksum);
+            // self.checksum -= 1;
+            self.index
+        })
+    }
     pub fn restore_entry(&mut self) {
         self.index += 1;
     }

From 9500e3b9a93f8995ca8f2c721a89f0da922898d3 Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Sun, 16 Apr 2023 09:07:59 +0900
Subject: [PATCH 09/19] ENBUG by two-phase propagation

---
 src/assign/propagate.rs | 20 +++++++++++++++-----
 1 file changed, 15 insertions(+), 5 deletions(-)

diff --git a/src/assign/propagate.rs b/src/assign/propagate.rs
index ea1557251..fd691c2df 100644
--- a/src/assign/propagate.rs
+++ b/src/assign/propagate.rs
@@ -878,12 +878,22 @@ impl AssignStack {
             //## normal clause loop
             //
             let mut source = cdb.watch_cache_iter(propagating);
-            while let Some((cid, cached)) = source
-                .next()
+            let transformers = source
+                .clone()
                 .map(|index| cdb.fetch_watch_cache_entry(propagating, index))
-            {
-                let c = &cdb[cid];
-                match self.build_propagatation_context(false_lit, cid, c, cached) {
+                .map(|(cid, cached)| {
+                    self.build_propagatation_context(false_lit, cid, &cdb[cid], cached)
+                })
+                .collect::<Vec<PropagationContext>>();
+            // let mut source = cdb.watch_cache_iter(propagating);
+            // while let Some((cid, cached)) = source
+            //     .current()
+            //     .map(|index| cdb.fetch_watch_cache_entry(propagating, index))
+            // {
+            for context in transformers.iter() {
+                match *context {
+                    // let cls = &cdb[cid];
+                    // match self.build_propagatation_context(false_lit, cid, cls, cached) {
                     PropagationContext::Conflict(cid, cached, flip_watches, cache) => {
                         if flip_watches {
                             cdb.swap_watch(cid);

From c28dc2b60e1fcd6c55fcfe81629cd881d1cdb025 Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Sun, 16 Apr 2023 10:21:52 +0900
Subject: [PATCH 10/19] add debug code

---
 src/assign/propagate.rs | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/src/assign/propagate.rs b/src/assign/propagate.rs
index fd691c2df..fe5fc4a1a 100644
--- a/src/assign/propagate.rs
+++ b/src/assign/propagate.rs
@@ -111,6 +111,7 @@ macro_rules! unset_assign {
     };
 }
 
+#[derive(Debug, Eq, PartialEq)]
 enum PropagationContext {
     Conflict(ClauseId, Lit, bool, Option<Lit>),
     Satisfied(ClauseId, Option<Lit>),
@@ -882,6 +883,7 @@ impl AssignStack {
                 .clone()
                 .map(|index| cdb.fetch_watch_cache_entry(propagating, index))
                 .map(|(cid, cached)| {
+                    dbg!(cid);
                     self.build_propagatation_context(false_lit, cid, &cdb[cid], cached)
                 })
                 .collect::<Vec<PropagationContext>>();
@@ -891,10 +893,14 @@ impl AssignStack {
             //     .map(|index| cdb.fetch_watch_cache_entry(propagating, index))
             // {
             for context in transformers.iter() {
+                let index = source.current().unwrap();
+                let x = cdb.fetch_watch_cache_entry(propagating, index).0;
+                dbg!(index, x, &context);
                 match *context {
                     // let cls = &cdb[cid];
                     // match self.build_propagatation_context(false_lit, cid, cls, cached) {
                     PropagationContext::Conflict(cid, cached, flip_watches, cache) => {
+                        assert_eq!(x, cid);
                         if flip_watches {
                             cdb.swap_watch(cid);
                         }
@@ -902,12 +908,14 @@ impl AssignStack {
                         check_in!(cid, Propagate::EmitConflict(self.num_conflict + 1, cached));
                         conflict_path!(cached, AssignReason::Implication(cid));
                     }
-                    PropagationContext::Satisfied(_cid, cached) => {
+                    PropagationContext::Satisfied(cid, cached) => {
+                        assert_eq!(x, cid);
                         // The following doesn't need an ID but the internal pointer in the iterator
                         cdb.transform_by_restoring_watch_cache(propagating, &mut source, cached);
                         check_in!(cid, Propagate::CacheSatisfied(self.num_conflict));
                     }
                     PropagationContext::UnitPropagation(cid, cached, flip_watches, cache) => {
+                        assert_eq!(x, cid);
                         if flip_watches {
                             cdb.swap_watch(cid);
                         }
@@ -919,6 +927,7 @@ impl AssignStack {
                         check_in!(cid, Propagate::BecameUnit(self.num_conflict, cached));
                     }
                     PropagationContext::UpdateWatch(cid, new_watch, k, false_watch_pos) => {
+                        assert_eq!(x, cid);
                         cdb.detach_watch_cache(propagating, &mut source);
                         cdb.transform_by_updating_watch(cid, false_watch_pos, k, true);
                         debug_assert_ne!(self.assigned(new_watch), Some(true));

From dea015ec241b6be532e474240380829172bb2251 Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Sun, 16 Apr 2023 20:42:41 +0900
Subject: [PATCH 11/19] I got it that an implication is a trigger to rebuild
 contexts

---
 src/assign/propagate.rs | 80 +++++++++++++++++++++++++++--------------
 src/cdb/db.rs           | 75 ++++++++++++++++++++++++++++++++++++++
 src/cdb/mod.rs          | 18 ++++++++++
 src/cdb/watch_cache.rs  |  6 +---
 4 files changed, 148 insertions(+), 31 deletions(-)

diff --git a/src/assign/propagate.rs b/src/assign/propagate.rs
index fe5fc4a1a..8f4e18d31 100644
--- a/src/assign/propagate.rs
+++ b/src/assign/propagate.rs
@@ -878,9 +878,8 @@ impl AssignStack {
             //
             //## normal clause loop
             //
-            let mut source = cdb.watch_cache_iter(propagating);
-            let transformers = source
-                .clone()
+            let transformers = cdb
+                .watch_cache_iter(propagating)
                 .map(|index| cdb.fetch_watch_cache_entry(propagating, index))
                 .map(|(cid, cached)| {
                     dbg!(cid);
@@ -892,44 +891,72 @@ impl AssignStack {
             //     .current()
             //     .map(|index| cdb.fetch_watch_cache_entry(propagating, index))
             // {
-            for context in transformers.iter() {
-                let index = source.current().unwrap();
-                let x = cdb.fetch_watch_cache_entry(propagating, index).0;
-                dbg!(index, x, &context);
+            let mut filling_index = 0;
+            for (i, context) in transformers.iter().enumerate() {
                 match *context {
                     // let cls = &cdb[cid];
                     // match self.build_propagatation_context(false_lit, cid, cls, cached) {
-                    PropagationContext::Conflict(cid, cached, flip_watches, cache) => {
-                        assert_eq!(x, cid);
+                    PropagationContext::Conflict(cid, conflicting, flip_watches, cached) => {
                         if flip_watches {
                             cdb.swap_watch(cid);
                         }
-                        cdb.transform_by_restoring_watch_cache(propagating, &mut source, cache);
-                        check_in!(cid, Propagate::EmitConflict(self.num_conflict + 1, cached));
-                        conflict_path!(cached, AssignReason::Implication(cid));
+                        // cdb.transform_by_restoring_watch_cache(propagating, &mut source, cache);
+                        cdb.transform2_by_pushing_watch_cache_back(
+                            propagating,
+                            i,
+                            &mut filling_index,
+                            cached,
+                        );
+                        cdb.transform2_by_resizing_watch_cache_list(propagating, filling_index);
+                        check_in!(
+                            cid,
+                            Propagate::EmitConflict(self.num_conflict + 1, conflicting)
+                        );
+                        conflict_path!(conflicting, AssignReason::Implication(cid));
                     }
-                    PropagationContext::Satisfied(cid, cached) => {
-                        assert_eq!(x, cid);
+                    PropagationContext::Satisfied(_cid, cached) => {
                         // The following doesn't need an ID but the internal pointer in the iterator
-                        cdb.transform_by_restoring_watch_cache(propagating, &mut source, cached);
+                        // cdb.transform_by_restoring_watch_cache(propagating, &mut source, cached);
+                        cdb.transform2_by_pushing_watch_cache_back(
+                            propagating,
+                            i,
+                            &mut filling_index,
+                            cached,
+                        );
                         check_in!(cid, Propagate::CacheSatisfied(self.num_conflict));
                     }
-                    PropagationContext::UnitPropagation(cid, cached, flip_watches, cache) => {
-                        assert_eq!(x, cid);
+                    PropagationContext::UnitPropagation(cid, implicated, flip_watches, cached) => {
                         if flip_watches {
                             cdb.swap_watch(cid);
                         }
-                        cdb.transform_by_restoring_watch_cache(propagating, &mut source, cache);
-                        debug_assert_eq!(cdb[cid].lit0(), cached);
-                        debug_assert_eq!(self.assigned(cached), None);
+                        // cdb.transform_by_restoring_watch_cache(propagating, &mut source, cache);
+                        cdb.transform2_by_pushing_watch_cache_back(
+                            propagating,
+                            i,
+                            &mut filling_index,
+                            cached,
+                        );
+                        debug_assert_eq!(cdb[cid].lit0(), implicated);
+                        debug_assert_eq!(self.assigned(implicated), None);
                         // debug_assert!(other_watch_value.is_none());
-                        self.assign_by_implication(cached, AssignReason::Implication(cid));
+                        self.assign_by_implication(implicated, AssignReason::Implication(cid));
+                        // FIXME
                         check_in!(cid, Propagate::BecameUnit(self.num_conflict, cached));
+                        panic!("We must purge the remains and rebuild context from here.");
                     }
-                    PropagationContext::UpdateWatch(cid, new_watch, k, false_watch_pos) => {
-                        assert_eq!(x, cid);
-                        cdb.detach_watch_cache(propagating, &mut source);
-                        cdb.transform_by_updating_watch(cid, false_watch_pos, k, true);
+                    PropagationContext::UpdateWatch(
+                        cid,
+                        new_watch,
+                        old_watch_pos,
+                        new_watch_pos,
+                    ) => {
+                        // cdb.transform2_by_detaching_from_watch_cache(propagating, i);
+                        cdb.transform2_by_updating_watch_cache(
+                            propagating,
+                            cid,
+                            old_watch_pos,
+                            new_watch_pos,
+                        );
                         debug_assert_ne!(self.assigned(new_watch), Some(true));
                         check_in!(
                             cid,
@@ -938,6 +965,7 @@ impl AssignStack {
                     }
                 }
             }
+            cdb.transform2_by_resizing_watch_cache_list(propagating, filling_index);
             from_saved_trail!();
         }
         let na = self.q_head + self.num_eliminated_vars + self.num_asserted_vars;
@@ -1038,7 +1066,7 @@ impl AssignStack {
                 //     Propagate::FindNewWatch(self.num_conflict, propagating, new_watch)
                 // );
                 // continue 'next_clause;
-                return PropagationContext::UpdateWatch(cid, new_watch, k, false_watch_pos);
+                return PropagationContext::UpdateWatch(cid, new_watch, false_watch_pos, k);
             }
         }
         // if false_watch_pos == 0 {
diff --git a/src/cdb/db.rs b/src/cdb/db.rs
index 3be96bd1d..294461a76 100644
--- a/src/cdb/db.rs
+++ b/src/cdb/db.rs
@@ -483,6 +483,81 @@ impl ClauseDBIF for ClauseDB {
 
         iter.restore_entry();
     }
+    fn transform2_by_updating_watch_cache(
+        &mut self,
+        propagating_lit: Lit,
+        cid: ClauseId,
+        old_watch_index: usize,
+        new_watch_index: usize,
+    ) {
+        //
+        //## Clause transform rules
+        //
+        // There is one case under non maintain_blocker:
+        // 1. one deletion (if not removed), and one insertion of watch caches
+        //
+        // There is one case under maintain_blocker:
+        // 1. one deletion (if not removed), one insertion, and one update
+        //
+        // So the proceduce is
+        // 1. delete an old one                   [Step:1]
+        // 2. insert a new watch                  [Step:2]
+        // 3. update a blocker cach e             [Step:3]
+
+        debug_assert!(!self[cid].is_dead());
+        debug_assert!(old_watch_index < 2);
+        debug_assert!(1 < new_watch_index);
+        let ClauseDB {
+            ref mut clause,
+            ref mut watch_cache,
+            ..
+        } = self;
+        let c = &mut clause[NonZeroU32::get(cid.ordinal) as usize];
+
+        //## Step:1 detaching this clause from old wathes's list.
+        // But `transform2_by_resizing_watch_list` will clear it. So nothing needed here.
+
+        //## Step:2
+        // assert!(watch_cache[!c.lits[new]].iter().all(|e| e.0 != cid));
+        watch_cache[!c.lits[new_watch_index]].insert_watch(cid, propagating_lit);
+
+        #[cfg(feature = "maintain_watch_cache")]
+        {
+            //## Step:3
+            watch_cache[!c.lits[another]].update_watch(cid, c.lits[new_watch_index]);
+        }
+
+        c.lits.swap(old_watch_index, new_watch_index);
+        c.search_from = (new_watch_index + 1) as u16;
+        // maintain_watch_literal \\ assert!(watch_cache[!c.lits[0]].iter().any(|wc| wc.0 == cid && wc.1 == c.lits[1]));
+        // maintain_watch_literal \\ assert!(watch_cache[!c.lits[1]].iter().any(|wc| wc.0 == cid && wc.1 == c.lits[0]));
+    }
+    fn transform2_by_pushing_watch_cache_back(
+        &mut self,
+        l: Lit,
+        from: usize,
+        to: &mut usize,
+        op: Option<Lit>,
+    ) {
+        self.watch_cache[l][*to] = self.watch_cache[l][from];
+
+        if let Some(p) = op {
+            self.watch_cache[l][*to].1 = p;
+        }
+
+        // let cid = self.watch_cache[l][iter.index].0;
+        // let c = &self[cid];
+        // let l0 = c.lits[0];
+        // let l1 = c.lits[1];
+        // assert!(self.watch_cache[!l0].iter().any(|wc| wc.0 == cid && wc.1 == l1));
+        // assert!(self.watch_cache[!l1].iter().any(|wc| wc.0 == cid && wc.1 == l0));
+
+        *to += 1;
+    }
+    fn transform2_by_resizing_watch_cache_list(&mut self, l: Lit, to: usize) {
+        debug_assert!(to <= self.watch_cache[l].len());
+        self.watch_cache[l].resize(to, (ClauseId::default(), Lit::from(0)));
+    }
     // return a Lit if the clause becomes a unit clause.
     fn transform_by_elimination(&mut self, cid: ClauseId, p: Lit) -> RefClause {
         //
diff --git a/src/cdb/mod.rs b/src/cdb/mod.rs
index de9a6da73..552db4eae 100644
--- a/src/cdb/mod.rs
+++ b/src/cdb/mod.rs
@@ -117,6 +117,24 @@ pub trait ClauseDBIF:
         iter: &mut WatchCacheIterator,
         p: Option<Lit>,
     );
+    /// FIXME:
+    fn transform2_by_updating_watch_cache(
+        &mut self,
+        propagating_lit: Lit,
+        cid: ClauseId,
+        old_watch_index: usize,
+        new_watch_index: usize,
+    );
+    /// FIXME: rayon_propagate
+    fn transform2_by_pushing_watch_cache_back(
+        &mut self,
+        l: Lit,
+        from: usize,
+        to: &mut usize,
+        op: Option<Lit>,
+    );
+    /// FIXME:
+    fn transform2_by_resizing_watch_cache_list(&mut self, l: Lit, to: usize);
     /// swap i-th watch with j-th literal then update watch caches correctly
     fn transform_by_updating_watch(&mut self, cid: ClauseId, old: usize, new: usize, removed: bool);
     /// allocate a new clause and return its id.
diff --git a/src/cdb/watch_cache.rs b/src/cdb/watch_cache.rs
index d330f7981..577a2216c 100644
--- a/src/cdb/watch_cache.rs
+++ b/src/cdb/watch_cache.rs
@@ -126,11 +126,7 @@ impl WatchCacheIterator {
         }
     }
     pub fn current(&mut self) -> Option<WatchCacheProxy> {
-        (self.index < self.end_at).then_some({
-            // assert!(0 < self.checksum);
-            // self.checksum -= 1;
-            self.index
-        })
+        (self.index < self.end_at).then_some(self.index)
     }
     pub fn restore_entry(&mut self) {
         self.index += 1;

From 9c2ffcd1af683754d2a18b022aff3c05eac17753 Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Mon, 17 Apr 2023 20:59:55 +0900
Subject: [PATCH 12/19] a snapshot that works

---
 src/assign/propagate.rs | 196 +++++++++++++++++++++++-----------------
 src/cdb/db.rs           |  73 ++++++++++++---
 src/cdb/mod.rs          |  10 ++
 src/cdb/watch_cache.rs  |   8 ++
 4 files changed, 189 insertions(+), 98 deletions(-)

diff --git a/src/assign/propagate.rs b/src/assign/propagate.rs
index 8f4e18d31..4986ae2eb 100644
--- a/src/assign/propagate.rs
+++ b/src/assign/propagate.rs
@@ -112,7 +112,7 @@ macro_rules! unset_assign {
 }
 
 #[derive(Debug, Eq, PartialEq)]
-enum PropagationContext {
+enum Transformation {
     Conflict(ClauseId, Lit, bool, Option<Lit>),
     Satisfied(ClauseId, Option<Lit>),
     UnitPropagation(ClauseId, Lit, bool, Option<Lit>),
@@ -878,92 +878,115 @@ impl AssignStack {
             //
             //## normal clause loop
             //
-            let transformers = cdb
-                .watch_cache_iter(propagating)
-                .map(|index| cdb.fetch_watch_cache_entry(propagating, index))
-                .map(|(cid, cached)| {
-                    dbg!(cid);
-                    self.build_propagatation_context(false_lit, cid, &cdb[cid], cached)
-                })
-                .collect::<Vec<PropagationContext>>();
-            // let mut source = cdb.watch_cache_iter(propagating);
-            // while let Some((cid, cached)) = source
-            //     .current()
-            //     .map(|index| cdb.fetch_watch_cache_entry(propagating, index))
-            // {
+            let mut start = 0;
             let mut filling_index = 0;
-            for (i, context) in transformers.iter().enumerate() {
-                match *context {
-                    // let cls = &cdb[cid];
-                    // match self.build_propagatation_context(false_lit, cid, cls, cached) {
-                    PropagationContext::Conflict(cid, conflicting, flip_watches, cached) => {
-                        if flip_watches {
-                            cdb.swap_watch(cid);
+            'new_context: while start < cdb.watcher_list_len(propagating) {
+                let transformers = cdb
+                    .watch_cache_iter(propagating)
+                    .skip(start)
+                    .take(1)
+                    .map(|index| cdb.fetch_watch_cache_entry(propagating, index))
+                    .map(|(cid, cached)| {
+                        self.build_propagatation_context(false_lit, cid, &cdb[cid], cached)
+                    })
+                    .collect::<Vec<Transformation>>();
+                // let mut source = cdb.watch_cache_iter(propagating);
+                // while let Some((cid, cached)) = source
+                //     .current()
+                //     .map(|index| cdb.fetch_watch_cache_entry(propagating, index))
+                // {
+                for (i, context) in transformers.iter().enumerate() {
+                    match *context {
+                        // let cls = &cdb[cid];
+                        // match self.build_propagatation_context(false_lit, cid, cls, cached) {
+                        Transformation::Conflict(cid, conflicting, flip_watches, cached) => {
+                            if flip_watches {
+                                cdb.swap_watch(cid);
+                            }
+                            // cdb.transform_by_restoring_watch_cache(propagating, &mut source, cache);
+                            cdb.transform2_by_pushing_watch_cache_back(
+                                propagating,
+                                start + i,
+                                &mut filling_index,
+                                cached,
+                            );
+                            // FIXME: Now watcher_list is 'propagated ... garbage ... remain ...'.
+                            // We need to transform it to 'propagated ... remain ...'.
+                            // So here is a new function:
+                            cdb.transform2_by_folding_watch_cache_list(
+                                propagating,
+                                filling_index,
+                                start + i + 1,
+                            );
+                            check_in!(
+                                cid,
+                                Propagate::EmitConflict(self.num_conflict + 1, conflicting)
+                            );
+                            conflict_path!(conflicting, AssignReason::Implication(cid));
                         }
-                        // cdb.transform_by_restoring_watch_cache(propagating, &mut source, cache);
-                        cdb.transform2_by_pushing_watch_cache_back(
-                            propagating,
-                            i,
-                            &mut filling_index,
-                            cached,
-                        );
-                        cdb.transform2_by_resizing_watch_cache_list(propagating, filling_index);
-                        check_in!(
-                            cid,
-                            Propagate::EmitConflict(self.num_conflict + 1, conflicting)
-                        );
-                        conflict_path!(conflicting, AssignReason::Implication(cid));
-                    }
-                    PropagationContext::Satisfied(_cid, cached) => {
-                        // The following doesn't need an ID but the internal pointer in the iterator
-                        // cdb.transform_by_restoring_watch_cache(propagating, &mut source, cached);
-                        cdb.transform2_by_pushing_watch_cache_back(
-                            propagating,
-                            i,
-                            &mut filling_index,
-                            cached,
-                        );
-                        check_in!(cid, Propagate::CacheSatisfied(self.num_conflict));
-                    }
-                    PropagationContext::UnitPropagation(cid, implicated, flip_watches, cached) => {
-                        if flip_watches {
-                            cdb.swap_watch(cid);
+                        Transformation::Satisfied(_cid, cached) => {
+                            // The following doesn't need an ID but the internal pointer in the iterator
+                            // cdb.transform_by_restoring_watch_cache(propagating, &mut source, cached);
+                            cdb.transform2_by_pushing_watch_cache_back(
+                                propagating,
+                                start + i,
+                                &mut filling_index,
+                                cached,
+                            );
+                            check_in!(cid, Propagate::CacheSatisfied(self.num_conflict));
                         }
-                        // cdb.transform_by_restoring_watch_cache(propagating, &mut source, cache);
-                        cdb.transform2_by_pushing_watch_cache_back(
-                            propagating,
-                            i,
-                            &mut filling_index,
-                            cached,
-                        );
-                        debug_assert_eq!(cdb[cid].lit0(), implicated);
-                        debug_assert_eq!(self.assigned(implicated), None);
-                        // debug_assert!(other_watch_value.is_none());
-                        self.assign_by_implication(implicated, AssignReason::Implication(cid));
-                        // FIXME
-                        check_in!(cid, Propagate::BecameUnit(self.num_conflict, cached));
-                        panic!("We must purge the remains and rebuild context from here.");
-                    }
-                    PropagationContext::UpdateWatch(
-                        cid,
-                        new_watch,
-                        old_watch_pos,
-                        new_watch_pos,
-                    ) => {
-                        // cdb.transform2_by_detaching_from_watch_cache(propagating, i);
-                        cdb.transform2_by_updating_watch_cache(
-                            propagating,
+                        Transformation::UnitPropagation(cid, implicated, flip_watches, cached) => {
+                            if flip_watches {
+                                cdb.swap_watch(cid);
+                            }
+                            // cdb.transform_by_restoring_watch_cache(propagating, &mut source, cache);
+                            cdb.transform2_by_pushing_watch_cache_back(
+                                propagating,
+                                start + i,
+                                &mut filling_index,
+                                cached,
+                            );
+                            debug_assert_eq!(cdb[cid].lit0(), implicated);
+                            debug_assert_eq!(self.assigned(implicated), None);
+                            // debug_assert!(other_watch_value.is_none());
+                            self.assign_by_implication(implicated, AssignReason::Implication(cid));
+                            // FIXME
+                            check_in!(cid, Propagate::BecameUnit(self.num_conflict, cached));
+                            // panic!("We must purge the remains and rebuild context from here.");
+                            start += i + 1;
+                            continue 'new_context;
+                        }
+                        Transformation::UpdateWatch(
                             cid,
+                            new_watch,
                             old_watch_pos,
                             new_watch_pos,
-                        );
-                        debug_assert_ne!(self.assigned(new_watch), Some(true));
-                        check_in!(
-                            cid,
-                            Propagate::FindNewWatch(self.num_conflict, propagating, new_watch)
-                        );
+                        ) => {
+                            {
+                                let c = &cdb[cid];
+                                let w1 = c[0];
+                                let w2 = c[1];
+                                // let old = c[old_watch_pos];
+                                let new = c[new_watch_pos];
+                                debug_assert_ne!(w1, new);
+                                debug_assert_ne!(w2, new);
+                            }
+                            // cdb.transform2_by_detaching_from_watch_cache(propagating, i);
+                            cdb.transform2_by_updating_watch_cache(
+                                propagating,
+                                cid,
+                                old_watch_pos,
+                                new_watch_pos,
+                            );
+                            debug_assert_ne!(self.assigned(new_watch), Some(true));
+                            check_in!(
+                                cid,
+                                Propagate::FindNewWatch(self.num_conflict, propagating, new_watch)
+                            );
+                        }
                     }
                 }
+                start += transformers.len();
             }
             cdb.transform2_by_resizing_watch_cache_list(propagating, filling_index);
             from_saved_trail!();
@@ -982,7 +1005,7 @@ impl AssignStack {
         cid: ClauseId,
         c: &Clause,
         mut cached: Lit,
-    ) -> PropagationContext {
+    ) -> Transformation {
         #[cfg(feature = "boundary_check")]
         debug_assert!(
             !cdb[cid].is_dead(),
@@ -1014,7 +1037,7 @@ impl AssignStack {
             // cdb.transform_by_restoring_watch_cache(propagating, &mut source, None);
             // check_in!(cid, Propagate::CacheSatisfied(self.num_conflict));
             // continue 'next_clause;
-            return PropagationContext::Satisfied(cid, updated_cache);
+            return Transformation::Satisfied(cid, updated_cache);
         }
 
         // let c = &cdb[cid];
@@ -1038,7 +1061,7 @@ impl AssignStack {
                 // cdb.transform_by_restoring_watch_cache(propagating, &mut source, Some(other));
                 // check_in!(cid, Propagate::CacheSatisfied(self.num_conflict));
                 // continue 'next_clause;
-                return PropagationContext::Satisfied(cid, updated_cache);
+                return Transformation::Satisfied(cid, updated_cache);
             }
         }
         // let c = &cdb[cid];
@@ -1066,7 +1089,10 @@ impl AssignStack {
                 //     Propagate::FindNewWatch(self.num_conflict, propagating, new_watch)
                 // );
                 // continue 'next_clause;
-                return PropagationContext::UpdateWatch(cid, new_watch, false_watch_pos, k);
+                debug_assert!(1 < k);
+                debug_assert_ne!(new_watch, lit0);
+                debug_assert_ne!(new_watch, lit1);
+                return Transformation::UpdateWatch(cid, new_watch, false_watch_pos, k);
             }
         }
         // if false_watch_pos == 0 {
@@ -1079,7 +1105,7 @@ impl AssignStack {
             // FIXME:
             // check_in!(cid, Propagate::EmitConflict(self.num_conflict + 1, cached));
             // conflict_path!(cached, AssignReason::Implication(cid));
-            return PropagationContext::Conflict(cid, cached, false_watch_pos == 0, updated_cache);
+            return Transformation::Conflict(cid, cached, false_watch_pos == 0, updated_cache);
         }
 
         // debug_assert_eq!(cdb[cid].lit0(), cached);
@@ -1096,7 +1122,7 @@ impl AssignStack {
         // check_in!(cid, Propagate::BecameUnit(self.num_conflict, cached));
         // from_saved_trail!();
 
-        PropagationContext::UnitPropagation(cid, cached, false_watch_pos == 0, updated_cache)
+        Transformation::UnitPropagation(cid, cached, false_watch_pos == 0, updated_cache)
     }
 
     #[allow(dead_code)]
diff --git a/src/cdb/db.rs b/src/cdb/db.rs
index 294461a76..feb18b386 100644
--- a/src/cdb/db.rs
+++ b/src/cdb/db.rs
@@ -227,6 +227,9 @@ impl ClauseDBIF for ClauseDB {
         self.binary_link.connect_with(l)
     }
     // watch_cache_IF
+    fn watcher_list_len(&self, lit: Lit) -> usize {
+        self.watch_cache[lit].len()
+    }
     fn fetch_watch_cache_entry(&self, lit: Lit, wix: WatchCacheProxy) -> (ClauseId, Lit) {
         self.watch_cache[lit][wix]
     }
@@ -513,18 +516,20 @@ impl ClauseDBIF for ClauseDB {
             ..
         } = self;
         let c = &mut clause[NonZeroU32::get(cid.ordinal) as usize];
+        let another_watch = c.lits[(old_watch_index == 0) as usize];
 
         //## Step:1 detaching this clause from old wathes's list.
         // But `transform2_by_resizing_watch_list` will clear it. So nothing needed here.
+        debug_assert_eq!(propagating_lit, !c.lits[old_watch_index]);
 
         //## Step:2
         // assert!(watch_cache[!c.lits[new]].iter().all(|e| e.0 != cid));
-        watch_cache[!c.lits[new_watch_index]].insert_watch(cid, propagating_lit);
+        watch_cache[!c.lits[new_watch_index]].insert_watch(cid, another_watch);
 
         #[cfg(feature = "maintain_watch_cache")]
         {
             //## Step:3
-            watch_cache[!c.lits[another]].update_watch(cid, c.lits[new_watch_index]);
+            watch_cache[!c.lits[another_watch]].update_watch(cid, c.lits[new_watch_index]);
         }
 
         c.lits.swap(old_watch_index, new_watch_index);
@@ -539,25 +544,67 @@ impl ClauseDBIF for ClauseDB {
         to: &mut usize,
         op: Option<Lit>,
     ) {
-        self.watch_cache[l][*to] = self.watch_cache[l][from];
-
         if let Some(p) = op {
-            self.watch_cache[l][*to].1 = p;
+            assert_ne!(p, l);
+            self.watch_cache[l][from].1 = p;
         }
+        self.watch_cache[l][*to] = self.watch_cache[l][from];
 
-        // let cid = self.watch_cache[l][iter.index].0;
-        // let c = &self[cid];
-        // let l0 = c.lits[0];
-        // let l1 = c.lits[1];
-        // assert!(self.watch_cache[!l0].iter().any(|wc| wc.0 == cid && wc.1 == l1));
-        // assert!(self.watch_cache[!l1].iter().any(|wc| wc.0 == cid && wc.1 == l0));
-
+        {
+            // self.watch_cache[l][from].0 = ClauseId::default();
+            let cid = self.watch_cache[l][*to].0;
+            let c = &self[cid];
+            let l0 = c.lits[0];
+            let l1 = c.lits[1];
+            debug_assert!(self.watch_cache[!l0]
+                .iter()
+                .any(|wc| wc.0 == cid && wc.1 != l0));
+            debug_assert!(self.watch_cache[!l1]
+                .iter()
+                .any(|wc| wc.0 == cid && wc.1 != l1));
+            // if !(self.watch_cache[!l0]
+            //     .iter()
+            //     .any(|wc| wc.0 == cid && wc.1 == l1))
+            // {
+            //     println!(
+            //         "{cid}: {c:?}, {l0}, {l1}, propagating: {l}, watch on !{l0} contains {:?}, op: {op:?}",
+            //         self.watch_cache[!l0]
+            //             .iter()
+            //             .filter(|wc| wc.0 == cid)
+            //             .collect::<Vec<_>>(),
+            //     );
+            //     // panic!();
+            // }
+            // assert!(self.watch_cache[!l0]
+            //     .iter()
+            //     .any(|wc| wc.0 == cid && wc.1 == l1));
+            // assert!(self.watch_cache[!l1]
+            //     .iter()
+            //     .any(|wc| wc.0 == cid && wc.1 == l0));
+        }
         *to += 1;
     }
     fn transform2_by_resizing_watch_cache_list(&mut self, l: Lit, to: usize) {
         debug_assert!(to <= self.watch_cache[l].len());
-        self.watch_cache[l].resize(to, (ClauseId::default(), Lit::from(0)));
+        self.watch_cache[l].truncate(to);
     }
+    fn transform2_by_folding_watch_cache_list(
+        &mut self,
+        propagating: Lit,
+        garbage_from: usize,
+        remain_from: usize,
+    ) {
+        let watcher = &mut self.watch_cache[propagating];
+        let len = watcher.len();
+        let mut last = garbage_from;
+        for i in remain_from..len {
+            watcher[last] = watcher[i];
+            last += 1;
+        }
+        assert!(last <= len);
+        watcher.truncate(last);
+    }
+
     // return a Lit if the clause becomes a unit clause.
     fn transform_by_elimination(&mut self, cid: ClauseId, p: Lit) -> RefClause {
         //
diff --git a/src/cdb/mod.rs b/src/cdb/mod.rs
index 552db4eae..d6dbe0f3f 100644
--- a/src/cdb/mod.rs
+++ b/src/cdb/mod.rs
@@ -95,6 +95,8 @@ pub trait ClauseDBIF:
     //## abstraction to watch_cache
     //
 
+    // return the number of clause watching `lit`
+    fn watcher_list_len(&self, lit: Lit) -> usize;
     // get mutable reference to a watch_cache
     fn fetch_watch_cache_entry(&self, lit: Lit, index: WatchCacheProxy) -> (ClauseId, Lit);
     /// replace the mutable watcher list with an empty one, and return the list
@@ -135,6 +137,14 @@ pub trait ClauseDBIF:
     );
     /// FIXME:
     fn transform2_by_resizing_watch_cache_list(&mut self, l: Lit, to: usize);
+    /// FIXME:
+    fn transform2_by_folding_watch_cache_list(
+        &mut self,
+        propagating: Lit,
+        garbage_from: usize,
+        remain_from: usize,
+    );
+
     /// swap i-th watch with j-th literal then update watch caches correctly
     fn transform_by_updating_watch(&mut self, cid: ClauseId, old: usize, new: usize, removed: bool);
     /// allocate a new clause and return its id.
diff --git a/src/cdb/watch_cache.rs b/src/cdb/watch_cache.rs
index 577a2216c..c1afaa64f 100644
--- a/src/cdb/watch_cache.rs
+++ b/src/cdb/watch_cache.rs
@@ -125,6 +125,14 @@ impl WatchCacheIterator {
             // checksum: len,
         }
     }
+    pub fn skip(mut self, start: usize) -> Self {
+        self.index = start;
+        self
+    }
+    pub fn take(mut self, count: usize) -> Self {
+        self.end_at = self.index + count;
+        self
+    }
     pub fn current(&mut self) -> Option<WatchCacheProxy> {
         (self.index < self.end_at).then_some(self.index)
     }

From 3b07ef48c42bb5317e32f52cf8e7a3e943507c34 Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Sat, 23 Mar 2024 23:39:57 +0900
Subject: [PATCH 13/19] keep a snapshot

---
 src/assign/propagate.rs | 56 +++++++++++++++++++++++++----------------
 src/cdb/db.rs           | 10 +++++++-
 src/cdb/mod.rs          |  1 +
 3 files changed, 45 insertions(+), 22 deletions(-)

diff --git a/src/assign/propagate.rs b/src/assign/propagate.rs
index 4986ae2eb..07fbf70ac 100644
--- a/src/assign/propagate.rs
+++ b/src/assign/propagate.rs
@@ -3,6 +3,7 @@
 use {
     super::{AssignIF, AssignStack, VarHeapIF, VarManipulateIF},
     crate::{cdb::ClauseDBIF, types::*},
+    rayon::prelude::*,
 };
 
 #[cfg(feature = "trail_saving")]
@@ -881,15 +882,29 @@ impl AssignStack {
             let mut start = 0;
             let mut filling_index = 0;
             'new_context: while start < cdb.watcher_list_len(propagating) {
+                // let transformers = cdb
+                //     .watcher_list(propagating)
+                //     .iter()
+                //     .map(|(cid, clause, cached)| {
+                //         self.build_propagatation_context(false_lit, *cid, clause, *cached)
+                //     })
+                //     .collect::<Vec<Transformation>>();
+
                 let transformers = cdb
                     .watch_cache_iter(propagating)
                     .skip(start)
                     .take(1)
                     .map(|index| cdb.fetch_watch_cache_entry(propagating, index))
                     .map(|(cid, cached)| {
-                        self.build_propagatation_context(false_lit, cid, &cdb[cid], cached)
+                        self.build_propagatation_context(
+                            false_lit,
+                            cid,
+                            &cdb[cid].iter().cloned().collect::<Vec<Lit>>(),
+                            cached,
+                        )
                     })
                     .collect::<Vec<Transformation>>();
+
                 // let mut source = cdb.watch_cache_iter(propagating);
                 // while let Some((cid, cached)) = source
                 //     .current()
@@ -1003,32 +1018,31 @@ impl AssignStack {
         &self,
         false_lit: Lit,
         cid: ClauseId,
-        c: &Clause,
+        c: &[Lit],
         mut cached: Lit,
     ) -> Transformation {
-        #[cfg(feature = "boundary_check")]
-        debug_assert!(
-            !cdb[cid].is_dead(),
-            "dead clause in propagation: {:?}",
-            cdb.is_garbage_collected(cid),
-        );
+        // #[cfg(feature = "boundary_check")]
+        // debug_assert!(
+        //     !cdb[cid].is_dead(),
+        //     "dead clause in propagation: {:?}",
+        //     cdb.is_garbage_collected(cid),
+        // );
         debug_assert!(!self.var[cached.vi()].is(FlagVar::ELIMINATED));
-        #[cfg(feature = "maintain_watch_cache")]
-        debug_assert!(
-            cached == cdb[cid].lit0() || cached == cdb[cid].lit1(),
-            "mismatch watch literal and its cache {}: l0 {}  l1 {}, timestamp: {:?}",
-            cached,
-            cdb[cid].lit0(),
-            cdb[cid].lit1(),
-            cdb[cid].timestamp(),
-        );
+        // #[cfg(feature = "maintain_watch_cache")]
+        // debug_assert!(
+        //     cached == cdb[cid].lit0() || cached == cdb[cid].lit1(),
+        //     "mismatch watch literal and its cache {}: l0 {}  l1 {}, timestamp: ?",
+        //     cached,
+        //     c[0],
+        //     c[1],
+        // );
         // assert_ne!(other_watch.vi(), false_lit.vi());
         // assert!(other_watch == cdb[cid].lit0() || other_watch == cdb[cid].lit1());
         let mut other_watch_value = lit_assign!(self, cached);
         let mut updated_cache: Option<Lit> = None;
         if Some(true) == other_watch_value {
             #[cfg(feature = "maintain_watch_cache")]
-            debug_assert!(cdb[cid].lit0() == cached || cdb[cid].lit1() == cached);
+            // debug_assert!(cdb[cid].lit0() == cached || cdb[cid].lit1() == cached);
 
             // In this path, we use only `AssignStack::assign`.
             // assert!(w.blocker == cdb[w.c].lits[0] || w.blocker == cdb[w.c].lits[1]);
@@ -1041,8 +1055,8 @@ impl AssignStack {
         }
 
         // let c = &cdb[cid];
-        let lit0 = c.lit0();
-        let lit1 = c.lit1();
+        let lit0 = c[0];
+        let lit1 = c[1];
         let (false_watch_pos, other) = if false_lit == lit1 {
             (1, lit0)
         } else {
@@ -1070,7 +1084,7 @@ impl AssignStack {
         //## Search an un-falsified literal
         //
         // Gathering good literals at the beginning of lits.
-        let start = c.search_from;
+        let start = 2;
         for (k, lk) in c
             .iter()
             .enumerate()
diff --git a/src/cdb/db.rs b/src/cdb/db.rs
index feb18b386..dc56a2b58 100644
--- a/src/cdb/db.rs
+++ b/src/cdb/db.rs
@@ -227,6 +227,12 @@ impl ClauseDBIF for ClauseDB {
         self.binary_link.connect_with(l)
     }
     // watch_cache_IF
+    fn watcher_list(&self, lit: Lit) -> Vec<(ClauseId, Vec<Lit>, Lit)> {
+        self.watch_cache[lit]
+            .iter()
+            .map(|(cid, lit)| (*cid, self[cid].lits.clone(), *lit))
+            .collect::<Vec<_>>()
+    }
     fn watcher_list_len(&self, lit: Lit) -> usize {
         self.watch_cache[lit].len()
     }
@@ -1326,7 +1332,9 @@ impl ClauseDBIF for ClauseDB {
                 panic!("conflicting var {} {:?}", vi, asg.assign(vi));
             }
         }
-        let Ok(out) = File::create(fname) else { return; };
+        let Ok(out) = File::create(fname) else {
+            return;
+        };
         let mut buf = std::io::BufWriter::new(out);
         let na = asg.derefer(crate::assign::property::Tusize::NumAssertedVar);
         let nc = self.iter().skip(1).filter(|c| !c.is_dead()).count();
diff --git a/src/cdb/mod.rs b/src/cdb/mod.rs
index d6dbe0f3f..0b88ca815 100644
--- a/src/cdb/mod.rs
+++ b/src/cdb/mod.rs
@@ -96,6 +96,7 @@ pub trait ClauseDBIF:
     //
 
     // return the number of clause watching `lit`
+    fn watcher_list(&self, lit: Lit) -> Vec<(ClauseId, Vec<Lit>, Lit)>;
     fn watcher_list_len(&self, lit: Lit) -> usize;
     // get mutable reference to a watch_cache
     fn fetch_watch_cache_entry(&self, lit: Lit, index: WatchCacheProxy) -> (ClauseId, Lit);

From 8912e72f9e533d6124f350516759a78bcd2b2c1c Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Sun, 24 Mar 2024 06:31:15 +0900
Subject: [PATCH 14/19] fix a wrong edit

---
 src/assign/propagate.rs | 34 ++++++++++++++++++----------------
 1 file changed, 18 insertions(+), 16 deletions(-)

diff --git a/src/assign/propagate.rs b/src/assign/propagate.rs
index 07fbf70ac..86f33c1f0 100644
--- a/src/assign/propagate.rs
+++ b/src/assign/propagate.rs
@@ -892,6 +892,8 @@ impl AssignStack {
 
                 let transformers = cdb
                     .watch_cache_iter(propagating)
+                    // .watcher_list(propagating)
+                    // .iter()
                     .skip(start)
                     .take(1)
                     .map(|index| cdb.fetch_watch_cache_entry(propagating, index))
@@ -904,7 +906,6 @@ impl AssignStack {
                         )
                     })
                     .collect::<Vec<Transformation>>();
-
                 // let mut source = cdb.watch_cache_iter(propagating);
                 // while let Some((cid, cached)) = source
                 //     .current()
@@ -1021,28 +1022,29 @@ impl AssignStack {
         c: &[Lit],
         mut cached: Lit,
     ) -> Transformation {
-        // #[cfg(feature = "boundary_check")]
-        // debug_assert!(
-        //     !cdb[cid].is_dead(),
-        //     "dead clause in propagation: {:?}",
-        //     cdb.is_garbage_collected(cid),
-        // );
+        #[cfg(feature = "boundary_check")]
+        debug_assert!(
+            !cdb[cid].is_dead(),
+            "dead clause in propagation: {:?}",
+            cdb.is_garbage_collected(cid),
+        );
         debug_assert!(!self.var[cached.vi()].is(FlagVar::ELIMINATED));
-        // #[cfg(feature = "maintain_watch_cache")]
-        // debug_assert!(
-        //     cached == cdb[cid].lit0() || cached == cdb[cid].lit1(),
-        //     "mismatch watch literal and its cache {}: l0 {}  l1 {}, timestamp: ?",
-        //     cached,
-        //     c[0],
-        //     c[1],
-        // );
+        #[cfg(feature = "maintain_watch_cache")]
+        debug_assert!(
+            cached == cdb[cid].lit0() || cached == cdb[cid].lit1(),
+            "mismatch watch literal and its cache {}: l0 {}  l1 {}, timestamp: ?",
+            cached,
+            cdb[cid].lit0(),
+            cdb[cid].lit1(),
+            cdb[cid].timestamp(),
+        );
         // assert_ne!(other_watch.vi(), false_lit.vi());
         // assert!(other_watch == cdb[cid].lit0() || other_watch == cdb[cid].lit1());
         let mut other_watch_value = lit_assign!(self, cached);
         let mut updated_cache: Option<Lit> = None;
         if Some(true) == other_watch_value {
             #[cfg(feature = "maintain_watch_cache")]
-            // debug_assert!(cdb[cid].lit0() == cached || cdb[cid].lit1() == cached);
+            debug_assert!(cdb[cid].lit0() == cached || cdb[cid].lit1() == cached);
 
             // In this path, we use only `AssignStack::assign`.
             // assert!(w.blocker == cdb[w.c].lits[0] || w.blocker == cdb[w.c].lits[1]);

From 99e9eef039064af86df06ecdc165c20525335957 Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Sun, 24 Mar 2024 07:02:06 +0900
Subject: [PATCH 15/19] (WatchCacheIterator::take) fix wrong boundary
 calculation:   src/cdb/watch_cache.rs

---
 src/cdb/watch_cache.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/cdb/watch_cache.rs b/src/cdb/watch_cache.rs
index c1afaa64f..72130a0b6 100644
--- a/src/cdb/watch_cache.rs
+++ b/src/cdb/watch_cache.rs
@@ -130,7 +130,7 @@ impl WatchCacheIterator {
         self
     }
     pub fn take(mut self, count: usize) -> Self {
-        self.end_at = self.index + count;
+        self.end_at = self.end_at.min(self.index + count);
         self
     }
     pub fn current(&mut self) -> Option<WatchCacheProxy> {

From c6dd0db290f962eaa97077983f567e3bd87aaf34 Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Sun, 24 Mar 2024 07:04:30 +0900
Subject: [PATCH 16/19] The transformer works

---
 src/assign/propagate.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/assign/propagate.rs b/src/assign/propagate.rs
index 86f33c1f0..b681c4ba0 100644
--- a/src/assign/propagate.rs
+++ b/src/assign/propagate.rs
@@ -895,7 +895,7 @@ impl AssignStack {
                     // .watcher_list(propagating)
                     // .iter()
                     .skip(start)
-                    .take(1)
+                    // .take(40)
                     .map(|index| cdb.fetch_watch_cache_entry(propagating, index))
                     .map(|(cid, cached)| {
                         self.build_propagatation_context(

From 804da43a0fdaf77d19ffd69c2a5b2a6d13f6014b Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Sun, 24 Mar 2024 09:40:54 +0900
Subject: [PATCH 17/19] seems to work

---
 src/assign/propagate.rs | 127 ++++++++--------------------------------
 src/cdb/db.rs           |  16 ++---
 src/cdb/mod.rs          |   8 +--
 3 files changed, 38 insertions(+), 113 deletions(-)

diff --git a/src/assign/propagate.rs b/src/assign/propagate.rs
index b681c4ba0..fabae7aeb 100644
--- a/src/assign/propagate.rs
+++ b/src/assign/propagate.rs
@@ -3,7 +3,7 @@
 use {
     super::{AssignIF, AssignStack, VarHeapIF, VarManipulateIF},
     crate::{cdb::ClauseDBIF, types::*},
-    rayon::prelude::*,
+    // rayon::prelude::*,
 };
 
 #[cfg(feature = "trail_saving")]
@@ -882,30 +882,33 @@ impl AssignStack {
             let mut start = 0;
             let mut filling_index = 0;
             'new_context: while start < cdb.watcher_list_len(propagating) {
-                // let transformers = cdb
-                //     .watcher_list(propagating)
-                //     .iter()
-                //     .map(|(cid, clause, cached)| {
-                //         self.build_propagatation_context(false_lit, *cid, clause, *cached)
-                //     })
-                //     .collect::<Vec<Transformation>>();
-
+                // We need to build transformers several times if new unit propagation occur.
                 let transformers = cdb
-                    .watch_cache_iter(propagating)
-                    // .watcher_list(propagating)
-                    // .iter()
-                    .skip(start)
-                    // .take(40)
-                    .map(|index| cdb.fetch_watch_cache_entry(propagating, index))
-                    .map(|(cid, cached)| {
-                        self.build_propagatation_context(
-                            false_lit,
-                            cid,
-                            &cdb[cid].iter().cloned().collect::<Vec<Lit>>(),
-                            cached,
-                        )
+                    .watcher_list(propagating, start, 20)
+                    .iter()
+                    .map(|(cid, clause, cached)| {
+                        self.build_propagatation_context(false_lit, *cid, clause, *cached)
                     })
                     .collect::<Vec<Transformation>>();
+
+                // let transformers_ = cdb
+                //     .watch_cache_iter(propagating)
+                //     .skip(start)
+                //     // .take(40)
+                //     .map(|index| cdb.fetch_watch_cache_entry(propagating, index))
+                //     .map(|(cid, cached)| {
+                //         self.build_propagatation_context(
+                //             false_lit,
+                //             cid,
+                //             &cdb[cid].iter().cloned().collect::<Vec<Lit>>(),
+                //             cached,
+                //         )
+                //     })
+                //     .collect::<Vec<Transformation>>();
+
+                // assert_eq!(transformers.len(), cdb.watcher_list_len(propagating));
+                // assert_eq!(transformers, transformers2);
+
                 // let mut source = cdb.watch_cache_iter(propagating);
                 // while let Some((cid, cached)) = source
                 //     .current()
@@ -1022,41 +1025,11 @@ impl AssignStack {
         c: &[Lit],
         mut cached: Lit,
     ) -> Transformation {
-        #[cfg(feature = "boundary_check")]
-        debug_assert!(
-            !cdb[cid].is_dead(),
-            "dead clause in propagation: {:?}",
-            cdb.is_garbage_collected(cid),
-        );
-        debug_assert!(!self.var[cached.vi()].is(FlagVar::ELIMINATED));
-        #[cfg(feature = "maintain_watch_cache")]
-        debug_assert!(
-            cached == cdb[cid].lit0() || cached == cdb[cid].lit1(),
-            "mismatch watch literal and its cache {}: l0 {}  l1 {}, timestamp: ?",
-            cached,
-            cdb[cid].lit0(),
-            cdb[cid].lit1(),
-            cdb[cid].timestamp(),
-        );
-        // assert_ne!(other_watch.vi(), false_lit.vi());
-        // assert!(other_watch == cdb[cid].lit0() || other_watch == cdb[cid].lit1());
         let mut other_watch_value = lit_assign!(self, cached);
         let mut updated_cache: Option<Lit> = None;
         if Some(true) == other_watch_value {
-            #[cfg(feature = "maintain_watch_cache")]
-            debug_assert!(cdb[cid].lit0() == cached || cdb[cid].lit1() == cached);
-
-            // In this path, we use only `AssignStack::assign`.
-            // assert!(w.blocker == cdb[w.c].lits[0] || w.blocker == cdb[w.c].lits[1]);
-
-            // FIXME:
-            // cdb.transform_by_restoring_watch_cache(propagating, &mut source, None);
-            // check_in!(cid, Propagate::CacheSatisfied(self.num_conflict));
-            // continue 'next_clause;
             return Transformation::Satisfied(cid, updated_cache);
         }
-
-        // let c = &cdb[cid];
         let lit0 = c[0];
         let lit1 = c[1];
         let (false_watch_pos, other) = if false_lit == lit1 {
@@ -1070,22 +1043,9 @@ impl AssignStack {
             other_watch_value = lit_assign!(self, other);
             updated_cache = Some(other);
             if Some(true) == other_watch_value {
-                debug_assert!(!self.var[other.vi()].is(FlagVar::ELIMINATED));
-                // In this path, we use only `AssignStack::assign`.
-
-                // FIXME:
-                // cdb.transform_by_restoring_watch_cache(propagating, &mut source, Some(other));
-                // check_in!(cid, Propagate::CacheSatisfied(self.num_conflict));
-                // continue 'next_clause;
                 return Transformation::Satisfied(cid, updated_cache);
             }
         }
-        // let c = &cdb[cid];
-        // debug_assert!(lit0 == false_lit || lit1 == false_lit);
-        //
-        //## Search an un-falsified literal
-        //
-        // Gathering good literals at the beginning of lits.
         let start = 2;
         for (k, lk) in c
             .iter()
@@ -1095,49 +1055,12 @@ impl AssignStack {
         {
             if lit_assign!(self, *lk) != Some(false) {
                 let new_watch = !*lk;
-                // FIXME:
-                // cdb.detach_watch_cache(propagating, &mut source);
-                // cdb.transform_by_updating_watch(cid, false_watch_pos, k, true);
-                // cdb[cid].search_from = (k + 1) as u16;
-                // debug_assert_ne!(self.assigned(new_watch), Some(true));
-                // check_in!(
-                //     cid,
-                //     Propagate::FindNewWatch(self.num_conflict, propagating, new_watch)
-                // );
-                // continue 'next_clause;
-                debug_assert!(1 < k);
-                debug_assert_ne!(new_watch, lit0);
-                debug_assert_ne!(new_watch, lit1);
                 return Transformation::UpdateWatch(cid, new_watch, false_watch_pos, k);
             }
         }
-        // if false_watch_pos == 0 {
-        //     cdb.swap_watch(cid);
-        // }
-
-        // FIXME:
-        // cdb.transform_by_restoring_watch_cache(propagating, &mut source, updated_cache);
         if other_watch_value == Some(false) {
-            // FIXME:
-            // check_in!(cid, Propagate::EmitConflict(self.num_conflict + 1, cached));
-            // conflict_path!(cached, AssignReason::Implication(cid));
             return Transformation::Conflict(cid, cached, false_watch_pos == 0, updated_cache);
         }
-
-        // debug_assert_eq!(cdb[cid].lit0(), cached);
-        debug_assert_eq!(self.assigned(cached), None);
-        debug_assert!(other_watch_value.is_none());
-
-        // FIXME:
-        // self.assign_by_implication(
-        //     cached,
-        //     AssignReason::Implication(cid),
-        //     #[cfg(feature = "chrono_BT")]
-        //     dl,
-        // );
-        // check_in!(cid, Propagate::BecameUnit(self.num_conflict, cached));
-        // from_saved_trail!();
-
         Transformation::UnitPropagation(cid, cached, false_watch_pos == 0, updated_cache)
     }
 
diff --git a/src/cdb/db.rs b/src/cdb/db.rs
index dc56a2b58..438998832 100644
--- a/src/cdb/db.rs
+++ b/src/cdb/db.rs
@@ -227,10 +227,12 @@ impl ClauseDBIF for ClauseDB {
         self.binary_link.connect_with(l)
     }
     // watch_cache_IF
-    fn watcher_list(&self, lit: Lit) -> Vec<(ClauseId, Vec<Lit>, Lit)> {
+    fn watcher_list(&self, lit: Lit, start: usize, len: usize) -> Vec<(ClauseId, Vec<Lit>, Lit)> {
         self.watch_cache[lit]
             .iter()
-            .map(|(cid, lit)| (*cid, self[cid].lits.clone(), *lit))
+            .skip(start)
+            .take(len)
+            .map(|(cid, l)| (*cid, self[*cid].lits.clone(), *l))
             .collect::<Vec<_>>()
     }
     fn watcher_list_len(&self, lit: Lit) -> usize {
@@ -240,14 +242,14 @@ impl ClauseDBIF for ClauseDB {
         self.watch_cache[lit][wix]
     }
     #[inline]
-    fn watch_cache_iter(&mut self, l: Lit) -> WatchCacheIterator {
+    fn watch_cache_iter(&mut self, lit: Lit) -> WatchCacheIterator {
         // let mut empty = WatchCache::new();
-        // std::mem::swap(&mut self.watch_cache[l], &mut empty);
+        // std::mem::swap(&mut self.watch_cache[lit], &mut empty);
         // empty
-        WatchCacheIterator::new(self.watch_cache[l].len())
+        WatchCacheIterator::new(self.watch_cache[lit].len())
     }
-    fn detach_watch_cache(&mut self, l: Lit, iter: &mut WatchCacheIterator) {
-        self.watch_cache[l].swap_remove(iter.index);
+    fn detach_watch_cache(&mut self, lit: Lit, iter: &mut WatchCacheIterator) {
+        self.watch_cache[lit].swap_remove(iter.index);
         iter.detach_entry();
     }
     fn merge_watch_cache(&mut self, p: Lit, wc: WatchCache) {
diff --git a/src/cdb/mod.rs b/src/cdb/mod.rs
index 0b88ca815..46ffd7a85 100644
--- a/src/cdb/mod.rs
+++ b/src/cdb/mod.rs
@@ -96,16 +96,16 @@ pub trait ClauseDBIF:
     //
 
     // return the number of clause watching `lit`
-    fn watcher_list(&self, lit: Lit) -> Vec<(ClauseId, Vec<Lit>, Lit)>;
+    fn watcher_list(&self, lit: Lit, start: usize, len: usize) -> Vec<(ClauseId, Vec<Lit>, Lit)>;
     fn watcher_list_len(&self, lit: Lit) -> usize;
     // get mutable reference to a watch_cache
     fn fetch_watch_cache_entry(&self, lit: Lit, index: WatchCacheProxy) -> (ClauseId, Lit);
     /// replace the mutable watcher list with an empty one, and return the list
-    fn watch_cache_iter(&mut self, l: Lit) -> WatchCacheIterator;
+    fn watch_cache_iter(&mut self, lit: Lit) -> WatchCacheIterator;
     /// detach the watch_cache referred by the head of a watch_cache iterator
-    fn detach_watch_cache(&mut self, l: Lit, iter: &mut WatchCacheIterator);
+    fn detach_watch_cache(&mut self, lit: Lit, iter: &mut WatchCacheIterator);
     /// Merge two watch cache
-    fn merge_watch_cache(&mut self, l: Lit, wc: WatchCache);
+    fn merge_watch_cache(&mut self, lit: Lit, wc: WatchCache);
     /// swap the first two literals in a clause.
     fn swap_watch(&mut self, cid: ClauseId);
 

From 9866d4bff72ab9a90231846b537732b2cd25c23e Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Mon, 25 Mar 2024 08:48:07 +0900
Subject: [PATCH 18/19] another snapshot

---
 src/assign/propagate.rs | 207 ++++++++++++++++++++++++++--------------
 src/cdb/db.rs           |  25 +++--
 src/cdb/mod.rs          |   3 +-
 3 files changed, 155 insertions(+), 80 deletions(-)

diff --git a/src/assign/propagate.rs b/src/assign/propagate.rs
index fabae7aeb..a8b3505d1 100644
--- a/src/assign/propagate.rs
+++ b/src/assign/propagate.rs
@@ -3,9 +3,11 @@
 use {
     super::{AssignIF, AssignStack, VarHeapIF, VarManipulateIF},
     crate::{cdb::ClauseDBIF, types::*},
-    // rayon::prelude::*,
 };
 
+#[allow(unused_imports)]
+use rayon::prelude::*;
+
 #[cfg(feature = "trail_saving")]
 use super::TrailSavingIF;
 
@@ -883,32 +885,82 @@ impl AssignStack {
             let mut filling_index = 0;
             'new_context: while start < cdb.watcher_list_len(propagating) {
                 // We need to build transformers several times if new unit propagation occur.
-                let transformers = cdb
-                    .watcher_list(propagating, start, 20)
-                    .iter()
-                    .map(|(cid, clause, cached)| {
-                        self.build_propagatation_context(false_lit, *cid, clause, *cached)
-                    })
-                    .collect::<Vec<Transformation>>();
-
-                // let transformers_ = cdb
-                //     .watch_cache_iter(propagating)
-                //     .skip(start)
-                //     // .take(40)
-                //     .map(|index| cdb.fetch_watch_cache_entry(propagating, index))
-                //     .map(|(cid, cached)| {
-                //         self.build_propagatation_context(
-                //             false_lit,
-                //             cid,
-                //             &cdb[cid].iter().cloned().collect::<Vec<Lit>>(),
-                //             cached,
-                //         )
-                //     })
-                //     .collect::<Vec<Transformation>>();
+                const CHUNK_SIZE: usize = 8;
 
+                let transformers = if CHUNK_SIZE * 4 < cdb.watcher_list_len(propagating) - start {
+                    cdb.watcher_list(propagating, start, 0)
+                        .par_iter()
+                        .chunks(CHUNK_SIZE)
+                        .map(|v /* (cid, clause, cached)*/| {
+                            v.iter()
+                                .map(|(cid, clause, cached)| {
+                                    build_propagatation_context(
+                                        &self.assign,
+                                        false_lit,
+                                        *cid,
+                                        clause,
+                                        *cached,
+                                    )
+                                })
+                                .collect::<Vec<_>>()
+                        })
+                        .flatten()
+                        .collect::<Vec<_>>()
+                } else {
+                    cdb.watcher_list(propagating, start, 1)
+                        // cdb.watch_cache_iter(propagating)
+                        .iter()
+                        // .skip(start)
+                        // .take(1)
+                        // .map(|index| cdb.fetch_watch_cache_entry(propagating, index))
+                        .map(|(cid, clause, cached)| {
+                            build_propagatation_context(
+                                &self.assign,
+                                false_lit,
+                                *cid,
+                                // &cdb[cid].iter().cloned().collect::<Vec<Lit>>(),
+                                clause,
+                                *cached,
+                            )
+                        })
+                        .collect::<Vec<Transformation>>()
+                };
                 // assert_eq!(transformers.len(), cdb.watcher_list_len(propagating));
                 // assert_eq!(transformers, transformers2);
 
+                // if let Some((i, Transformation::Conflict(cid, conflicting, flip_watches, cached))) =
+                //     transformers
+                //         .iter()
+                //         .enumerate()
+                //         .find(|(_, e)| matches!(**e, Transformation::Conflict(_, _, _, _)))
+                // {
+                //     // transformers.swap(start, i);
+                //     cdb.watcher_list_swap(propagating, 0, start + i);
+                //     if *flip_watches {
+                //         cdb.swap_watch(*cid);
+                //     }
+                //     // // cdb.transform_by_restoring_watch_cache(propagating, &mut source, cache);
+                //     cdb.transform2_by_pushing_watch_cache_back(
+                //         propagating,
+                //         start + i,
+                //         &mut filling_index,
+                //         *cached,
+                //     );
+                //     // FIXME: Now watcher_list is 'propagated ... garbage ... remain ...'.
+                //     // We need to transform it to 'propagated ... remain ...'.
+                //     // So here is a new function:
+                //     cdb.transform2_by_folding_watch_cache_list(
+                //         propagating,
+                //         filling_index,
+                //         start + i + 1,
+                //     );
+                //     check_in!(
+                //         cid,
+                //         Propagate::EmitConflict(self.num_conflict + 1, conflicting)
+                //     );
+                //     conflict_path!(*conflicting, AssignReason::Implication(*cid));
+                // }
+
                 // let mut source = cdb.watch_cache_iter(propagating);
                 // while let Some((cid, cached)) = source
                 //     .current()
@@ -916,8 +968,6 @@ impl AssignStack {
                 // {
                 for (i, context) in transformers.iter().enumerate() {
                     match *context {
-                        // let cls = &cdb[cid];
-                        // match self.build_propagatation_context(false_lit, cid, cls, cached) {
                         Transformation::Conflict(cid, conflicting, flip_watches, cached) => {
                             if flip_watches {
                                 cdb.swap_watch(cid);
@@ -1002,7 +1052,9 @@ impl AssignStack {
                                 cid,
                                 Propagate::FindNewWatch(self.num_conflict, propagating, new_watch)
                             );
-                        }
+                        } // Transformation::Conflict(_, _, _, _) => {
+                          //     unreachable!()
+                          // }
                     }
                 }
                 start += transformers.len();
@@ -1017,52 +1069,6 @@ impl AssignStack {
         }
         Ok(())
     }
-    // NOTE: doesn't support chronoBT
-    fn build_propagatation_context(
-        &self,
-        false_lit: Lit,
-        cid: ClauseId,
-        c: &[Lit],
-        mut cached: Lit,
-    ) -> Transformation {
-        let mut other_watch_value = lit_assign!(self, cached);
-        let mut updated_cache: Option<Lit> = None;
-        if Some(true) == other_watch_value {
-            return Transformation::Satisfied(cid, updated_cache);
-        }
-        let lit0 = c[0];
-        let lit1 = c[1];
-        let (false_watch_pos, other) = if false_lit == lit1 {
-            (1, lit0)
-        } else {
-            (0, lit1)
-        };
-
-        if cached != other {
-            cached = other;
-            other_watch_value = lit_assign!(self, other);
-            updated_cache = Some(other);
-            if Some(true) == other_watch_value {
-                return Transformation::Satisfied(cid, updated_cache);
-            }
-        }
-        let start = 2;
-        for (k, lk) in c
-            .iter()
-            .enumerate()
-            .skip(start as usize)
-            .chain(c.iter().enumerate().skip(2).take(start as usize - 2))
-        {
-            if lit_assign!(self, *lk) != Some(false) {
-                let new_watch = !*lk;
-                return Transformation::UpdateWatch(cid, new_watch, false_watch_pos, k);
-            }
-        }
-        if other_watch_value == Some(false) {
-            return Transformation::Conflict(cid, cached, false_watch_pos == 0, updated_cache);
-        }
-        Transformation::UnitPropagation(cid, cached, false_watch_pos == 0, updated_cache)
-    }
 
     #[allow(dead_code)]
     fn check(&self, (b0, b1): (Lit, Lit)) {
@@ -1120,3 +1126,60 @@ impl AssignStack {
         }
     }
 }
+
+// NOTE: doesn't support chronoBT
+fn build_propagatation_context(
+    assign: &[Option<bool>],
+    false_lit: Lit,
+    cid: ClauseId,
+    c: &[Lit],
+    mut cached: Lit,
+) -> Transformation {
+    macro_rules! l_assign {
+        ($asg: expr, $lit: expr) => {
+            match $lit {
+                l => match unsafe { *$asg.get_unchecked(l.vi()) } {
+                    Some(x) if !bool::from(l) => Some(!x),
+                    x => x,
+                },
+            }
+        };
+    }
+    let mut other_watch_value = l_assign!(assign, cached);
+    let mut updated_cache: Option<Lit> = None;
+    if Some(true) == other_watch_value {
+        return Transformation::Satisfied(cid, updated_cache);
+    }
+    let lit0 = c[0];
+    let lit1 = c[1];
+    let (false_watch_pos, other) = if false_lit == lit1 {
+        (1, lit0)
+    } else {
+        (0, lit1)
+    };
+
+    if cached != other {
+        cached = other;
+        other_watch_value = l_assign!(assign, other);
+        updated_cache = Some(other);
+        if Some(true) == other_watch_value {
+            return Transformation::Satisfied(cid, updated_cache);
+        }
+    }
+    let start = 2;
+    for (k, lk) in c
+        .iter()
+        .enumerate()
+        .skip(start as usize)
+        .chain(c.iter().enumerate().skip(2).take(start as usize - 2))
+    {
+        if l_assign!(assign, *lk) != Some(false) {
+            let new_watch = !*lk;
+            return Transformation::UpdateWatch(cid, new_watch, false_watch_pos, k);
+        }
+    }
+    if other_watch_value == Some(false) {
+        return Transformation::Conflict(cid, cached, false_watch_pos == 0, updated_cache);
+    }
+    Transformation::UnitPropagation(cid, cached, false_watch_pos == 0, updated_cache)
+}
diff --git a/src/cdb/db.rs b/src/cdb/db.rs
index 438998832..6b3d4c7a7 100644
--- a/src/cdb/db.rs
+++ b/src/cdb/db.rs
@@ -227,13 +227,24 @@ impl ClauseDBIF for ClauseDB {
         self.binary_link.connect_with(l)
     }
     // watch_cache_IF
-    fn watcher_list(&self, lit: Lit, start: usize, len: usize) -> Vec<(ClauseId, Vec<Lit>, Lit)> {
-        self.watch_cache[lit]
-            .iter()
-            .skip(start)
-            .take(len)
-            .map(|(cid, l)| (*cid, self[*cid].lits.clone(), *l))
-            .collect::<Vec<_>>()
+    fn watcher_list(&self, lit: Lit, start: usize, len: usize) -> Vec<(ClauseId, &Vec<Lit>, Lit)> {
+        if len == 0 {
+            self.watch_cache[lit]
+                .iter()
+                .skip(start)
+                .map(|(cid, l)| (*cid, &self[*cid].lits, *l))
+                .collect::<Vec<_>>()
+        } else {
+            self.watch_cache[lit]
+                .iter()
+                .skip(start)
+                .take(len)
+                .map(|(cid, l)| (*cid, &self[*cid].lits, *l))
+                .collect::<Vec<_>>()
+        }
+    }
+    fn watcher_list_swap(&mut self, lit: Lit, index_a: usize, index_b: usize) {
+        self.watch_cache[lit].swap(index_a, index_b);
     }
     fn watcher_list_len(&self, lit: Lit) -> usize {
         self.watch_cache[lit].len()
diff --git a/src/cdb/mod.rs b/src/cdb/mod.rs
index 46ffd7a85..9c1d1640a 100644
--- a/src/cdb/mod.rs
+++ b/src/cdb/mod.rs
@@ -96,7 +96,8 @@ pub trait ClauseDBIF:
     //
 
     // return the number of clause watching `lit`
-    fn watcher_list(&self, lit: Lit, start: usize, len: usize) -> Vec<(ClauseId, Vec<Lit>, Lit)>;
+    fn watcher_list(&self, lit: Lit, start: usize, len: usize) -> Vec<(ClauseId, &Vec<Lit>, Lit)>;
+    fn watcher_list_swap(&mut self, lit: Lit, index_a: usize, index_b: usize);
     fn watcher_list_len(&self, lit: Lit) -> usize;
     // get mutable reference to a watch_cache
     fn fetch_watch_cache_entry(&self, lit: Lit, index: WatchCacheProxy) -> (ClauseId, Lit);

From 0dc62d39465416b7098197f4aa1a8665a3b4474e Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Mon, 25 Mar 2024 12:14:49 +0900
Subject: [PATCH 19/19] clean up

---
 src/assign/propagate.rs | 73 ++++++++++++++++++++---------------------
 1 file changed, 35 insertions(+), 38 deletions(-)

diff --git a/src/assign/propagate.rs b/src/assign/propagate.rs
index a8b3505d1..034f8c144 100644
--- a/src/assign/propagate.rs
+++ b/src/assign/propagate.rs
@@ -887,44 +887,41 @@ impl AssignStack {
                 // We need to build transformers several times if new unit propagation occur.
                 const CHUNK_SIZE: usize = 8;
 
-                let transformers = if CHUNK_SIZE * 4 < cdb.watcher_list_len(propagating) - start {
-                    cdb.watcher_list(propagating, start, 0)
-                        .par_iter()
-                        .chunks(CHUNK_SIZE)
-                        .map(|v /* (cid, clause, cached)*/| {
-                            v.iter()
-                                .map(|(cid, clause, cached)| {
-                                    build_propagatation_context(
-                                        &self.assign,
-                                        false_lit,
-                                        *cid,
-                                        clause,
-                                        *cached,
-                                    )
-                                })
-                                .collect::<Vec<_>>()
-                        })
-                        .flatten()
-                        .collect::<Vec<_>>()
-                } else {
-                    cdb.watcher_list(propagating, start, 1)
-                        // cdb.watch_cache_iter(propagating)
-                        .iter()
-                        // .skip(start)
-                        // .take(1)
-                        // .map(|index| cdb.fetch_watch_cache_entry(propagating, index))
-                        .map(|(cid, clause, cached)| {
-                            build_propagatation_context(
-                                &self.assign,
-                                false_lit,
-                                *cid,
-                                // &cdb[cid].iter().cloned().collect::<Vec<Lit>>(),
-                                clause,
-                                *cached,
-                            )
-                        })
-                        .collect::<Vec<Transformation>>()
-                };
+                let transformers =
+                    if CHUNK_SIZE * 400000000 < cdb.watcher_list_len(propagating) - start {
+                        cdb.watcher_list(propagating, start, 0)
+                            .par_iter()
+                            .chunks(CHUNK_SIZE)
+                            .map(|v /* (cid, clause, cached)*/| {
+                                v.iter()
+                                    .map(|(cid, lits, cached)| {
+                                        build_propagatation_context(
+                                            &self.assign,
+                                            false_lit,
+                                            *cid,
+                                            lits,
+                                            *cached,
+                                        )
+                                    })
+                                    .collect::<Vec<_>>()
+                            })
+                            .flatten()
+                            .collect::<Vec<_>>()
+                    } else {
+                        cdb.watcher_list(propagating, start, 1)
+                            .iter()
+                            .map(|(cid, lits, cached)| {
+                                build_propagatation_context(
+                                    &self.assign,
+                                    false_lit,
+                                    *cid,
+                                    // &cdb[cid].iter().cloned().collect::<Vec<Lit>>(),
+                                    lits,
+                                    *cached,
+                                )
+                            })
+                            .collect::<Vec<Transformation>>()
+                    };
                 // assert_eq!(transformers.len(), cdb.watcher_list_len(propagating));
                 // assert_eq!(transformers, transformers2);