From 4514d9c18d188cce34e05622a8131937086fb7d6 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Mon, 1 Apr 2024 07:13:52 +0900 Subject: [PATCH] another snapshot --- src/assign/propagate.rs | 16 ++++++++++------ src/cdb/cref.rs | 8 +++----- src/cdb/db.rs | 1 - src/cdb/mod.rs | 2 +- src/processor/simplify.rs | 8 ++++---- src/solver/conflict.rs | 32 +++++++++++++++----------------- 6 files changed, 33 insertions(+), 34 deletions(-) diff --git a/src/assign/propagate.rs b/src/assign/propagate.rs index 884a360bf..44db3a98d 100644 --- a/src/assign/propagate.rs +++ b/src/assign/propagate.rs @@ -81,7 +81,7 @@ impl PropagateIF for AssignStack { // self.make_var_asserted(vi); Ok(()) } - _ => Err(SolverError::RootLevelConflict((l, var.reason))), + _ => Err(SolverError::RootLevelConflict((l, var.reason.clone()))), } } fn assign_by_implication( @@ -401,6 +401,7 @@ impl PropagateIF for AssignStack { ); // assert_ne!(other_watch.vi(), false_lit.vi()); // assert!(other_watch == cdb[cr].lit0() || other_watch == cdb[cr].lit1()); + let cr = cr.clone(); let mut other_watch_value = lit_assign!(self.var[cached.vi()], cached); let mut updated_cache: Option = None; if Some(true) == other_watch_value { @@ -414,7 +415,8 @@ impl PropagateIF for AssignStack { continue 'next_clause; } { - let c = cr.get(); + let mut writer = cr.clone(); + let c = writer.get_mut(); let lit0 = c.lit0(); let lit1 = c.lit1(); let (false_watch_pos, other) = if false_lit == lit1 { @@ -577,11 +579,13 @@ impl PropagateIF for AssignStack { //## normal clause loop // let mut source = cdb.watch_cache_iter(propagating); - 'next_clause: while let Some((cr, mut cached)) = source + 'next_clause: while let Some((cr0, mut cached)) = source .next() .map(|index| cdb.fetch_watch_cache_entry(propagating, index)) { - let c = cr.get(); + let cr1 = cr0.clone(); + let mut cr = cr0.clone(); + let c = cr.get_mut(); if c.is_dead() { cdb.transform_by_restoring_watch_cache(propagating, &mut source, None); continue; @@ -629,7 +633,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.clone(), false_watch_pos, k, true); + cdb.transform_by_updating_watch(cr1.clone(), false_watch_pos, k, true); c.search_from = (k as u16).saturating_add(1); debug_assert!( self.assigned(!new_watch) == Some(true) @@ -647,7 +651,7 @@ impl PropagateIF for AssignStack { } } if false_watch_pos == 0 { - cdb.swap_watch(cr.clone()); + cdb.swap_watch(cr1.clone()); } } cdb.transform_by_restoring_watch_cache(propagating, &mut source, updated_cache); diff --git a/src/cdb/cref.rs b/src/cdb/cref.rs index 9c213ccf0..e7d3cec61 100644 --- a/src/cdb/cref.rs +++ b/src/cdb/cref.rs @@ -21,7 +21,7 @@ impl Ord for ClauseRef { impl PartialOrd for ClauseRef { fn partial_cmp(&self, other: &Self) -> Option { - Some(self.cmp(&other)) + Some(self.cmp(other)) } } @@ -65,12 +65,10 @@ impl fmt::Display for ClauseRef { impl ClauseRefIF for ClauseRef { fn new(c: Clause) -> Self { - ClauseRef { - c: Rc::new(Box::new(c)), - } + ClauseRef { c: Rc::new(c) } } fn get(&self) -> &Clause { - &**self.c + &self.c } fn get_mut(&mut self) -> &mut Clause { Rc::get_mut(&mut self.c).unwrap() diff --git a/src/cdb/db.rs b/src/cdb/db.rs index 35db96b2f..56ecbbe27 100644 --- a/src/cdb/db.rs +++ b/src/cdb/db.rs @@ -1001,7 +1001,6 @@ impl ClauseDBIF for ClauseDB { && !c.is_dead() && (self.co_lbd_bound as usize) < c.lits.len() { - drop(c); remove_clause_fn( &mut self.clause, &mut self.certification_store, diff --git a/src/cdb/mod.rs b/src/cdb/mod.rs index 1444b9636..f69af9c94 100644 --- a/src/cdb/mod.rs +++ b/src/cdb/mod.rs @@ -191,7 +191,7 @@ pub trait ClauseDBIF: /// Note: ids are re-used after 'garbage collection'. #[derive(Clone, Eq, Hash, PartialEq)] pub struct ClauseRef { - c: Rc>, + c: Rc, } /// A representation of 'clause' diff --git a/src/processor/simplify.rs b/src/processor/simplify.rs index cc6d09b22..88d6b3e29 100644 --- a/src/processor/simplify.rs +++ b/src/processor/simplify.rs @@ -588,11 +588,11 @@ impl Eliminator { if bool::from(l) { debug_assert_eq!(w.pos_occurs.iter().filter(|&c| *c == *cr).count(), 1); w.pos_occurs.delete_unstable(|c| c == cr); - debug_assert!(!w.pos_occurs.contains(&cr)); + debug_assert!(!w.pos_occurs.contains(cr)); } else { debug_assert_eq!(w.neg_occurs.iter().filter(|&c| *c == *cr).count(), 1); w.neg_occurs.delete_unstable(|c| c == cr); - debug_assert!(!w.neg_occurs.contains(&cr)); + debug_assert!(!w.neg_occurs.contains(cr)); } self.enqueue_var(asg, l.vi(), true); } @@ -666,10 +666,10 @@ fn check_eliminator(cdb: &impl ClauseDBIF, elim: &Eliminator) -> bool { for l in c.iter() { let v = l.vi(); if bool::from(*l) { - if !elim[v].pos_occurs.contains(&cr) { + if !elim[v].pos_occurs.contains(cr) { panic!("failed to check {}", cr); } - } else if !elim[v].neg_occurs.contains(&cr) { + } else if !elim[v].neg_occurs.contains(cr) { panic!("failed to check {}", cr); } } diff --git a/src/solver/conflict.rs b/src/solver/conflict.rs index 10812e8c2..efc9b4710 100644 --- a/src/solver/conflict.rs +++ b/src/solver/conflict.rs @@ -104,7 +104,10 @@ pub fn handle_conflict( // asg.lift_to_asserted(l0.vi()); } Some(false) if asg.level(l0.vi()) == asg.root_level() => { - return Err(SolverError::RootLevelConflict((l0, *asg.reason(l0.vi())))); + return Err(SolverError::RootLevelConflict(( + l0, + asg.reason(l0.vi()).clone(), + ))); } _ => { // dump to certified even if it's a literal. @@ -149,7 +152,8 @@ pub fn handle_conflict( } } AssignReason::Implication(r) => { - for l in r.get().iter() { + let reader = r.clone(); + for l in reader.get().iter() { let vi = l.vi(); if !bumped.contains(&vi) { asg.reward_at_analysis(vi); @@ -442,7 +446,7 @@ fn conflict_analyze( } debug_assert!(0 < trail_index); trail_index -= 1; - reason = *asg.reason(p.vi()); + reason = asg.reason(p.vi()).clone(); } if let Some(cid) = cid_with_max_lbd { cdb.update_at_analysis(asg, cid); @@ -511,7 +515,7 @@ impl Lit { let mut stack = vec![self]; let top = clear.len(); while let Some(sl) = stack.pop() { - match asg.reason(sl.vi()) { + match asg.reason(sl.vi()).clone() { AssignReason::BinaryLink(l) => { let vi = l.vi(); let lv = asg.level(vi); @@ -523,8 +527,8 @@ impl Lit { ) && levels[lv as usize] { asg.var_mut(vi).turn_on(FlagVar::CA_SEEN); - stack.push(*l); - clear.push(*l); + stack.push(l); + clear.push(l); } else { // one of the roots is a decision var at an unchecked level. for l in &clear[top..] { @@ -569,21 +573,15 @@ impl Lit { } #[allow(dead_code)] -fn check_graph(asg: &AssignStack, cdb: &ClauseDB, lit: Lit, mes: &str) { +fn check_graph(asg: &AssignStack, lit: Lit, mes: &str) { let its_level = asg.level(lit.vi()); let mut children = Vec::new(); - let precedents = lit_level(asg, cdb, lit, &mut children, mes); + let precedents = lit_level(asg, lit, &mut children, mes); assert!(precedents <= its_level); } #[allow(dead_code)] -fn lit_level( - asg: &AssignStack, - cdb: &ClauseDB, - lit: Lit, - bag: &mut Vec, - _mes: &str, -) -> DecisionLevel { +fn lit_level(asg: &AssignStack, lit: Lit, bag: &mut Vec, _mes: &str) -> DecisionLevel { if bag.contains(&lit) { return 0; } @@ -614,11 +612,11 @@ fn lit_level( cr.get() .iter() .skip(1) - .map(|l| lit_level(asg, cdb, !*l, bag, _mes)) + .map(|l| lit_level(asg, !*l, bag, _mes)) .max() .unwrap() } - AssignReason::BinaryLink(b) => lit_level(asg, cdb, *b, bag, _mes), + AssignReason::BinaryLink(b) => lit_level(asg, *b, bag, _mes), AssignReason::None => panic!("One of root of {lit} isn't assigned."), } }