diff options
Diffstat (limited to 'vendor/varisat/src/clause/db.rs')
-rw-r--r-- | vendor/varisat/src/clause/db.rs | 269 |
1 files changed, 269 insertions, 0 deletions
diff --git a/vendor/varisat/src/clause/db.rs b/vendor/varisat/src/clause/db.rs new file mode 100644 index 000000000..780e14557 --- /dev/null +++ b/vendor/varisat/src/clause/db.rs @@ -0,0 +1,269 @@ +//! Database for long clauses. +use std::mem::transmute; + +use partial_ref::{partial, PartialRef}; + +use varisat_formula::Lit; + +use crate::{ + context::{parts::*, Context}, + prop::Reason, +}; + +use super::{header::HEADER_LEN, ClauseAlloc, ClauseHeader, ClauseRef}; + +/// Partitions of the clause database. +/// +/// The long clauses are partitioned into 4 [`Tier`]s. This follows the approach described by +/// Chanseok Oh in ["Between SAT and UNSAT: The Fundamental Difference in CDCL +/// SAT"](https://doi.org/10.1007/978-3-319-24318-4_23), section 4. +#[derive(Debug, Copy, Clone, PartialEq, Eq)] +#[repr(u8)] +pub enum Tier { + Irred = 0, + Core = 1, + Mid = 2, + Local = 3, +} + +impl Tier { + /// Total number of tiers. + pub const fn count() -> usize { + 4 + } + + /// Cast an index into the corresponding tier. + pub unsafe fn from_index(index: usize) -> Tier { + debug_assert!(index < Tier::count()); + transmute(index as u8) + } +} + +/// Database for long clauses. +/// +/// Removal of clauses from the `clauses` and the `by_tier` fields can be delayed. The clause +/// header's deleted and tier fields need to be checked when iterating over these. `by_tier` may +/// also contain duplicate entries. +#[derive(Default)] +pub struct ClauseDb { + /// May contain deleted clauses, see above + pub(super) clauses: Vec<ClauseRef>, + /// May contain deleted and moved clauses, see above + pub(super) by_tier: [Vec<ClauseRef>; Tier::count()], + /// These counts should always be up to date + pub(super) count_by_tier: [usize; Tier::count()], + /// Size of deleted but not collected clauses + pub(super) garbage_size: usize, +} + +impl ClauseDb { + /// The number of long clauses of a given tier. + pub fn count_by_tier(&self, tier: Tier) -> usize { + self.count_by_tier[tier as usize] + } +} + +/// Add a long clause to the database. +pub fn add_clause( + mut ctx: partial!(Context, mut ClauseAllocP, mut ClauseDbP, mut WatchlistsP), + header: ClauseHeader, + lits: &[Lit], +) -> ClauseRef { + let tier = header.tier(); + + let cref = ctx.part_mut(ClauseAllocP).add_clause(header, lits); + + ctx.part_mut(WatchlistsP) + .watch_clause(cref, [lits[0], lits[1]]); + + let db = ctx.part_mut(ClauseDbP); + + db.clauses.push(cref); + db.by_tier[tier as usize].push(cref); + db.count_by_tier[tier as usize] += 1; + + cref +} + +/// Change the tier of a long clause. +/// +/// This is a noop for a clause already of the specified tier. +pub fn set_clause_tier( + mut ctx: partial!(Context, mut ClauseAllocP, mut ClauseDbP), + cref: ClauseRef, + tier: Tier, +) { + let (alloc, mut ctx) = ctx.split_part_mut(ClauseAllocP); + let db = ctx.part_mut(ClauseDbP); + + let old_tier = alloc.header(cref).tier(); + if old_tier != tier { + db.count_by_tier[old_tier as usize] -= 1; + db.count_by_tier[tier as usize] += 1; + + alloc.header_mut(cref).set_tier(tier); + db.by_tier[tier as usize].push(cref); + } +} + +/// Delete a long clause from the database. +pub fn delete_clause( + mut ctx: partial!(Context, mut ClauseAllocP, mut ClauseDbP, mut WatchlistsP), + cref: ClauseRef, +) { + // TODO Don't force a rebuild of all watchlists here + ctx.part_mut(WatchlistsP).disable(); + + let (alloc, mut ctx) = ctx.split_part_mut(ClauseAllocP); + let db = ctx.part_mut(ClauseDbP); + + let header = alloc.header_mut(cref); + + debug_assert!( + !header.deleted(), + "delete_clause for already deleted clause" + ); + + header.set_deleted(true); + + db.count_by_tier[header.tier() as usize] -= 1; + + db.garbage_size += header.len() + HEADER_LEN; +} + +/// Delete a long clause from the database unless it is asserting. +/// +/// Returns true if the clause was deleted. +pub fn try_delete_clause( + mut ctx: partial!( + Context, + mut ClauseAllocP, + mut ClauseDbP, + mut WatchlistsP, + ImplGraphP, + AssignmentP, + ), + cref: ClauseRef, +) -> bool { + let initial_lit = ctx.part(ClauseAllocP).clause(cref).lits()[0]; + let asserting = ctx.part(AssignmentP).lit_is_true(initial_lit) + && ctx.part(ImplGraphP).reason(initial_lit.var()) == &Reason::Long(cref); + + if !asserting { + delete_clause(ctx.borrow(), cref); + } + !asserting +} + +/// Iterator over all long clauses. +/// +/// This filters deleted (but uncollected) clauses on the fly. +pub fn clauses_iter<'a>( + ctx: &'a partial!('a Context, ClauseAllocP, ClauseDbP), +) -> impl Iterator<Item = ClauseRef> + 'a { + let alloc = ctx.part(ClauseAllocP); + ctx.part(ClauseDbP) + .clauses + .iter() + .cloned() + .filter(move |&cref| !alloc.header(cref).deleted()) +} + +/// Iterate over all and remove some long clauses. +/// +/// Takes a closure that returns true for each clause that should be kept and false for each that +/// should be deleted. +pub fn filter_clauses<F>( + mut ctx: partial!(Context, mut ClauseAllocP, mut ClauseDbP, mut WatchlistsP), + mut filter: F, +) where + F: FnMut(&mut ClauseAlloc, ClauseRef) -> bool, +{ + ctx.part_mut(WatchlistsP).disable(); + + let (alloc, mut ctx) = ctx.split_part_mut(ClauseAllocP); + let db = ctx.part_mut(ClauseDbP); + + let count_by_tier = &mut db.count_by_tier; + let garbage_size = &mut db.garbage_size; + + db.clauses.retain(|&cref| { + if alloc.header(cref).deleted() { + false + } else if filter(alloc, cref) { + true + } else { + let header = alloc.header_mut(cref); + + header.set_deleted(true); + + count_by_tier[header.tier() as usize] -= 1; + + *garbage_size += header.len() + HEADER_LEN; + + false + } + }) +} + +#[cfg(test)] +mod tests { + use super::*; + + use partial_ref::IntoPartialRefMut; + + use varisat_formula::cnf_formula; + + use crate::context::set_var_count; + + #[test] + fn set_tiers_and_deletes() { + let mut ctx = Context::default(); + + let mut ctx = ctx.into_partial_ref_mut(); + + let clauses = cnf_formula![ + 1, 2, 3; + 4, -5, 6; + -2, 3, -4; + -3, 5, 2, 7, 5; + ]; + + set_var_count(ctx.borrow(), clauses.var_count()); + + let tiers = vec![Tier::Irred, Tier::Core, Tier::Mid, Tier::Local]; + let new_tiers = vec![Tier::Irred, Tier::Local, Tier::Local, Tier::Core]; + + let mut crefs = vec![]; + + for (clause, &tier) in clauses.iter().zip(tiers.iter()) { + let mut header = ClauseHeader::new(); + header.set_tier(tier); + let cref = add_clause(ctx.borrow(), header, clause); + crefs.push(cref); + } + + for (&cref, &tier) in crefs.iter().rev().zip(new_tiers.iter().rev()) { + set_clause_tier(ctx.borrow(), cref, tier); + } + + // We only check presence, as deletion from these lists is delayed + assert!(ctx.part(ClauseDbP).by_tier[Tier::Irred as usize].contains(&crefs[0])); + assert!(ctx.part(ClauseDbP).by_tier[Tier::Core as usize].contains(&crefs[3])); + assert!(ctx.part(ClauseDbP).by_tier[Tier::Local as usize].contains(&crefs[1])); + assert!(ctx.part(ClauseDbP).by_tier[Tier::Local as usize].contains(&crefs[2])); + + assert_eq!(ctx.part(ClauseDbP).count_by_tier(Tier::Irred), 1); + assert_eq!(ctx.part(ClauseDbP).count_by_tier(Tier::Core), 1); + assert_eq!(ctx.part(ClauseDbP).count_by_tier(Tier::Mid), 0); + assert_eq!(ctx.part(ClauseDbP).count_by_tier(Tier::Local), 2); + + delete_clause(ctx.borrow(), crefs[0]); + delete_clause(ctx.borrow(), crefs[2]); + + assert_eq!(ctx.part(ClauseDbP).count_by_tier(Tier::Irred), 0); + assert_eq!(ctx.part(ClauseDbP).count_by_tier(Tier::Core), 1); + assert_eq!(ctx.part(ClauseDbP).count_by_tier(Tier::Mid), 0); + assert_eq!(ctx.part(ClauseDbP).count_by_tier(Tier::Local), 1); + } +} |