Fix errors under non trail-saving settings

shnarazk · Feb 10, 2025 · 02f1d65 · 02f1d65
1 parent 7df2938
commit 02f1d65
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 4 deletions.
diff --git a/src/assign/propagate.rs b/src/assign/propagate.rs
@@ -202,8 +202,8 @@ impl PropagateIF for AssignStack {
 
             #[cfg(not(feature = "trail_saving"))]
             {
-                self.reward_at_unassign(vi);
-                self.insert_heap(vi);
+                VarActivityManager::reward_at_unassign(vi);
+                VarActivityManager::insert_heap(vi);
             }
         }
         self.trail.truncate(lim);

diff --git a/src/vam.rs b/src/vam.rs
@@ -241,6 +241,7 @@ impl VarHeapIF for VarIdHeap {
         let i = self.insert(vi);
         self.percolate_up(i as u32);
     }
+    #[allow(unused_variables)]
     fn get_heap_root(&mut self, asg: &mut AssignStack) -> VarId {
         #[cfg(feature = "trail_saving")]
         if self.is_empty() {
@@ -325,7 +326,7 @@ impl VarHeapIF for VarIdHeap {
     }
 }
 
-trait VarOrderIF {
+pub trait VarOrderIF {
     fn clear(&mut self);
     fn contains(&self, v: VarId) -> bool;
     fn get_root(&mut self) -> VarId;

diff --git a/src/var_vector.rs b/src/var_vector.rs
@@ -10,7 +10,9 @@ pub trait VarRefIF {
     fn set_level(&self, value: DecisionLevel);
     fn reason(&self) -> AssignReason;
     fn set_reason(&self, value: AssignReason);
+    #[cfg(feature = "trail_saving")]
     fn reason_saved(&self) -> AssignReason;
+    #[cfg(feature = "trail_saving")]
     fn set_reason_saved(&self, value: AssignReason);
     fn activity(&self) -> f64;
     fn set_activity(&self, value: f64);
@@ -52,11 +54,12 @@ impl VarRef {
             let vi = lit.vi();
             let possitive = bool::from(lit);
             match VAR_VECTOR.get_unchecked(vi).assign {
-                Some(b) if !possitive => Some(!b),
+                Some(b) => Some(b == possitive),
                 ob => ob,
             }
         }
     }
+    #[inline]
     pub fn set_lit(lit: Lit) {
         unsafe {
             let vi = lit.vi();
@@ -139,10 +142,12 @@ impl VarRefIF for VarRef {
             VAR_VECTOR.get_unchecked_mut(self.0).reason = value;
         }
     }
+    #[cfg(feature = "trail_saving")]
     #[inline]
     fn reason_saved(&self) -> AssignReason {
         unsafe { VAR_VECTOR.get_unchecked(self.0).reason_saved }
     }
+    #[cfg(feature = "trail_saving")]
     #[inline]
     fn set_reason_saved(&self, value: AssignReason) {
         unsafe {