From 07efd8898d0bad7593cc729009cb9d57241a6dde Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Sun, 12 Jan 2025 14:03:49 +0900
Subject: [PATCH] add `Clause::watches`

---
 src/assign/propagate.rs | 4 ++++
 src/cdb/clause.rs       | 3 +++
 src/cdb/mod.rs          | 2 ++
 3 files changed, 9 insertions(+)

diff --git a/src/assign/propagate.rs b/src/assign/propagate.rs
index c165202aa..187fdaa08 100644
--- a/src/assign/propagate.rs
+++ b/src/assign/propagate.rs
@@ -433,6 +433,7 @@ impl PropagateIF for AssignStack {
             //
             //## normal clause loop
             //
+            // TODO: check whether dead clauses exists. If so, run `retain()` after propagation.
             let mut source = cdb.watch_cache_iter(propagating);
             'next_clause: while let Some((cid, mut cached)) = source
                 .next()
@@ -444,6 +445,9 @@ impl PropagateIF for AssignStack {
                     "dead clause in propagation: {:?}",
                     cdb.is_garbage_collected(cid),
                 );
+                if cdb[cid].watches(propagating) {
+                    continue;
+                }
                 debug_assert!(!self.var[cached.vi()].is(FlagVar::ELIMINATED));
                 #[cfg(feature = "maintain_watch_cache")]
                 debug_assert!(
diff --git a/src/cdb/clause.rs b/src/cdb/clause.rs
index 31b02478a..5965f318e 100644
--- a/src/cdb/clause.rs
+++ b/src/cdb/clause.rs
@@ -204,6 +204,9 @@ impl ClauseIF for Clause {
         }
         false
     }
+    fn watches(&self, lit: Lit) -> bool {
+        self.lits[0] == lit || self.lits[1] == lit
+    }
     fn len(&self) -> usize {
         self.lits.len()
     }
diff --git a/src/cdb/mod.rs b/src/cdb/mod.rs
index 1fdad39f9..22aaeec25 100644
--- a/src/cdb/mod.rs
+++ b/src/cdb/mod.rs
@@ -56,6 +56,8 @@ pub trait ClauseIF {
     fn contains(&self, lit: Lit) -> bool;
     /// check clause satisfiability
     fn is_satisfied_under(&self, asg: &impl AssignIF) -> bool;
+    /// return `true` if the clause is watching the literal
+    fn watches(&self, lit: Lit) -> bool;
     /// return an iterator over its literals.
     fn iter(&self) -> Iter<'_, Lit>;
     /// return the number of literals.