JigSAT: Prepare clauses for new clause DB

JigSAT/src/clause.rs

@@ -7,13 +7,13 @@ use std::{
 use crate::preprocess::SubsumptionRes;
 
 pub struct Clause {
-    pub deleted: bool,
-    pub can_be_deleted: bool,
-    pub mark: u8, // This is an artifact of Glucose/MiniSat, and should be enumed
-    pub lbd: u32,
-    pub search: usize,
+    deleted: bool,
+    can_be_deleted: bool,
+    mark: u8, // This is an artifact of Glucose/MiniSat, and should be enumed
+    lbd: u32,
+    search: usize,
     abstraction: usize,
-    pub lits: Vec<Lit>,
+    lits: Vec<Lit>,
 }
 
 impl Index<usize> for Clause {
@@ -92,6 +92,16 @@ impl Clause {
         self.lits.pop();
     }
 
+    /*
+    deleted: bool,
+    can_be_deleted: bool,
+    mark: u8, // This is an artifact of Glucose/MiniSat, and should be enumed
+    lbd: u32,
+    search: usize,
+    abstraction: usize,
+    lits: Vec<Lit>,
+    */
+
     pub(crate) fn less_than(&self, other: &Clause) -> Ordering {
         if self.len() == 2 {
             if other.len() == 2 {
@@ -261,3 +271,61 @@ impl Clause {
         self.calc_and_set_abstraction();
     }
 }
+
+impl ClauseTrait for Clause {
+    fn is_deleted(&self) -> bool {
+        self.deleted
+    }
+
+    fn can_be_deleted(&self) -> bool {
+        self.can_be_deleted
+    }
+
+    fn get_mark(&self) -> u8 {
+        self.mark
+    }
+
+    fn get_lbd(&self) -> u32 {
+        self.lbd
+    }
+
+    fn get_search_index(&self) -> usize {
+        self.search
+    }
+
+    fn set_search_index(&mut self, new_idx: usize) {
+        self.search = new_idx;
+    }
+
+    fn get_abstraction(&self) -> usize {
+        self.abstraction
+    }
+
+    fn get_literals(&self) -> &[Lit] {
+        &self.lits
+    }
+
+    fn set_deleted(&mut self, new_val: bool) {
+        self.deleted = new_val;
+    }
+}
+
+pub(crate) trait ClauseTrait {
+    fn is_deleted(&self) -> bool;
+
+    fn can_be_deleted(&self) -> bool;
+
+    fn set_deleted(&mut self, new_val: bool);
+
+    fn get_mark(&self) -> u8; // TODO: enum
+
+    fn get_lbd(&self) -> u32;
+
+    fn get_search_index(&self) -> usize;
+
+    fn set_search_index(&mut self, new_idx: usize);
+
+    fn get_abstraction(&self) -> usize;
+
+    fn get_literals(&self) -> &[Lit];
+}

JigSAT/src/conflict_analysis.rs

@@ -105,13 +105,13 @@ pub(crate) fn analyze_conflict(
         out_learnt.swap(1, max_i);
         let mut clause = Clause::new(out_learnt);
         clause.calc_and_set_lbd(trail, solver);
-        let lbd = clause.lbd;
+        let lbd = clause.get_lbd();
 
         // VSIDS:
         // UPDATEVARACTIVITY trick (see competition'09 companion paper)
         if solver.search_mode == SearchMode::Focus || solver.search_mode == SearchMode::OnlyFocus {
             for var in to_bump.iter() {
-                if formula[trail.lit_to_reason[*var]].lbd < lbd {
+                if formula[trail.lit_to_reason[*var]].get_lbd() < lbd {
                     decisions.bump_variable(*var);
                 }
             }

JigSAT/src/decision.rs

@@ -1,4 +1,4 @@
-use crate::{assignments::*, formula::*, trail::*, util::*};
+use crate::{assignments::*, formula::*, trail::*, util::*, clause::ClauseTrait};
 use std::ops::{Index, IndexMut};
 
 const INVALID: usize = usize::MAX;
@@ -469,7 +469,7 @@ impl Decisions for VSIDS {
             return;
         }
         let clause = &formula[reason];
-        for l in formula[reason].lits.iter().skip(1) {
+        for l in formula[reason].get_literals().iter().skip(1) {
             self.bump_variable(l.index());
         }
     }

JigSAT/src/formula.rs

@@ -128,15 +128,15 @@ impl Formula {
 
     #[inline(always)]
     pub(crate) fn mark_clause_as_deleted(&mut self, cref: usize) {
-        self.clauses[cref].deleted = true;
+        self.clauses[cref].set_deleted(true);
         self.num_deleted_clauses += 1;
         //self.clauses.remove(cref);
     }
 
     pub(crate) fn remove_deleted(&mut self) {
         let mut i = 0;
         while i < self.len() {
-            if self[i].deleted {
+            if self[i].is_deleted() {
                 self.clauses.swap_remove(i);
             } else {
                 i += 1;
@@ -156,7 +156,7 @@ impl Formula {
         // unwatch trivially SAT
         let mut i = 0;
         while i < self.len() {
-            if !self[i].deleted {
+            if !self[i].is_deleted() {
                 if self[i].len() > 1 && self.is_clause_sat(i, &t.assignments) {
                     self.unwatch_and_mark_as_deleted(i, watches, t);
                 }
@@ -182,10 +182,10 @@ impl Formula {
         self.learnt_core.sort_unstable_by(|a, b| self.clauses[*a].less_than(&self.clauses[*b]));
         //s.max_len += self.len() + 300;
         //self.num_reduced += 1;
-        if self[self.learnt_core[self.learnt_core.len() / 2]].lbd <= 3 {
+        if self[self.learnt_core[self.learnt_core.len() / 2]].get_lbd() <= 3 {
             self.num_clauses_before_reduce += self.special_inc_reduce_db;
         }
-        if self[self.learnt_core[self.learnt_core.len() - 1]].lbd <= 5 {
+        if self[self.learnt_core[self.learnt_core.len() - 1]].get_lbd() <= 5 {
             self.num_clauses_before_reduce += self.special_inc_reduce_db;
         }
         //watches.unwatch_all_lemmas(self, s);
@@ -195,13 +195,13 @@ impl Formula {
         while i < self.learnt_core.len() && limit > 0 {
             let cref = self.learnt_core[i];
             let clause = &mut self[cref];
-            if clause.lbd > 2 && clause.len() > 2 && clause.can_be_deleted {
+            if clause.get_lbd() > 2 && clause.len() > 2 && clause.can_be_deleted() {
                 //&& !trail.locked(clause[0]) {
                 self.unwatch_and_mark_as_deleted(cref, watches, trail);
                 self.learnt_core.swap_remove(i);
                 limit -= 1;
             } else {
-                clause.can_be_deleted = true;
+                clause.set_deleted(true);
                 i += 1;
             }
         }
@@ -232,7 +232,7 @@ impl Formula {
         self.learnt_core.clear();
         let mut i = s.initial_len;
         while i < self.len() {
-            if self[i].deleted {
+            if self[i].can_be_deleted() {
                 self.clauses.swap_remove(i);
             } else {
                 self.learnt_core.push(i);

JigSAT/src/preprocess.rs

@@ -78,7 +78,7 @@ impl Preprocess {
         self.occurs = vec![Vec::new(); formula.num_vars() * 2];
         self.n_occ = vec![0; formula.num_vars() * 2];
         for (i, c) in formula.iter().enumerate() {
-            for l in &c.lits {
+            for l in c.get_literals() {
                 self.occurs[l.index()].push(i);
                 self.n_occ[l.to_watchidx()] += 1;
             }
@@ -106,7 +106,7 @@ impl Preprocess {
         let cref = formula.add_unwatched_clause(clause);
         debug!("Added: {}", cref);
         self.subsumption_queue.push_back(cref);
-        for l in &formula[cref].lits {
+        for l in formula[cref].get_literals() {
             self.occurs[l.index()].push(cref);
             self.n_occ[l.to_watchidx()] += 1;
             self.touched[l.index()] = true;
@@ -134,7 +134,7 @@ impl Preprocess {
                 //for j in 0..cs.len() {
                 //if formula[cs[j]].get_mark() == 0 && !formula[cs[j]].deleted {
                 while j < cs.len() {
-                    if !formula[cs[j]].deleted {
+                    if !formula[cs[j]].is_deleted() {
                         cs.swap_remove(j);
                     } else if formula[cs[j]].get_mark() == 0 {
                         self.subsumption_queue.push_back(cs[j]);
@@ -217,12 +217,12 @@ impl Preprocess {
     }
 
     fn remove_clause_in_preprocessing(&mut self, formula: &mut Formula, cref: usize) {
-        if formula[cref].deleted {
+        if formula[cref].is_deleted() {
             unreachable!("Already deleted");
             return;
         }
-        debug!("Removing cref: {}, {:?}", cref, &formula[cref].lits);
-        for l in &formula[cref].lits {
+        debug!("Removing cref: {}, {:?}", cref, formula[cref].get_literals());
+        for l in formula[cref].get_literals() {
             self.n_occ[l.to_watchidx()] -= 1;
             if let Some(index) = self.occurs[l.index()].iter().position(|value| *value == cref) {
                 debug!("Removed clause {} due to {}", &formula[cref], l);
@@ -265,7 +265,7 @@ impl Preprocess {
             //let c = &formula[cr];
 
             // When is the clause marked?
-            if formula[cr].is_marked() || formula[cr].deleted {
+            if formula[cr].is_marked() || formula[cr].is_deleted() {
                 continue;
             }
 
@@ -388,9 +388,9 @@ impl Preprocess {
         let mut pos = Vec::new();
         let mut neg = Vec::new();
         for e in &self.occurs[v] {
-            if Lit::new(v, true).lit_in_clause(&formula[*e].lits) {
+            if Lit::new(v, true).lit_in_clause(&formula[*e].get_literals()) {
                 pos.push(*e);
-            } else if Lit::new(v, false).lit_in_clause(&formula[*e].lits) {
+            } else if Lit::new(v, false).lit_in_clause(&formula[*e].get_literals()) {
                 neg.push(*e);
             } else {
                 panic!("Haha");
@@ -439,7 +439,7 @@ impl Preprocess {
         for p in &pos {
             for n in &neg {
                 let mut resolvent = Vec::new();
-                if formula[*p].deleted || formula[*n].deleted {
+                if formula[*p].is_deleted() || formula[*n].is_deleted() {
                     panic!("Deleted clauses used in the DP procedure");
                     continue;
                 }
@@ -478,9 +478,9 @@ impl Preprocess {
 
         *size = ps.len() - 1;
 
-        'outer: for q in &qs.lits {
+        'outer: for q in qs.get_literals() {
             if q.index() != v {
-                for p in &ps.lits {
+                for p in ps.get_literals() {
                     if p.index() != q.index() {
                         if *p == !*q {
                             return false;
@@ -503,9 +503,9 @@ impl Preprocess {
 
         let (ps, qs) = if _ps.len() < _qs.len() { (_qs, _ps) } else { (_ps, _qs) };
 
-        'outer: for q in &qs.lits {
+        'outer: for q in qs.get_literals() {
             if q.index() != v {
-                for p in &ps.lits {
+                for p in ps.get_literals() {
                     if p.index() == q.index() {
                         if *p == !*q {
                             return false;
@@ -518,7 +518,7 @@ impl Preprocess {
             }
         }
 
-        for p in &ps.lits {
+        for p in ps.get_literals() {
             if p.index() != v {
                 out_clause.push(*p);
             }
@@ -534,7 +534,7 @@ impl Preprocess {
 
         // Remove the other places where the clauses are referenced.
         while let Some(cref) = self.occurs[v].pop() {
-            for l in &formula[cref].lits {
+            for l in formula[cref].get_literals() {
                 self.n_occ[l.to_watchidx()] -= 1;
                 if let Some(index) = self.occurs[l.index()].iter().position(|value| *value == cref) {
                     debug!("Found {}", l);

JigSAT/src/solver.rs

@@ -128,7 +128,7 @@ impl Solver {
         clause: Clause, level: u32, target_phase: &mut TargetPhase,
     ) {
         let clause_len = clause.len();
-        let lbd = clause.lbd;
+        let lbd = clause.get_lbd();
         let cref = formula.learn_clause(clause, watches, trail);
 
         self.restart.glucose.update(trail.trail.len(), lbd as usize);

JigSAT/src/unit_prop.rs

@@ -1,4 +1,4 @@
-use crate::{formula::*, lit::*, solver::*, trail::*, watches::*};
+use crate::{formula::*, lit::*, solver::*, trail::*, watches::*, clause::ClauseTrait};
 
 #[inline]
 fn unit_prop_check_rest(
@@ -41,7 +41,7 @@ fn unit_prop_do_outer(
     // At this point we know that none of the watched literals are sat
     let mut k: usize = 2;
     let clause_len: usize = clause.len();
-    let mut search = clause.search;
+    let mut search = clause.get_search_index();
     while k < clause_len {
         search += 1;
         if search == clause_len {
@@ -50,7 +50,7 @@ fn unit_prop_do_outer(
         match unit_prop_check_rest(formula, trail, watches, cref, j, search, lit) {
             Err(_) => {}
             Ok(_) => {
-                formula[cref].search = search;
+                formula[cref].set_search_index(search);
                 return Ok(false);
             }
         }