Skip to content

Commit

Permalink
ditto
Browse files Browse the repository at this point in the history
  • Loading branch information
shnarazk committed Mar 31, 2024
1 parent 7c37e5c commit b3b249d
Show file tree
Hide file tree
Showing 12 changed files with 219 additions and 215 deletions.
28 changes: 15 additions & 13 deletions src/assign/propagate.rs
Original file line number Diff line number Diff line change
Expand Up @@ -454,7 +454,7 @@ impl PropagateIF for AssignStack {
if lit_assign!(self.var[lk.vi()], *lk) != Some(false) {
let new_watch = !*lk;
cdb.detach_watch_cache(propagating, &mut source);
cdb.transform_by_updating_watch(cr, false_watch_pos, k, true);
cdb.transform_by_updating_watch(cr.clone(), false_watch_pos, k, true);
c.search_from = (k + 1) as u16;
debug_assert_ne!(self.assigned(new_watch), Some(true));
check_in!(
Expand All @@ -465,14 +465,14 @@ impl PropagateIF for AssignStack {
}
}
if false_watch_pos == 0 {
cdb.swap_watch(cr);
cdb.swap_watch(cr.clone());
}
}
let c = cr.get();
cdb.transform_by_restoring_watch_cache(propagating, &mut source, updated_cache);
if other_watch_value == Some(false) {
check_in!(cr, Propagate::EmitConflict(self.num_conflict + 1, cached));
conflict_path!(cached, AssignReason::Implication(cr));
conflict_path!(cached, AssignReason::Implication(cr.clone()));
}

#[cfg(feature = "chrono_BT")]
Expand All @@ -488,7 +488,7 @@ impl PropagateIF for AssignStack {
debug_assert!(other_watch_value.is_none());
self.assign_by_implication(
cached,
AssignReason::Implication(cr),
AssignReason::Implication(cr.clone()),
#[cfg(feature = "chrono_BT")]
dl,
);
Expand Down Expand Up @@ -629,7 +629,7 @@ impl PropagateIF for AssignStack {
if lit_assign!(self.var[lk.vi()], *lk) != Some(false) {
let new_watch = !*lk;
cdb.detach_watch_cache(propagating, &mut source);
cdb.transform_by_updating_watch(cr, false_watch_pos, k, true);
cdb.transform_by_updating_watch(cr.clone(), false_watch_pos, k, true);
c.search_from = (k as u16).saturating_add(1);
debug_assert!(
self.assigned(!new_watch) == Some(true)
Expand All @@ -647,7 +647,7 @@ impl PropagateIF for AssignStack {
}
}
if false_watch_pos == 0 {
cdb.swap_watch(cr);
cdb.swap_watch(cr.clone());
}
}
cdb.transform_by_restoring_watch_cache(propagating, &mut source, updated_cache);
Expand All @@ -656,7 +656,7 @@ impl PropagateIF for AssignStack {
cr,
Propagate::SandboxEmitConflict(self.num_conflict, propagating)
);
return Err((cached, AssignReason::Implication(cr)));
return Err((cached, AssignReason::Implication(cr.clone())));
}

#[cfg(feature = "chrono_BT")]
Expand All @@ -672,7 +672,7 @@ impl PropagateIF for AssignStack {

self.assign_by_implication(
cached,
AssignReason::Implication(cr),
AssignReason::Implication(cr.clone()),
#[cfg(feature = "chrono_BT")]
dl,
);
Expand Down Expand Up @@ -715,13 +715,15 @@ impl AssignStack {
let mut num_propagated = 0;
while num_propagated < self.trail.len() {
num_propagated = self.trail.len();
for cr in cdb.iter() {
let c = cr.get();
let copied = cdb.iter().cloned().collect::<Vec<_>>();
for cr in copied.iter() {
let writer = cr.clone();
let c = writer.get();
if c.is_dead() {
continue;
}
debug_assert!(c.iter().all(|l| !self.var[l.vi()].is(FlagVar::ELIMINATED)));
match cdb.transform_by_simplification(self, *cr) {
match cdb.transform_by_simplification(self, writer.clone()) {
RefClause::Clause(_) => (),
RefClause::Dead => (), // was a satisfied clause
RefClause::EmptyClause => return Err(SolverError::EmptyClause),
Expand All @@ -730,7 +732,7 @@ impl AssignStack {
debug_assert!(self.assigned(lit).is_none());
cdb.certificate_add_assertion(lit);
self.assign_at_root_level(lit)?;
cdb.remove_clause(*cr);
cdb.remove_clause(writer);
}
}
}
Expand All @@ -749,7 +751,7 @@ impl AssignStack {
let vi = l.vi();
let var = &self.var[vi];
if let Some(b) = var.assign {
self.best_phases.insert(vi, (b, var.reason));
self.best_phases.insert(vi, (b, var.reason.clone()));
}
}
}
Expand Down
14 changes: 7 additions & 7 deletions src/assign/trail_saving.rs
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ impl TrailSavingIF for AssignStack {
// }

self.trail_saved.push(l);
self.reason_saved[vi] = self.var[vi].reason;
self.reason_saved[vi] = self.var[vi].reason.clone();
self.reward_at_unassign(vi);
if activity_threshold <= self.var[vi].reward {
self.insert_heap(vi);
Expand All @@ -63,12 +63,12 @@ impl TrailSavingIF for AssignStack {
for i in (0..self.trail_saved.len()).rev() {
let lit = self.trail_saved[i];
let vi = lit.vi();
let old_reason = self.reason_saved[vi];
match (self.assigned(lit), old_reason) {
let old_reason = self.reason_saved[vi].clone();
match (self.assigned(lit), &old_reason) {
(Some(true), _) => (),
(None, AssignReason::BinaryLink(link)) => {
debug_assert_ne!(link.vi(), lit.vi());
debug_assert_eq!(self.assigned(link), Some(true));
debug_assert_eq!(self.assigned(*link), Some(true));
self.num_repropagation += 1;

self.assign_by_implication(
Expand Down Expand Up @@ -101,7 +101,7 @@ impl TrailSavingIF for AssignStack {
}
(Some(false), AssignReason::BinaryLink(link)) => {
debug_assert_ne!(link.vi(), lit.vi());
debug_assert_eq!(self.assigned(link), Some(true));
debug_assert_eq!(self.assigned(*link), Some(true));
let _ = self.truncate_trail_saved(i + 1); // reduce heap ops.
self.clear_saved_trail();
return Err((lit, old_reason));
Expand All @@ -111,10 +111,10 @@ impl TrailSavingIF for AssignStack {
debug_assert!(c.iter().all(|l| self.assigned(*l) == Some(false)));
let _ = self.truncate_trail_saved(i + 1); // reduce heap ops.
self.clear_saved_trail();
return Err((c.lit0(), AssignReason::Implication(cr)));
return Err((c.lit0(), AssignReason::Implication(cr.clone())));
}
(_, AssignReason::Decision(lvl)) => {
debug_assert_ne!(0, lvl);
debug_assert_ne!(0, *lvl);
self.insert_heap(vi);
return self.truncate_trail_saved(i + 1);
}
Expand Down
10 changes: 5 additions & 5 deletions src/cdb/binary.rs
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,7 @@ impl Instantiate for BinaryLinkDB {

pub trait BinaryLinkIF {
/// add a mapping from a pair of Lit to a `ClauseRef`
fn add(&mut self, lit0: Lit, lit1: Lit, cid: ClauseRef);
fn add(&mut self, lit0: Lit, lit1: Lit, cr: ClauseRef);
/// remove a pair of `Lit`s
fn remove(&mut self, lit0: Lit, lit1: Lit) -> MaybeInconsistent;
/// return 'ClauseRef` linked from a pair of `Lit`s
Expand All @@ -69,12 +69,12 @@ pub trait BinaryLinkIF {
}

impl BinaryLinkIF for BinaryLinkDB {
fn add(&mut self, lit0: Lit, lit1: Lit, cid: ClauseRef) {
fn add(&mut self, lit0: Lit, lit1: Lit, cr: ClauseRef) {
let l0 = lit0.min(lit1);
let l1 = lit0.max(lit1);
self.hash.insert((l0, l1), cid);
self.list[lit0].push((lit1, cid));
self.list[lit1].push((lit0, cid));
self.hash.insert((l0, l1), cr.clone());
self.list[lit0].push((lit1, cr.clone()));
self.list[lit1].push((lit0, cr.clone()));
}
fn remove(&mut self, lit0: Lit, lit1: Lit) -> MaybeInconsistent {
let l0 = lit0.min(lit1);
Expand Down
Loading

0 comments on commit b3b249d

Please sign in to comment.