Initialize Clause::{rank|rank_old} correctly

shnarazk · Sep 21, 2024 · 5ebd423 · 5ebd423
1 parent a9744ff
commit 5ebd423
Show file tree

Hide file tree

Showing 3 changed files with 13 additions and 8 deletions.
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/src/cdb/clause.rs b/src/cdb/clause.rs
@@ -100,8 +100,8 @@ impl Default for Clause {
             ],
             lits: vec![Lit::default(), Lit::default()],
             flags: FlagClause::empty(),
-            rank: 0,
-            rank_old: 0,
+            rank: u32::MAX,
+            rank_old: u32::MAX,
             search_from: 2,
 
             #[cfg(any(feature = "boundary_check", feature = "clause_rewarding"))]
@@ -327,7 +327,10 @@ impl Clause {
                 cnt += 1;
             }
         }
-        self.rank = cnt;
-        cnt
+        if cnt < self.rank {
+            self.rank_old = self.rank;
+            self.rank = cnt;
+        }
+        self.rank
     }
 }
diff --git a/src/cdb/mod.rs b/src/cdb/mod.rs
@@ -270,7 +270,6 @@ impl ClauseDBIF for ClauseDB {
             debug_assert_eq!(l1, self[ci].lits[1]);
         }
         self.clause[ci].search_from = 0;
-        self.clause[ci].rank_old = self[ci].rank;
         self.lbd.update(self[ci].rank);
         self.num_clause += 1;
         if learnt {
@@ -1157,7 +1156,10 @@ impl ClauseWeaverIF for ClauseDB {
             );
             debug_assert_ne!(next, self.watch[FREE_LIT].next);
             debug_assert_ne!(0, next.as_ci());
-            next.as_ci()
+            let ci = next.as_ci();
+            self.clause[ci].rank = u32::MAX;
+            self.clause[ci].rank_old = u32::MAX;
+            ci
         }
     }
     // Check whether a zombi exists