ditto and fix a bug

shnarazk · Feb 8, 2025 · 5fab2c0 · 5fab2c0
1 parent d34ba70
commit 5fab2c0
Show file tree

Hide file tree

Showing 7 changed files with 110 additions and 105 deletions.
diff --git a/src/assign/mod.rs b/src/assign/mod.rs
@@ -5,6 +5,11 @@
 mod ema;
 /// Boolean constraint propagation
 mod propagate;
+
+#[cfg(feature = "rephase")]
+/// rephasing
+pub mod rephase;
+
 /// assignment management
 mod stack;
 /// properties
@@ -13,10 +18,7 @@ pub mod stats;
 mod trail_saving;
 
 pub use self::{propagate::PropagateIF, stack::AssignStack};
-use {
-    crate::types::*,
-    std::{collections::HashMap, fmt},
-};
+use {crate::types::*, std::fmt};
 
 #[cfg(feature = "trail_saving")]
 pub use self::trail_saving::TrailSavingIF;
@@ -111,14 +113,3 @@ impl DebugReportIF for Clause {
         l
     }
 }
-
-#[cfg(feature = "rephase")]
-pub trait AssignRephaseIF {
-    /// check usability of the saved best phase.
-    /// return `true` if the current best phase got invalid.
-    fn check_best_phase(&mut self, vi: VarId) -> bool;
-    fn best_phases_ref(&mut self, default_value: Option<bool>) -> HashMap<VarId, bool>;
-    fn override_rephasing_target(&mut self, assignment: &HashMap<VarId, bool>) -> usize;
-    fn select_rephasing_target(&mut self);
-    fn check_consistency_of_best_phases(&mut self);
-}
diff --git a/src/assign/propagate.rs b/src/assign/propagate.rs
@@ -11,7 +11,7 @@ use {
 };
 
 #[cfg(feature = "rephase")]
-use super::AssignRephaseIF;
+use super::rephase::AssignRephaseIF;
 
 #[cfg(feature = "trail_saving")]
 use super::TrailSavingIF;

diff --git a/src/assign/rephase.rs b/src/assign/rephase.rs
@@ -0,0 +1,90 @@
+use {
+    super::AssignStack,
+    crate::{types::*, var_vector::*},
+    std::collections::HashMap,
+};
+
+pub trait AssignRephaseIF {
+    /// check usability of the saved best phase.
+    /// return `true` if the current best phase got invalid.
+    fn check_best_phase(&mut self, vi: VarId) -> bool;
+    fn best_phases_ref(&mut self, default_value: Option<bool>) -> HashMap<VarId, bool>;
+    fn override_rephasing_target(&mut self, assignment: &HashMap<VarId, bool>) -> usize;
+    fn select_rephasing_target(&mut self);
+    fn check_consistency_of_best_phases(&mut self);
+}
+
+impl AssignRephaseIF for AssignStack {
+    /// check usability of the saved best phase.
+    /// return `true` if the current best phase got invalid.
+    fn check_best_phase(&mut self, vi: VarId) -> bool {
+        if let Some((b, _)) = self.best_phases.get(&vi) {
+            debug_assert!(VarRef(vi).assign().is_some());
+            if VarRef(vi).assign() != Some(*b) {
+                if self.root_level == VarRef(vi).level() {
+                    self.best_phases.clear();
+                    self.num_best_assign = self.num_asserted_vars + self.num_eliminated_vars;
+                }
+                return true;
+            }
+        }
+        false
+    }
+    fn best_phases_ref(&mut self, default_value: Option<bool>) -> HashMap<VarId, bool> {
+        VarRef::var_id_iter()
+            .filter_map(|vi| {
+                if VarRef(vi).level() == self.root_level || VarRef(vi).is(FlagVar::ELIMINATED) {
+                    default_value.map(|b| (vi, b))
+                } else {
+                    Some((
+                        vi,
+                        self.best_phases.get(&vi).map_or(
+                            VarRef(vi)
+                                .assign()
+                                .unwrap_or_else(|| VarRef(vi).is(FlagVar::PHASE)),
+                            |(b, _)| *b,
+                        ),
+                    ))
+                }
+            })
+            .collect::<HashMap<VarId, bool>>()
+    }
+    fn override_rephasing_target(&mut self, assignment: &HashMap<VarId, bool>) -> usize {
+        let mut num_flipped = 0;
+        for (vi, b) in assignment.iter() {
+            if self.best_phases.get(vi).is_none_or(|(p, _)| *p != *b) {
+                num_flipped += 1;
+                self.best_phases.insert(*vi, (*b, AssignReason::None));
+            }
+        }
+        num_flipped
+    }
+    fn select_rephasing_target(&mut self) {
+        if self.best_phases.is_empty() {
+            return;
+        }
+        self.check_consistency_of_best_phases();
+        if self.num_unasserted_vars() <= self.best_phases.len() {
+            self.best_phases.clear();
+            return;
+        }
+        debug_assert!(self
+            .best_phases
+            .iter()
+            .all(|(vi, b)| VarRef(*vi).assign() != Some(!b.0)));
+        self.num_rephase += 1;
+        for (vi, (b, _)) in self.best_phases.iter() {
+            VarRef(*vi).set_flag(FlagVar::PHASE, *b);
+        }
+    }
+    fn check_consistency_of_best_phases(&mut self) {
+        if self
+            .best_phases
+            .iter()
+            .any(|(vi, b)| VarRef(*vi).assign() == Some(!b.0))
+        {
+            self.best_phases.clear();
+            self.num_best_assign = self.num_asserted_vars + self.num_eliminated_vars;
+        }
+    }
+}
diff --git a/src/assign/stack.rs b/src/assign/stack.rs
@@ -6,7 +6,7 @@ use {
 };
 
 #[cfg(any(feature = "best_phases_tracking", feature = "rephase"))]
