Skip to content

Commit

Permalink
another snapshot
Browse files Browse the repository at this point in the history
  • Loading branch information
@shnarazk
shnarazk committed Mar 31, 2024
1 parent 4f3494b commit 4514d9c
Show file tree
Hide file tree
Showing 6 changed files with 33 additions and 34 deletions.
16 changes: 10 additions & 6 deletions src/assign/propagate.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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(
Expand Down Expand Up @@ -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<Lit> = None;
if Some(true) == other_watch_value {
Expand All @@ -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 {
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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)
Expand All @@ -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);
Expand Down
8 changes: 3 additions & 5 deletions src/cdb/cref.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ impl Ord for ClauseRef {

impl PartialOrd for ClauseRef {
fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
Some(self.cmp(&other))
Some(self.cmp(other))
}
}

Expand Down Expand Up @@ -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()
Expand Down
1 change: 0 additions & 1 deletion src/cdb/db.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
2 changes: 1 addition & 1 deletion src/cdb/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<Box<Clause>>,
c: Rc<Clause>,
}

/// A representation of 'clause'
Expand Down
8 changes: 4 additions & 4 deletions src/processor/simplify.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}
Expand Down Expand Up @@ -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);
}
}
Expand Down
32 changes: 15 additions & 17 deletions src/solver/conflict.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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);
Expand All @@ -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..] {
Expand Down Expand Up @@ -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<Lit>,
_mes: &str,
) -> DecisionLevel {
fn lit_level(asg: &AssignStack, lit: Lit, bag: &mut Vec<Lit>, _mes: &str) -> DecisionLevel {
if bag.contains(&lit) {
return 0;
}
Expand Down Expand Up @@ -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."),
}
}
Expand Down

0 comments on commit 4514d9c

Please sign in to comment.