Plug a conversion miss; rename a function

shnarazk · Feb 8, 2025 · 3bc95b4 · 3bc95b4
1 parent 4db2c1a
commit 3bc95b4
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 5 deletions.
diff --git a/src/processor/mod.rs b/src/processor/mod.rs
@@ -73,7 +73,7 @@ pub trait EliminateIF: Instantiate {
     /// return the order of vars based on their occurrences
     fn sorted_iterator(&self) -> Iter<'_, u32>;
     /// return vi's stats
-    fn num_phases(&self, vi: VarId) -> Option<(usize, usize)>;
+    fn get_phases(&self, vi: VarId) -> Option<(usize, usize)>;
     /// return the constraints on eliminated literals.
     fn eliminated_lits(&mut self) -> &mut Vec<Lit>;
 }

diff --git a/src/processor/simplify.rs b/src/processor/simplify.rs
@@ -283,7 +283,7 @@ impl EliminateIF for Eliminator {
             if !force_run && self.mode == EliminatorMode::Dormant {
                 self.prepare(cdb, true);
             }
-            self.eliminate_grow_limit = state.stm.current_scale();
+            self.eliminate_grow_limit = state.stm.current_scale() / 2;
             self.subsume_literal_limit =
                 state.config.elm_cls_lim + cdb.lb_entanglement().get() as usize;
             debug_assert!(!cdb.lb_entanglement().get().is_nan());
@@ -306,7 +306,7 @@ impl EliminateIF for Eliminator {
     fn sorted_iterator(&self) -> Iter<'_, u32> {
         self.var_queue.heap[1..].iter()
     }
-    fn num_phases(&self, vi: VarId) -> Option<(usize, usize)> {
+    fn get_phases(&self, vi: VarId) -> Option<(usize, usize)> {
         let w = &self[vi];
         if w.aborted {
             None

diff --git a/src/solver/search.rs b/src/solver/search.rs
@@ -101,7 +101,7 @@ impl SolveIF for Solver {
                     if VarRef(vi).assign().is_some() {
                         continue;
                     }
-                    if let Some((p, m)) = elim.num_phases(vi) {
+                    if let Some((p, m)) = elim.get_phases(vi) {
                         // We can't call `asg.assign_at_root_level(l)` even if p or m == 0.
                         // This means we can't pick `!l`.
                         // This becomes a problem in the case of incremental solving.
@@ -142,7 +142,7 @@ impl SolveIF for Solver {
                         if VarRef(vi).assign().is_some() || VarRef(vi).is(FlagVar::ELIMINATED) {
                             continue;
                         }
-                        match elim.num_phases(vi) {
+                        match elim.get_phases(vi) {
                             Some((_, 0)) => (),
                             Some((0, _)) => (),
                             Some((p, m)) if m * 10 < p => VarRef(vi).turn_on(FlagVar::PHASE),