JigSAT: Remove Step from trail entirely

sarsko · Jul 15, 2022 · eba2cbc · eba2cbc
1 parent 6f3f09b
commit eba2cbc
Show file tree

Hide file tree

Showing 7 changed files with 27 additions and 34 deletions.
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/JigSAT/src/assignments.rs b/JigSAT/src/assignments.rs
@@ -32,7 +32,7 @@ impl Assignments {
     }
 
     #[inline]
-    pub(crate) fn set_assignment(&mut self, lit: Lit, _f: &Formula, _t: &[Step]) {
+    pub(crate) fn set_assignment(&mut self, lit: Lit, _f: &Formula, _t: &[Lit]) {
         self[lit.index()] = lit.is_positive() as u8;
     }
 

diff --git a/JigSAT/src/conflict_analysis.rs b/JigSAT/src/conflict_analysis.rs
@@ -71,19 +71,19 @@ pub(crate) fn analyze_conflict(
         let next = {
             loop {
                 i -= 1;
-                if seen[trail.trail[i].lit.index()] {
+                if seen[trail.trail[i].index()] {
                     break;
                 }
             }
             &trail.trail[i]
         };
-        seen[next.lit.index()] = false;
+        seen[next.index()] = false;
         path_c -= 1;
         if path_c == 0 {
-            out_learnt[0] = !next.lit;
+            out_learnt[0] = !*next;
             break;
         }
-        confl = next.reason;
+        confl = trail.lit_to_reason[next.index()];
     }
     // decisions.bump_vec_of_vars(f, to_bump); // VMTF. NO-OP for VSIDS
 

diff --git a/JigSAT/src/solver.rs b/JigSAT/src/solver.rs
@@ -146,8 +146,7 @@ impl Solver {
         //d.increment_and_move(f, cref, &t.assignments);
         trail.backtrack_to(level, formula, decisions, target_phase);
         let lit = formula[cref][0];
-        let step = Step { lit, reason: cref };
-        trail.enq_assignment(step, formula);
+        trail.enq_assignment(lit, formula, cref);
     }
 
     #[inline]

diff --git a/JigSAT/src/target_phase.rs b/JigSAT/src/target_phase.rs
@@ -90,7 +90,7 @@ impl TargetPhase {
                 *e = 2;
             }
             for e in &trail.trail {
-                self.best_polarity[e.lit.index()] = e.lit.is_positive() as u8;
+                self.best_polarity[e.index()] = e.is_positive() as u8;
             }
             self.best_phase_len = len;
             if self.best_of_the_best_phase_len < self.best_phase_len {

diff --git a/JigSAT/src/trail.rs b/JigSAT/src/trail.rs
@@ -21,7 +21,7 @@ const UNIT: usize = usize::MAX;
 pub(crate) struct Step {
     pub lit: Lit,
     //decision_level: u32, // Turns out we never read this
-    pub reason: Cref,
+    //pub reason: Cref,
 }
 
 pub const UNSET_LEVEL: u32 = u32::MAX;
@@ -31,7 +31,7 @@ pub(crate) struct Trail {
     pub assignments: Assignments,
     pub lit_to_level: Vec<u32>,    // u32::MAX if unassigned
     pub lit_to_reason: Vec<usize>, // usize::MAX if unassigned
-    pub trail: Vec<Step>,
+    pub trail: Vec<Lit>,
     pub curr_i: usize,
     pub decisions: Vec<usize>,
 }
@@ -55,14 +55,14 @@ impl Trail {
 
     fn backstep(&mut self, formula: &Formula, target_phase: &mut TargetPhase) -> usize {
         match self.trail.pop() {
-            Some(step) => {
-                target_phase.set_polarity(step.lit.index(), step.lit.is_positive());
+            Some(lit) => {
+                target_phase.set_polarity(lit.index(), lit.is_positive());
 
-                self.assignments[step.lit.index()] = 2;
-                self.lit_to_reason[step.lit.index()] = UNSET_REASON;
+                self.assignments[lit.index()] = 2;
+                self.lit_to_reason[lit.index()] = UNSET_REASON;
                 //self.lit_to_level[step.lit.index()] = UNSET_LEVEL;
 
-                step.lit.index()
+                lit.index()
             }
             None => {
                 unreachable!();
@@ -117,15 +117,13 @@ impl Trail {
         self.curr_i = self.trail.len();
     }
 
-    pub(crate) fn enq_assignment(&mut self, step: Step, _f: &Formula) {
+    pub(crate) fn enq_assignment(&mut self, lit: Lit, _f: &Formula, reason: Cref) {
         // This should be refactored to not have to be a match (ie splitting up enq_assignment)
-        if step.reason < usize::MAX - 1 {
-            self.lit_to_reason[step.lit.index()] = step.reason;
-        }
+        self.lit_to_reason[lit.index()] = reason;
 
-        self.lit_to_level[step.lit.index()] = self.decision_level();
-        self.assignments.set_assignment(step.lit, _f, &self.trail);
-        self.trail.push(step);
+        self.lit_to_level[lit.index()] = self.decision_level();
+        self.assignments.set_assignment(lit, _f, &self.trail);
+        self.trail.push(lit);
     }
 
     pub(crate) fn enq_decision(&mut self, idx: usize, _f: &Formula, target_phase: &TargetPhase, mode_is_focus: bool) {
@@ -139,8 +137,7 @@ impl Trail {
         self.assignments[idx] = polarity as u8;
         let lit = Lit::new(idx, polarity);
 
-        let step = Step { lit /*, decision_level: dlevel*/, reason: DECISION };
-        self.trail.push(step);
+        self.trail.push(lit);
     }
 
     #[inline]
@@ -149,7 +146,7 @@ impl Trail {
         solver: &Solver, target_phase: &mut TargetPhase,
     ) {
         self.restart(formula, decisions, watches, solver, target_phase);
-        self.enq_assignment(Step { lit /*, decision_level: 0*/, reason: UNIT }, formula);
+        self.enq_assignment(lit, formula, UNIT);
     }
 
     pub(crate) fn learn_units(&mut self, formula: &mut Formula) -> Option<usize> {
@@ -164,7 +161,7 @@ impl Trail {
                         return Some(i);
                     }
                 }
-                self.enq_assignment(Step { lit /*, decision_level: 0*/, reason: UNIT }, formula);
+                self.enq_assignment(lit, formula, UNIT);
                 formula.remove_clause_in_preprocessing(i);
             } else {
                 i += 1;
@@ -184,6 +181,6 @@ impl Trail {
     #[inline]
     pub(crate) fn learn_unit_in_preprocessing(&mut self, lit: Lit, f: &Formula) {
         debug!("Learned unit: {} in preproc", lit);
-        self.enq_assignment(Step { lit /*, decision_level: 0*/, reason: UNIT }, f);
+        self.enq_assignment(lit, f, UNIT);
     }
 }
diff --git a/JigSAT/src/unit_prop.rs b/JigSAT/src/unit_prop.rs
@@ -61,14 +61,10 @@ fn unit_prop_do_outer(
         return Err(cref);
     }
     if f[cref][0].lit_unset(&trail.assignments) {
-        let step = Step { lit: f[cref][0] /*, decision_level: trail.decision_level()*/, reason: cref };
-
-        trail.enq_assignment(step, f);
+        trail.enq_assignment(f[cref][0], f, cref);
         return Ok(true);
     } else {
-        let step = Step { lit: f[cref][1] /*, decision_level: trail.decision_level()*/, reason: cref };
-
-        trail.enq_assignment(step, f);
+        trail.enq_assignment(f[cref][1], f, cref);
         f[cref].swap(0, 1);
         return Ok(true);
     }
@@ -106,7 +102,7 @@ pub(crate) fn unit_propagate(
 ) -> Result<(), usize> {
     let mut i = trail.curr_i;
     while i < trail.trail.len() {
-        let lit = trail.trail[i].lit;
+        let lit = trail.trail[i];
         match unit_prop_current_level(f, trail, watches, lit, solver) {
             Ok(_) => {}
             Err(cref) => {