From d8f6e8c547ffde76c7b58f3bd0f87b2f39343670 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Sun, 12 Jan 2025 02:25:56 +0900 Subject: [PATCH] Move `Clause`, `ClauseId` and `ClauseDB` to appropriate files --- src/cdb/clause.rs | 38 +++++++++++ src/cdb/db.rs | 84 +++++++++++++++++++++++- src/cdb/mod.rs | 129 ++----------------------------------- src/cdb/vivify.rs | 2 +- src/processor/eliminate.rs | 2 +- src/solver/build.rs | 2 +- src/solver/conflict.rs | 2 +- src/solver/mod.rs | 2 +- src/solver/search.rs | 2 +- src/types.rs | 6 +- 10 files changed, 138 insertions(+), 131 deletions(-) diff --git a/src/cdb/clause.rs b/src/cdb/clause.rs index 3db3ac3da..31b02478a 100644 --- a/src/cdb/clause.rs +++ b/src/cdb/clause.rs @@ -2,11 +2,49 @@ use { crate::{assign::AssignIF, types::*}, std::{ fmt, + num::NonZeroU32, ops::{Index, IndexMut, Range, RangeFrom}, slice::Iter, }, }; +/// Clause identifier, or clause index, starting with one. +/// Note: ids are re-used after 'garbage collection'. +#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)] +pub struct ClauseId { + /// a sequence number. + pub ordinal: NonZeroU32, +} + +/// A representation of 'clause' +#[derive(Clone, Debug, Eq, PartialEq, PartialOrd)] +pub struct Clause { + /// The literals in a clause. + pub(super) lits: Vec, + /// Flags (8 bits) + pub(crate) flags: FlagClause, + /// A static clause evaluation criterion like LBD, NDD, or something. + pub rank: u16, + /// A record of the rank at previos stage. + pub rank_old: u16, + /// the index from which `propagate` starts searching an un-falsified literal. + /// Since it's just a hint, we don't need u32 or usize. + pub(crate) search_from: u16, + + #[cfg(any(feature = "boundary_check", feature = "clause_rewarding"))] + /// the number of conflicts at which this clause was used in `conflict_analyze` + timestamp: usize, + + #[cfg(feature = "clause_rewarding")] + /// A dynamic clause evaluation criterion based on the number of references. + reward: f64, + + #[cfg(feature = "boundary_check")] + pub birth: usize, + #[cfg(feature = "boundary_check")] + pub moved_at: Propagate, +} + impl Default for Clause { fn default() -> Clause { Clause { diff --git a/src/cdb/db.rs b/src/cdb/db.rs index db528ade2..6ee26d26f 100644 --- a/src/cdb/db.rs +++ b/src/cdb/db.rs @@ -1,11 +1,11 @@ use { super::{ binary::{BinaryLinkIF, BinaryLinkList}, + clause::{Clause, ClauseId}, ema::ProgressLBD, property, watch_cache::*, - BinaryLinkDB, CertificationStore, Clause, ClauseDB, ClauseDBIF, ClauseId, ReductionType, - RefClause, + BinaryLinkDB, CertificationStore, ClauseDBIF, ReductionType, RefClause, }, crate::{assign::AssignIF, types::*}, std::{ @@ -18,6 +18,86 @@ use { #[cfg(not(feature = "no_IO"))] use std::{fs::File, io::Write, path::Path}; +/// Clause database +/// +///``` +/// use crate::{splr::config::Config, splr::types::*}; +/// use crate::splr::cdb::ClauseDB; +/// let cdb = ClauseDB::instantiate(&Config::default(), &CNFDescription::default()); +///``` +#[derive(Clone, Debug)] +pub struct ClauseDB { + /// container of clauses + pub(crate) clause: Vec, + /// hashed representation of binary clauses. + ///## Note + /// This means a biclause \[l0, l1\] is stored at bi_clause\[l0\] instead of bi_clause\[!l0\]. + /// + pub(super) binary_link: BinaryLinkDB, + /// container of watch literals + pub(crate) watch_cache: Vec, + /// collected free clause ids. + pub(super) freelist: Vec, + /// see unsat_certificate.rs + pub(super) certification_store: CertificationStore, + /// a number of clauses to emit out-of-memory exception + soft_limit: usize, + /// 'small' clause threshold + co_lbd_bound: u16, + // not in use + // lbd_frozen_clause: usize, + + // bi-clause completion + bi_clause_completion_queue: Vec, + pub(super) num_bi_clause_completion: usize, + + // + //## clause rewarding + // + /// an index for counting elapsed time + #[cfg(feature = "clause_rewarding")] + tick: usize, + #[cfg(feature = "clause_rewarding")] + activity_decay: f64, + #[cfg(feature = "clause_rewarding")] + activity_anti_decay: f64, + + // + //## LBD + // + /// a working buffer for LBD calculation + lbd_temp: Vec, + pub(crate) lbd: ProgressLBD, + + // + //## statistics + // + /// the number of active (not DEAD) clauses. + pub(super) num_clause: usize, + /// the number of binary clauses. + pub(super) num_bi_clause: usize, + /// the number of binary learnt clauses. + pub(super) num_bi_learnt: usize, + /// the number of clauses which LBDs are 2. + pub(super) num_lbd2: usize, + /// the present number of learnt clauses. + pub(super) num_learnt: usize, + /// the number of reductions. + pub(super) num_reduction: usize, + /// the number of reregistration of a bi-clause + pub(super) num_reregistration: usize, + /// Literal Block Entanglement + /// EMA of LBD of clauses used in conflict analysis (dependency graph) + pub(super) lb_entanglement: Ema2, + /// cutoff value used in the last `reduce` + pub(super) reduction_threshold: f64, + + // + //## incremental solving + // + pub eliminated_permanent: Vec>, +} + impl Default for ClauseDB { fn default() -> ClauseDB { ClauseDB { diff --git a/src/cdb/mod.rs b/src/cdb/mod.rs index de9a6da73..1fdad39f9 100644 --- a/src/cdb/mod.rs +++ b/src/cdb/mod.rs @@ -5,9 +5,9 @@ mod binary; /// methods on `ClauseId` mod cid; /// methods on `Clause` -mod clause; +pub mod clause; /// methods on `ClauseDB` -mod db; +pub mod db; /// EMA mod ema; /// methods for Stochastic Local Search @@ -29,10 +29,10 @@ pub use self::{ }; use { - self::ema::ProgressLBD, crate::{assign::AssignIF, types::*}, + clause::{Clause, ClauseId}, + db::ClauseDB, std::{ - num::NonZeroU32, ops::IndexMut, slice::{Iter, IterMut}, }, @@ -182,128 +182,11 @@ pub trait ClauseDBIF: fn dump_cnf(&self, asg: &impl AssignIF, fname: &Path); } -/// Clause identifier, or clause index, starting with one. -/// Note: ids are re-used after 'garbage collection'. -#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)] -pub struct ClauseId { - /// a sequence number. - pub ordinal: NonZeroU32, -} - -/// A representation of 'clause' -#[derive(Clone, Debug, Eq, PartialEq, PartialOrd)] -pub struct Clause { - /// The literals in a clause. - lits: Vec, - /// Flags (8 bits) - flags: FlagClause, - /// A static clause evaluation criterion like LBD, NDD, or something. - pub rank: u16, - /// A record of the rank at previos stage. - pub rank_old: u16, - /// the index from which `propagate` starts searching an un-falsified literal. - /// Since it's just a hint, we don't need u32 or usize. - pub search_from: u16, - - #[cfg(any(feature = "boundary_check", feature = "clause_rewarding"))] - /// the number of conflicts at which this clause was used in `conflict_analyze` - timestamp: usize, - - #[cfg(feature = "clause_rewarding")] - /// A dynamic clause evaluation criterion based on the number of references. - reward: f64, - - #[cfg(feature = "boundary_check")] - pub birth: usize, - #[cfg(feature = "boundary_check")] - pub moved_at: Propagate, -} - -/// Clause database -/// -///``` -/// use crate::{splr::config::Config, splr::types::*}; -/// use crate::splr::cdb::ClauseDB; -/// let cdb = ClauseDB::instantiate(&Config::default(), &CNFDescription::default()); -///``` -#[derive(Clone, Debug)] -pub struct ClauseDB { - /// container of clauses - clause: Vec, - /// hashed representation of binary clauses. - ///## Note - /// This means a biclause \[l0, l1\] is stored at bi_clause\[l0\] instead of bi_clause\[!l0\]. - /// - binary_link: BinaryLinkDB, - /// container of watch literals - watch_cache: Vec, - /// collected free clause ids. - freelist: Vec, - /// see unsat_certificate.rs - certification_store: CertificationStore, - /// a number of clauses to emit out-of-memory exception - soft_limit: usize, - /// 'small' clause threshold - co_lbd_bound: u16, - // not in use - // lbd_frozen_clause: usize, - - // bi-clause completion - bi_clause_completion_queue: Vec, - num_bi_clause_completion: usize, - - // - //## clause rewarding - // - /// an index for counting elapsed time - #[cfg(feature = "clause_rewarding")] - tick: usize, - #[cfg(feature = "clause_rewarding")] - activity_decay: f64, - #[cfg(feature = "clause_rewarding")] - activity_anti_decay: f64, - - // - //## LBD - // - /// a working buffer for LBD calculation - lbd_temp: Vec, - lbd: ProgressLBD, - - // - //## statistics - // - /// the number of active (not DEAD) clauses. - num_clause: usize, - /// the number of binary clauses. - num_bi_clause: usize, - /// the number of binary learnt clauses. - num_bi_learnt: usize, - /// the number of clauses which LBDs are 2. - num_lbd2: usize, - /// the present number of learnt clauses. - num_learnt: usize, - /// the number of reductions. - num_reduction: usize, - /// the number of reregistration of a bi-clause - num_reregistration: usize, - /// Literal Block Entanglement - /// EMA of LBD of clauses used in conflict analysis (dependency graph) - lb_entanglement: Ema2, - /// cutoff value used in the last `reduce` - reduction_threshold: f64, - - // - //## incremental solving - // - pub eliminated_permanent: Vec>, -} - #[derive(Clone, Debug)] pub enum ReductionType { /// weight by Reverse Activity Sum over the added clauses RASonADD(usize), - /// weight by Reverse Activito Sum over all learnt clauses + /// weight by Reverse Activity Sum over all learnt clauses RASonALL(f64, f64), /// weight by Literal Block Distance over the added clauses LBDonADD(usize), @@ -406,6 +289,8 @@ pub mod property { #[cfg(test)] mod tests { + use std::num::NonZeroU32; + use super::*; use crate::assign::{AssignStack, PropagateIF}; diff --git a/src/cdb/vivify.rs b/src/cdb/vivify.rs index acd6685ae..fe4488d8c 100644 --- a/src/cdb/vivify.rs +++ b/src/cdb/vivify.rs @@ -2,7 +2,7 @@ #![allow(dead_code)] use crate::{ assign::{AssignIF, AssignStack, PropagateIF, VarManipulateIF}, - cdb::{ClauseDB, ClauseDBIF, ClauseIF}, + cdb::{clause::Clause, db::ClauseDB, ClauseDBIF, ClauseIF}, state::{Stat, State, StateIF}, types::*, }; diff --git a/src/processor/eliminate.rs b/src/processor/eliminate.rs index ee0e4ad90..f5a444801 100644 --- a/src/processor/eliminate.rs +++ b/src/processor/eliminate.rs @@ -334,7 +334,7 @@ mod tests { use super::*; use crate::{ assign::VarManipulateIF, - cdb::{Clause, ClauseDB}, + cdb::{clause::Clause, db::ClauseDB}, processor::EliminateIF, solver::Solver, }; diff --git a/src/solver/build.rs b/src/solver/build.rs index 664e9e47e..cb632abbc 100644 --- a/src/solver/build.rs +++ b/src/solver/build.rs @@ -3,7 +3,7 @@ use { super::{Certificate, Solver, SolverEvent, SolverResult, State, StateIF}, crate::{ assign::{AssignIF, AssignStack, PropagateIF, VarManipulateIF}, - cdb::{ClauseDB, ClauseDBIF}, + cdb::{db::ClauseDB, ClauseDBIF}, types::*, }, }; diff --git a/src/solver/conflict.rs b/src/solver/conflict.rs index 103d8bf69..82dd681dd 100644 --- a/src/solver/conflict.rs +++ b/src/solver/conflict.rs @@ -7,7 +7,7 @@ use { super::State, crate::{ assign::{AssignIF, AssignStack, PropagateIF, VarManipulateIF}, - cdb::{ClauseDB, ClauseDBIF}, + cdb::{db::ClauseDB, ClauseDBIF}, types::*, }, }; diff --git a/src/solver/mod.rs b/src/solver/mod.rs index 64f0366b9..5c38bb449 100644 --- a/src/solver/mod.rs +++ b/src/solver/mod.rs @@ -20,7 +20,7 @@ pub use self::{ validate::ValidateIF, }; -use crate::{assign::AssignStack, cdb::ClauseDB, state::*, types::*}; +use crate::{assign::AssignStack, cdb::db::ClauseDB, state::*, types::*}; /// Normal results returned by Solver. #[derive(Debug, Eq, PartialEq)] diff --git a/src/solver/search.rs b/src/solver/search.rs index ae7cae3ac..9d9a2bcaf 100644 --- a/src/solver/search.rs +++ b/src/solver/search.rs @@ -6,7 +6,7 @@ use { }, crate::{ assign::{self, AssignIF, AssignStack, PropagateIF, VarManipulateIF, VarSelectIF}, - cdb::{self, ClauseDB, ClauseDBIF, ReductionType, VivifyIF}, + cdb::{self, db::ClauseDB, ClauseDBIF, ReductionType, VivifyIF}, processor::{EliminateIF, Eliminator}, state::{Stat, State, StateIF}, types::*, diff --git a/src/types.rs b/src/types.rs index 81fe142f9..567202b1f 100644 --- a/src/types.rs +++ b/src/types.rs @@ -2,7 +2,11 @@ /// some common traits. pub use crate::{ assign::AssignReason, - cdb::{Clause, ClauseDB, ClauseIF, ClauseId, ClauseIdIF}, + cdb::{ + clause::{Clause, ClauseId}, + db::ClauseDB, + ClauseIF, ClauseIdIF, + }, config::Config, primitive::{ema::*, luby::*}, solver::SolverEvent,