diff --git a/Cargo.toml b/Cargo.toml index cad3a60..acfee24 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,5 +1,5 @@ - [workspace] +resolver = "2" members = [ "src/batsat", diff --git a/src/batsat/Cargo.toml b/src/batsat/Cargo.toml index 6767568..15b9607 100644 --- a/src/batsat/Cargo.toml +++ b/src/batsat/Cargo.toml @@ -9,7 +9,7 @@ readme = "../../README.md" keywords = ["sat", "minisat"] categories = ["algorithms"] license = "MIT" -edition = "2018" +edition = "2021" publish = true diff --git a/src/batsat/src/clause.rs b/src/batsat/src/clause.rs index 1f386d7..5f32e80 100644 --- a/src/batsat/src/clause.rs +++ b/src/batsat/src/clause.rs @@ -24,7 +24,7 @@ use { alloc::{self, RegionAllocator}, intmap::{AsIndex, IntMap, IntMapBool, IntSet}, }, - std::{fmt, iter::DoubleEndedIterator, ops, slice, u32}, + std::{fmt, iter::DoubleEndedIterator, ops, slice}, }; #[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)] @@ -42,7 +42,7 @@ impl fmt::Debug for Var { } impl Var { - pub const UNDEF: Var = Var(!0); + pub const UNDEF: Var = Var(u32::MAX / 2); #[inline(always)] pub(crate) fn from_idx(idx: u32) -> Self { debug_assert!(idx < u32::MAX / 2, "Var::from_idx: index too large"); diff --git a/src/batsat/src/core.rs b/src/batsat/src/core.rs index 26bb69a..e88f1ea 100644 --- a/src/batsat/src/core.rs +++ b/src/batsat/src/core.rs @@ -25,10 +25,10 @@ use { self, lbool, CRef, ClauseAllocator, ClauseRef, DeletePred, LSet, Lit, OccLists, OccListsData, VMap, Var, }, + crate::heap::{CachedKeyComparator, Heap, HeapData}, crate::interface::SolverInterface, - crate::intmap::{Comparator, Heap, HeapData}, crate::theory::Theory, - std::{cmp, f64, fmt, i32, mem}, + std::{cmp, fmt, mem}, }; #[cfg(feature = "logging")] @@ -65,14 +65,16 @@ pub struct Solver { /// The current assignments. struct VarState { /// A heuristic measurement of the activity of a variable. - activity: VMap, + activity: VMap, + /// A priority queue of variables ordered with respect to the variable activity. + order_heap_data: HeapData, /// Current assignment for each variable. ass: VMap, /// Stores reason and level for each variable. vardata: VMap, /// Amount to bump next variable with. - var_inc: f64, - var_decay: f64, + var_inc: f32, + var_decay: f32, /// Assignment stack; stores all assigments made in the order they were made. trail: Vec, @@ -116,6 +118,8 @@ struct SolverV { // v.activity: VMap, // /// The current assignments. // v.assigns: VMap, + // /// A priority queue of variables ordered with respect to the variable activity. + // v.order_heap_data: HeapData, /// The preferred polarity of each variable. polarity: VMap, /// The users preferred polarity of each variable. @@ -125,8 +129,6 @@ struct SolverV { // /// Stores reason and level for each variable. /// `watches[lit]` is a list of constraints watching 'lit' (will go there if literal becomes true). watches_data: OccListsData, - /// A priority queue of variables ordered with respect to the variable activity. - order_heap_data: HeapData, /// If `false`, the constraints are already unsatisfiable. No part of the solver state may be used! ok: bool, /// Amount to bump next clause with. @@ -297,9 +299,11 @@ impl SolverInterface for Solver { th: &mut Th, assumps: &[Lit], ) -> lbool { - self.v.assumptions.clear(); + let old_len = self.v.assumptions.len(); self.v.assumptions.extend_from_slice(assumps); - self.solve_internal(th) + let res = self.solve_internal(th); + self.v.assumptions.truncate(old_len); + res } fn pop_model(&mut self, th: &mut Th) { @@ -389,6 +393,18 @@ impl SolverInterface for Solver { fn proved_at_lvl_0(&self) -> &[Lit] { self.v.vars.proved_at_lvl_0() } + + fn set_decision_var(&mut self, v: Var, dvar: bool) { + self.v.set_decision_var(v, dvar) + } + + fn assumptions(&mut self) -> &[Lit] { + &self.v.assumptions + } + + fn assumptions_mut(&mut self) -> &mut Vec { + &mut self.v.assumptions + } } impl Default for Solver { @@ -459,7 +475,6 @@ impl Solver { self.remove_satisfied(ClauseSetSelect::Original); // remove satisfied normal clauses } self.check_garbage(); - self.v.rebuild_order_heap(); self.v.simp_db_assigns = self.v.num_assigns() as i32; // (shouldn't depend on stats really, but it will do for now) @@ -701,6 +716,9 @@ impl Solver { TheoryCall::Final => th.final_check(&mut th_arg), } if let TheoryConflict::Clause { costly } = th_arg.conflict { + if th_arg.lits.is_empty() { + return Err(ConflictAtLevel0); + } // borrow magic let mut local_confl_cl = vec![]; mem::swap(&mut local_confl_cl, th_arg.lits); @@ -1124,9 +1142,7 @@ impl SolverV { } fn order_heap(&mut self) -> Heap { - self.order_heap_data.promote(VarOrder { - activity: &self.vars.activity, - }) + self.vars.order_heap() } fn set_decision_var(&mut self, v: Var, b: bool) { @@ -1177,9 +1193,9 @@ impl SolverV { { let idx_tmp = utils::irand( &mut self.opts.random_seed, - self.order_heap_data.len() as i32, + self.vars.order_heap_data.len() as i32, ) as usize; - next = self.order_heap_data[idx_tmp]; + next = self.vars.order_heap_data[idx_tmp].var(); if self.value(next) == lbool::UNDEF && self.decision[next] { self.rnd_decisions += 1; } @@ -1225,9 +1241,10 @@ impl SolverV { .vardata .insert_default(v, VarData::new(CRef::UNDEF, 0)); if self.opts.rnd_init_act { - self.vars - .activity - .insert_default(v, utils::drand(&mut self.opts.random_seed) * 0.00001); + self.vars.activity.insert_default( + v, + (utils::drand(&mut self.opts.random_seed) * 0.00001) as f32, + ); } else { self.vars.activity.insert_default(v, 0.0); } @@ -1391,8 +1408,7 @@ impl SolverV { let lvl = self.vars.level(q.var()); assert!(lvl <= conflict_level); if !self.seen[q.var()].is_seen() && lvl > 0 { - self.vars - .var_bump_activity(&mut self.order_heap_data, q.var()); + self.vars.var_bump_activity(q.var()); self.seen[q.var()] = Seen::SOURCE; if lvl == conflict_level { // at conflict level: need to eliminate this lit by resolution @@ -1599,7 +1615,7 @@ impl SolverV { out_conflict.insert(!lit); } else if reason == CRef::SPECIAL { // resolution with propagation reason - let lits = th.explain_propagation(lit); + let lits = th.explain_propagation_final(lit); for &p in lits { if self.vars.level(p.var()) > 0 { self.seen[p.var()] = Seen::SOURCE; @@ -1789,16 +1805,6 @@ impl SolverV { confl } - fn rebuild_order_heap(&mut self) { - let mut vs = vec![]; - for v in (0..self.num_vars()).map(Var::from_idx) { - if self.decision[v] && self.value(v) == lbool::UNDEF { - vs.push(v); - } - } - self.order_heap().build(&vs); - } - /// Sort literals of `clause` so that unassigned literals are first, /// followed by literals in decreasing assignment level fn sort_clause_lits(&self, clause: &mut [Lit]) { @@ -1927,7 +1933,7 @@ impl SolverV { debug_assert!(self.decision_level() > level); let trail_lim_last = *self.vars.trail_lim.last().expect("trail_lim is empty") as usize; let trail_lim_level = self.vars.trail_lim[level as usize] as usize; - for c in (trail_lim_level..self.vars.trail.len()).rev() { + for c in trail_lim_level..self.vars.trail.len() { let x = self.vars.trail[c].var(); self.vars.ass[x] = lbool::UNDEF; if self.opts.phase_saving > 1 || (self.opts.phase_saving == 1 && c > trail_lim_last) { @@ -1936,10 +1942,10 @@ impl SolverV { self.insert_var_order(x); } self.qhead = trail_lim_level as i32; - self.vars.trail.resize(trail_lim_level, Lit::UNDEF); + self.vars.trail.truncate(trail_lim_level); // eprintln!("decision_level {} -> {}", self.trail_lim.len(), level); self.th_st.clear(); - self.vars.trail_lim.resize(level as usize, 0); + self.vars.trail_lim.truncate(level as usize); } /// Detach a clause from watcher lists. @@ -2074,7 +2080,6 @@ impl SolverV { decision: VMap::new(), // v.vardata: VMap::new(), watches_data: OccListsData::new(), - order_heap_data: HeapData::new(), ok: true, cla_inc: 1.0, // v.var_inc: 1.0, @@ -2105,6 +2110,16 @@ impl SolverV { } } +/// Large f32 that is still small enough that it can't cause another f32 to overflow to infinity +const THRESHOLD: f32 = 1.0141204e31; +#[test] +fn test_threshold() { + let f = f32::MAX * 2.0f32.powi(-1 - (f32::MANTISSA_DIGITS as i32)); + assert_eq!(THRESHOLD, f); + // adding THRESHOLD to a float can never make it overflow to infinity + assert_eq!(f32::MAX + THRESHOLD, f32::MAX) +} + impl VarState { fn new(opts: &SolverOpts) -> Self { Self { @@ -2115,6 +2130,7 @@ impl VarState { var_decay: opts.var_decay, trail: vec![], trail_lim: vec![], + order_heap_data: HeapData::new(), } } @@ -2160,6 +2176,17 @@ impl VarState { fn var_decay_activity(&mut self) { self.var_inc *= 1.0 / self.var_decay; + if self.var_inc > THRESHOLD { + let scale = 2.0_f32.powi(f32::MIN_EXP); + // Rescale: + for (_, x) in self.activity.iter_mut() { + *x *= scale; + } + for x in self.order_heap_data.heap_mut().iter_mut() { + x.scale_activity(scale) + } + self.var_inc *= scale; + } } #[inline(always)] @@ -2179,21 +2206,18 @@ impl VarState { self.trail.push(p); } + fn order_heap(&mut self) -> Heap { + self.order_heap_data.promote(VarOrder { + activity: &self.activity, + }) + } + /// Increase a variable with the current 'bump' value. - fn var_bump_activity(&mut self, order_heap_data: &mut HeapData, v: Var) { + fn var_bump_activity(&mut self, v: Var) { self.activity[v] += self.var_inc; - if self.activity[v] > 1e100 { - // Rescale: - for (_, x) in self.activity.iter_mut() { - *x *= 1e-100; - } - self.var_inc *= 1e-100; - } // Update order_heap with respect to new activity: - let mut order_heap = order_heap_data.promote(VarOrder { - activity: &self.activity, - }); + let mut order_heap = self.order_heap(); if order_heap.in_heap(v) { order_heap.decrease(v); } @@ -2292,9 +2316,6 @@ impl<'a> TheoryArg<'a> { /// This is a hint for the SAT solver to keep the theory lemma that corresponds /// to `c` along with the actual learnt clause. pub fn raise_conflict(&mut self, lits: &[Lit], costly: bool) { - if lits.len() == 0 { - panic!("conflicts must have a least one literal") - } if self.is_ok() { self.conflict = TheoryConflict::Clause { costly }; self.lits.clear(); @@ -2322,7 +2343,7 @@ struct Watcher { } struct VarOrder<'a> { - activity: &'a VMap, + activity: &'a VMap, } /// Predicate to test whether a clause has been removed from some lit's watchlist @@ -2339,8 +2360,6 @@ enum Seen { } mod utils { - use super::*; - /// Finite subsequences of the Luby-sequence: /// /// > 0: 1 @@ -2405,12 +2424,42 @@ impl PartialEq for Watcher { } impl Eq for Watcher {} -impl<'a> Comparator for VarOrder<'a> { - fn cmp(&self, lhs: &Var, rhs: &Var) -> cmp::Ordering { - PartialOrd::partial_cmp(&self.activity[*rhs], &self.activity[*lhs]).expect("NaN activity") +#[derive(Copy, Clone, Ord, PartialOrd, Eq, PartialEq)] +struct VarOrderKey(u64); + +impl VarOrderKey { + #[inline] + fn new(var: Var, activity: f32) -> Self { + VarOrderKey((!(activity.to_bits() as u64) << u32::BITS) | (var.idx() as u64)) + } + + fn var(self) -> Var { + Var::unsafe_from_idx(self.0 as u32) + } + + fn activity(self) -> f32 { + f32::from_bits(!((self.0 >> u32::BITS) as u32)) + } + + fn scale_activity(&mut self, scale: f32) { + *self = VarOrderKey::new(self.var(), self.activity() * scale) } } +impl<'a> CachedKeyComparator for VarOrder<'a> { + type Key = VarOrderKey; + + fn cache_key(&self, t: Var) -> Self::Key { + VarOrderKey::new(t, self.activity[t]) + } + fn max_key(&self) -> Self::Key { + VarOrderKey::new(Var::UNDEF, 0.0) + } + + fn un_cache_key(&self, k: Self::Key) -> Var { + k.var() + } +} impl<'a> DeletePred for WatcherDeleted<'a> { #[inline] fn deleted(&self, w: &Watcher) -> bool { @@ -2447,7 +2496,7 @@ impl Watcher { /// This can be used to tune the solver heuristics. #[derive(Clone)] pub struct SolverOpts { - pub var_decay: f64, + pub var_decay: f32, pub clause_decay: f64, pub random_var_freq: f64, pub random_seed: f64, @@ -2500,7 +2549,7 @@ impl Default for SolverOpts { impl SolverOpts { /// Check that options are valid. pub fn check(&self) -> bool { - (0.0 < self.var_decay && self.var_decay < 1.0) + (1f32 / THRESHOLD < self.var_decay && self.var_decay < 1.0) && (0.0 < self.clause_decay && self.clause_decay < 1.0) && (0.0 <= self.random_var_freq && self.random_var_freq <= 1.0) && (0.0 < self.random_seed && self.random_seed < f64::INFINITY) diff --git a/src/batsat/src/heap.rs b/src/batsat/src/heap.rs new file mode 100644 index 0000000..ccb07a6 --- /dev/null +++ b/src/batsat/src/heap.rs @@ -0,0 +1,210 @@ +use crate::intmap::{AsIndex, IntMap}; +use std::fmt::Debug; +use std::{mem, ops}; + +/// Quaternary Heap +#[derive(Debug, Clone)] +pub struct HeapData { + heap: Box<[V]>, + next_slot: usize, + indices: IntMap, +} + +impl Default for HeapData { + fn default() -> Self { + Self { + heap: Box::new([]), + next_slot: 0, + indices: IntMap::new(), + } + } +} + +impl HeapData { + pub fn new() -> Self { + Self::default() + } + pub fn len(&self) -> usize { + self.heap.len() + } + pub fn is_empty(&self) -> bool { + self.next_slot <= ROOT as usize + } + pub fn in_heap(&self, k: K) -> bool { + self.indices.has(k) && self.indices[k] >= 0 + } + + pub fn promote>(&mut self, comp: Comp) -> Heap { + Heap { data: self, comp } + } + + /// Raw mutable access to all the elements of the heap + pub(crate) fn heap_mut(&mut self) -> &mut [V] { + if self.next_slot == 0 { + &mut [] + } else { + &mut self.heap[ROOT as usize..self.next_slot] + } + } +} + +impl ops::Index for HeapData { + type Output = V; + fn index(&self, index: usize) -> &Self::Output { + &self.heap[index] + } +} + +pub trait CachedKeyComparator { + type Key: Ord + Copy; + + fn cache_key(&self, t: T) -> Self::Key; + + fn max_key(&self) -> Self::Key; + + fn un_cache_key(&self, k: Self::Key) -> T; +} + +#[derive(Debug)] +pub struct Heap<'a, K: AsIndex + 'a, Comp: CachedKeyComparator> { + data: &'a mut HeapData, + comp: Comp, +} + +impl<'a, K: AsIndex + 'a, Comp: CachedKeyComparator> ops::Deref for Heap<'a, K, Comp> { + type Target = HeapData; + fn deref(&self) -> &Self::Target { + &self.data + } +} +impl<'a, K: AsIndex + 'a, Comp: CachedKeyComparator> ops::DerefMut for Heap<'a, K, Comp> { + fn deref_mut(&mut self) -> &mut Self::Target { + &mut self.data + } +} + +impl<'a, K: AsIndex + 'a, Comp: CachedKeyComparator> Heap<'a, K, Comp> { + // ensure size is always a multiple of 4 + #[cold] + #[inline(never)] + fn heap_reserve(&mut self) { + debug_assert_eq!(self.next_slot, self.data.len()); + if self.next_slot == 0 { + self.next_slot = ROOT as usize; + // Enough space for the root and 4 children + self.heap = vec![self.comp.max_key(); 8].into_boxed_slice(); + } else { + let new_size = self.next_slot << 2; + let mut heap = mem::replace(&mut self.heap, Box::new([])).into_vec(); + heap.resize(new_size, self.comp.max_key()); + self.heap = heap.into_boxed_slice(); + } + } + + #[inline] + fn heap_push(&mut self, k: Comp::Key) -> u32 { + if self.next_slot >= self.heap.len() { + self.heap_reserve(); + assert!(self.next_slot < self.heap.len()); + } + let slot = self.next_slot; + self.heap[slot] = k; + self.next_slot += 1; + slot as u32 + } + + fn percolate_up(&mut self, mut i: u32) { + let x = self.heap[i as usize]; + let mut p = parent_index(i); + + while i != ROOT && x < self.heap[p as usize] { + self.heap[i as usize] = self.heap[p as usize]; + let tmp = self.heap[p as usize]; + self.data.indices[self.comp.un_cache_key(tmp)] = i as i32; + i = p; + p = parent_index(p); + } + self.heap[i as usize] = x; + self.data.indices[self.comp.un_cache_key(x)] = i as i32; + } + + fn percolate_down(&mut self, mut i: u32) { + let x = self.heap[i as usize]; + let len = (self.next_slot + 3) & (usize::MAX - 3); // round up to nearest multiple of 4 + // since the heap is padded with maximum values we can pretend that these are part of the + // heap but never swap with them + let heap = &mut self.data.heap[..len]; + loop { + let min = |x: (u32, Comp::Key), y: (u32, Comp::Key)| if x.1 < y.1 { x } else { y }; + let left_index = left_index(i); + let Some(arr) = heap.get(left_index as usize..left_index as usize + 4) else { + break; + }; + let bundle = |x| (left_index + x, arr[x as usize]); + let b0 = bundle(0); + let b1 = bundle(1); + let b2 = bundle(2); + let b3 = bundle(3); + let b01 = min(b0, b1); + let b23 = min(b2, b3); + let (child, min) = min(b01, b23); + if min > x { + break; + } + heap[i as usize] = min; + self.data.indices[self.comp.un_cache_key(min)] = i as i32; + i = child; + } + heap[i as usize] = x; + self.data.indices[self.comp.un_cache_key(x)] = i as i32; + } + + pub fn decrease(&mut self, k: K) { + debug_assert!(self.in_heap(k)); + let k_index = self.indices[k]; + self.heap[k_index as usize] = self.comp.cache_key(k); + self.percolate_up(k_index as u32); + } + + pub fn insert(&mut self, k: K) { + self.indices.reserve(k, -1); + debug_assert!(!self.in_heap(k)); + let k_index = self.heap_push(self.comp.cache_key(k)); + self.indices[k] = k_index as i32; + self.percolate_up(k_index); + } + + pub fn remove_min(&mut self) -> K { + assert!(!self.is_empty(), "cannot pop from empty heap"); + let x = self.heap[ROOT as usize]; + let last = self.next_slot - 1; + self.next_slot = last; + let x_var = self.comp.un_cache_key(x); + self.indices[x_var] = -1; + if self.is_empty() { + self.heap[last] = self.comp.max_key(); + return x_var; + } + let lastval = self.heap[last]; + self.heap[last] = self.comp.max_key(); + self.heap[ROOT as usize] = lastval; + self.data.indices[self.comp.un_cache_key(lastval)] = ROOT as i32; + self.percolate_down(ROOT); + self.comp.un_cache_key(x) + } +} + +/// Root of the quaternary heap +/// By using 3 as the root we ensure each chunk of 4 children has a multiple of 4 starting index +/// This gives the chunks a better chance of being cache aligned, i.e. they are cache aligned if +/// the allocation is cache aligned +const ROOT: u32 = 3; + +#[inline(always)] +fn left_index(i: u32) -> u32 { + (i - 2) << 2 +} +#[inline(always)] +fn parent_index(i: u32) -> u32 { + (i >> 2) + 2 +} diff --git a/src/batsat/src/interface.rs b/src/batsat/src/interface.rs index babc1ec..e445107 100644 --- a/src/batsat/src/interface.rs +++ b/src/batsat/src/interface.rs @@ -152,6 +152,18 @@ pub trait SolverInterface { /// /// Precondition: last result was `Unsat` fn unsat_core_contains_var(&self, v: Var) -> bool; + + /// Sets if a variable can be used in decisions + /// (NOTE! This has effects on the meaning of a SATISFIABLE result). + fn set_decision_var(&mut self, v: Var, dvar: bool); + + /// Get access to the set of assumptions that will be implicitly added to calls to + /// [`SolverInterface::solve_limited_th`] + fn assumptions(&mut self) -> &[Lit]; + + /// Get mutable access to the set of assumptions that will be implicitly added to calls to + /// [`SolverInterface::solve_limited_th`] + fn assumptions_mut(&mut self) -> &mut Vec; } /// Result of calling [`SolverInterface::solve_limited_th_full`], contains the unsat-core diff --git a/src/batsat/src/intmap.rs b/src/batsat/src/intmap.rs index f1f48ff..1a64c6e 100644 --- a/src/batsat/src/intmap.rs +++ b/src/batsat/src/intmap.rs @@ -20,7 +20,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA **************************************************************************************************/ use bit_vec::BitVec; -use std::cmp; use std::iter; use std::marker::PhantomData; use std::ops; @@ -236,262 +235,3 @@ impl ops::Deref for IntSet { &self.xs } } - -#[derive(Debug, Clone)] -pub struct HeapData { - heap: Vec, - indices: IntMap, -} - -impl Default for HeapData { - fn default() -> Self { - Self { - heap: Vec::new(), - indices: IntMap::new(), - } - } -} - -impl HeapData { - pub fn new() -> Self { - Self::default() - } - pub fn len(&self) -> usize { - self.heap.len() - } - pub fn is_empty(&self) -> bool { - self.heap.is_empty() - } - pub fn in_heap(&self, k: K) -> bool { - self.indices.has(k) && self.indices[k] >= 0 - } - - pub fn promote>(&mut self, comp: Comp) -> Heap { - Heap { data: self, comp } - } -} - -impl ops::Index for HeapData { - type Output = K; - fn index(&self, index: usize) -> &Self::Output { - &self.heap[index] - } -} - -pub trait Comparator { - fn cmp(&self, lhs: &T, rhs: &T) -> cmp::Ordering; - fn max(&self, lhs: T, rhs: T) -> T - where - T: Sized, - { - if self.ge(&rhs, &lhs) { - rhs - } else { - lhs - } - } - fn min(&self, lhs: T, rhs: T) -> T - where - T: Sized, - { - if self.le(&lhs, &rhs) { - lhs - } else { - rhs - } - } - fn le(&self, lhs: &T, rhs: &T) -> bool { - match self.cmp(lhs, rhs) { - cmp::Ordering::Less | cmp::Ordering::Equal => true, - _ => false, - } - } - fn lt(&self, lhs: &T, rhs: &T) -> bool { - match self.cmp(lhs, rhs) { - cmp::Ordering::Less => true, - _ => false, - } - } - #[inline] - fn gt(&self, lhs: &T, rhs: &T) -> bool { - self.lt(rhs, lhs) - } - #[inline] - fn ge(&self, lhs: &T, rhs: &T) -> bool { - self.le(rhs, lhs) - } -} - -#[derive(Debug)] -pub struct Heap<'a, K: AsIndex + 'a, Comp: Comparator> { - data: &'a mut HeapData, - comp: Comp, -} - -impl<'a, K: AsIndex + 'a, Comp: Comparator> ops::Deref for Heap<'a, K, Comp> { - type Target = HeapData; - fn deref(&self) -> &Self::Target { - &self.data - } -} -impl<'a, K: AsIndex + 'a, Comp: Comparator> ops::DerefMut for Heap<'a, K, Comp> { - fn deref_mut(&mut self) -> &mut Self::Target { - &mut self.data - } -} - -impl<'a, K: AsIndex + 'a, Comp: Comparator> Heap<'a, K, Comp> { - fn percolate_up(&mut self, mut i: u32) { - let x = self.heap[i as usize]; - let mut p = parent_index(i); - - while i != 0 && self.comp.lt(&x, &self.heap[p as usize]) { - self.heap[i as usize] = self.heap[p as usize]; - let tmp = self.heap[p as usize]; - self.indices[tmp] = i as i32; - i = p; - p = parent_index(p); - } - self.heap[i as usize] = x; - self.indices[x] = i as i32; - } - - fn percolate_down(&mut self, mut i: u32) { - let x = self.heap[i as usize]; - while (left_index(i) as usize) < self.heap.len() { - let child = if (right_index(i) as usize) < self.heap.len() - && self.comp.lt( - &self.heap[right_index(i) as usize], - &self.heap[left_index(i) as usize], - ) { - right_index(i) - } else { - left_index(i) - }; - if !self.comp.lt(&self.heap[child as usize], &x) { - break; - } - self.heap[i as usize] = self.heap[child as usize]; - let tmp = self.heap[i as usize]; - self.indices[tmp] = i as i32; - i = child; - } - self.heap[i as usize] = x; - self.indices[x] = i as i32; - } - pub fn decrease(&mut self, k: K) { - debug_assert!(self.in_heap(k)); - let k_index = self.indices[k]; - self.percolate_up(k_index as u32); - } - pub fn increase(&mut self, k: K) { - debug_assert!(self.in_heap(k)); - let k_index = self.indices[k]; - self.percolate_down(k_index as u32); - } - - /// Safe variant of insert/decrease/increase: - pub fn update(&mut self, k: K) { - if !self.in_heap(k) { - self.insert(k); - } else { - let k_index = self.indices[k]; - self.percolate_up(k_index as u32); - let k_index = self.indices[k]; - self.percolate_down(k_index as u32); - } - } - - pub fn insert(&mut self, k: K) { - self.indices.reserve(k, -1); - debug_assert!(!self.in_heap(k)); - - self.indices[k] = self.heap.len() as i32; - self.heap.push(k); - let k_index = self.indices[k]; - self.percolate_up(k_index as u32); - } - - pub fn remove(&mut self, k: K) { - debug_assert!(self.in_heap(k)); - let k_pos = self.indices[k] as u32; - self.indices[k] = -1; - if (k_pos as usize) < self.heap.len() - 1 { - self.heap[k_pos as usize] = *self.heap.last().unwrap(); - let tmp = self.heap[k_pos as usize]; - self.indices[tmp] = k_pos as i32; - self.heap.pop().expect("cannot pop from empty heap"); - self.percolate_down(k_pos); - } else { - self.heap.pop().expect("cannot pop from empty heap"); - } - } - - pub fn remove_min(&mut self) -> K { - let x = *self.heap.first().expect("heap is empty"); - let lastval = *self.heap.last().expect("heap is empty"); - self.heap[0] = lastval; - self.indices[lastval] = 0; - self.indices[x] = -1; - self.heap.pop().expect("cannot pop from empty heap"); - if self.heap.len() > 1 { - self.percolate_down(0); - } - x - } - - /// Rebuild the heap from scratch, using the elements in 'ns': - pub fn build(&mut self, ns: &[K]) { - { - let data = &mut self.data; - for &x in &data.heap { - data.indices[x] = -1; - } - } - self.heap.clear(); - - for (i, &x) in ns.iter().enumerate() { - // TODO: this should probably call reserve instead of relying on it being reserved already. - debug_assert!(self.indices.has(x)); - self.indices[x] = i as i32; - self.heap.push(x); - } - - let mut i = self.heap.len() as i32 / 2 - 1; - while i >= 0 { - self.percolate_down(i as u32); - i -= 1; - } - } - - pub fn clear_dispose(&mut self, dispose: bool) { - // TODO: shouldn't the 'indices' map also be dispose-cleared? - { - let data = &mut self.data; - for &x in &data.heap { - data.indices[x] = -1; - } - } - self.heap.clear(); - if dispose { - self.heap.shrink_to_fit(); - } - } - - pub fn clear(&mut self) { - self.clear_dispose(false) - } -} - -#[inline(always)] -fn left_index(i: u32) -> u32 { - i * 2 + 1 -} -#[inline(always)] -fn right_index(i: u32) -> u32 { - (i + 1) * 2 -} -#[inline(always)] -fn parent_index(i: u32) -> u32 { - (i.wrapping_sub(1)) >> 1 -} diff --git a/src/batsat/src/lib.rs b/src/batsat/src/lib.rs index 244c276..b8556fe 100644 --- a/src/batsat/src/lib.rs +++ b/src/batsat/src/lib.rs @@ -51,6 +51,7 @@ pub mod clause; pub mod core; pub mod dimacs; pub mod drat; +mod heap; pub mod interface; pub mod intmap; pub mod theory; diff --git a/src/batsat/src/theory.rs b/src/batsat/src/theory.rs index a8ad889..7490eb6 100644 --- a/src/batsat/src/theory.rs +++ b/src/batsat/src/theory.rs @@ -40,7 +40,18 @@ pub trait Theory { /// /// `p` is the literal that has been propagated by the theory in a prefix /// of the current trail. - fn explain_propagation(&mut self, _p: Lit) -> &[Lit]; + fn explain_propagation(&mut self, p: Lit) -> &[Lit]; + + /// Similar to `explain_propagation` but theories should prefer larger older explanations + /// For example, if a theory knows `(a && b) => c` and `c => d` and is asked to explain `d`, + /// `explain_propagation` may prefer to explain using `[c]` to generate a better clause, but + /// `explain_propagation_final` may as well explain using `[a, b]` since otherwise it would just + /// be asked to explain `c` anyway. + /// + /// The default implementation just calls `explain_propagation` + fn explain_propagation_final(&mut self, p: Lit) -> &[Lit] { + self.explain_propagation(p) + } } /// Trivial theory that does nothing