-use {super::AssignRephaseIF, std::collections::HashMap};
+use std::collections::HashMap;
 
 #[cfg(feature = "trail_saving")]
 use super::TrailSavingIF;
@@ -377,82 +377,6 @@ impl fmt::Display for AssignStack {
     }
 }
 
-#[cfg(feature = "rephase")]
-impl AssignRephaseIF for AssignStack {
-    /// check usability of the saved best phase.
-    /// return `true` if the current best phase got invalid.
-    fn check_best_phase(&mut self, vi: VarId) -> bool {
-        if let Some((b, _)) = self.best_phases.get(&vi) {
-            debug_assert!(VarRef(vi).assign().is_some());
-            if VarRef(vi).assign() != Some(*b) {
-                if self.root_level == VarRef(vi).level() {
-                    self.best_phases.clear();
-                    self.num_best_assign = self.num_asserted_vars + self.num_eliminated_vars;
-                }
-                return true;
-            }
-        }
-        false
-    }
-    fn best_phases_ref(&mut self, default_value: Option<bool>) -> HashMap<VarId, bool> {
-        VarRef::var_id_iter()
-            .filter_map(|vi| {
-                if VarRef(vi).level() == self.root_level || VarRef(vi).is(FlagVar::ELIMINATED) {
-                    default_value.map(|b| (vi, b))
-                } else {
-                    Some((
-                        vi,
-                        self.best_phases.get(&vi).map_or(
-                            VarRef(vi)
-                                .assign()
-                                .unwrap_or_else(|| VarRef(vi).is(FlagVar::PHASE)),
-                            |(b, _)| *b,
-                        ),
-                    ))
-                }
-            })
-            .collect::<HashMap<VarId, bool>>()
-    }
-    fn override_rephasing_target(&mut self, assignment: &HashMap<VarId, bool>) -> usize {
-        let mut num_flipped = 0;
-        for (vi, b) in assignment.iter() {
-            if self.best_phases.get(vi).is_none_or(|(p, _)| *p != *b) {
-                num_flipped += 1;
-                self.best_phases.insert(*vi, (*b, AssignReason::None));
-            }
-        }
-        num_flipped
-    }
-    fn select_rephasing_target(&mut self) {
-        if self.best_phases.is_empty() {
-            return;
-        }
-        self.check_consistency_of_best_phases();
-        if self.num_unasserted_vars() <= self.best_phases.len() {
-            self.best_phases.clear();
-            return;
-        }
-        debug_assert!(self
-            .best_phases
-            .iter()
-            .all(|(vi, b)| VarRef(*vi).assign() != Some(!b.0)));
-        self.num_rephase += 1;
-        for (vi, (b, _)) in self.best_phases.iter() {
-            VarRef(*vi).set_flag(FlagVar::PHASE, *b);
-        }
-    }
-    fn check_consistency_of_best_phases(&mut self) {
-        if self
-            .best_phases
-            .iter()
-            .any(|(vi, b)| VarRef(*vi).assign() == Some(!b.0))
-        {
-            self.best_phases.clear();
-            self.num_best_assign = self.num_asserted_vars + self.num_eliminated_vars;
-        }
-    }
-}
-
 #[cfg(test)]
 mod tests {
     use super::*;

diff --git a/src/processor/eliminate.rs b/src/processor/eliminate.rs
@@ -135,9 +135,10 @@ pub fn eliminate_var(
         cdb.remove_clause(*cid);
     }
     elim[vi].clear();
-    VarRef::make_var_eliminated(vi);
-    asg.handle(SolverEvent::Eliminate(vi));
-    state.restart.handle(SolverEvent::Eliminate(vi));
+    if VarRef::make_var_eliminated(vi) {
+        asg.handle(SolverEvent::Eliminate(vi));
+        state.restart.handle(SolverEvent::Eliminate(vi));
+    }
     elim.backward_subsumption_check(asg, cdb, timedout)
 }
 

diff --git a/src/solver/search.rs b/src/solver/search.rs
@@ -16,7 +16,7 @@ use {
 };
 
 #[cfg(feature = "rephase")]
-use crate::assign::AssignRephaseIF;
+use crate::assign::rephase::AssignRephaseIF;
 
 /// API to [`solve`](`crate::solver::SolveIF::solve`) SAT problems.
 pub trait SolveIF {

diff --git a/src/var_vector.rs b/src/var_vector.rs
@@ -83,9 +83,14 @@ impl VarRef {
         }
     }
     /// set `vi`s status to eliminated.
-    pub fn make_var_eliminated(vi: VarId) {
+    /// return true if `vi` is just eliminated.
+    pub fn make_var_eliminated(vi: VarId) -> bool {
         unsafe {
             if VAR_VECTOR[vi].is(FlagVar::ELIMINATED) {
+                #[cfg(feature = "boundary_check")]
+                panic!("double elimination");
+                false
+            } else {
                 VAR_VECTOR[vi].turn_on(FlagVar::ELIMINATED);
                 VAR_VECTOR[vi].activity = 0.0;
                 VarActivityManager::remove_from_heap(vi);
@@ -94,13 +99,7 @@ impl VarRef {
                 {
                     self.var[vi].timestamp = self.tick;
                 }
-                #[cfg(feature = "trace_elimination")]
-                debug_assert!(
-                    asg.root_level() < VAR_VECTOR[vi].level || VAR_VECTOR[vi].assign.is_none()
-                );
-            } else {
-                #[cfg(feature = "boundary_check")]
-                panic!("double elimination");
+                true
             }
         }
     }