add Clause::watches

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!(

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()
     }

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.