Struct ClauseDatabase 

pub struct ClauseDatabase { /* private fields */ }

Database of clauses with memory pool

Implementations

impl ClauseDatabase

pub fn new() -> Self

Create a new clause database

pub fn stats(&self) -> &ClauseDatabaseStats

Get statistics about the clause database

pub fn add(&mut self, clause: Clause) -> ClauseId

Add a clause to the database

Uses the memory pool (free list) to reuse deleted clause slots when available

pub fn add_original(&mut self, lits: impl IntoIterator<Item = Lit>) -> ClauseId

Add an original clause

pub fn add_learned(&mut self, lits: impl IntoIterator<Item = Lit>) -> ClauseId

Add a learned clause

pub fn get(&self, id: ClauseId) -> Option<&Clause>

Get a clause by ID

pub fn get_mut(&mut self, id: ClauseId) -> Option<&mut Clause>

Get a mutable reference to a clause

pub fn remove(&mut self, id: ClauseId)

Mark a clause as deleted

The deleted clause slot is added to the free list for reuse (memory pool)

pub fn compact(&mut self)

Compact the database by removing deleted clauses from the free list

This should be called periodically to prevent the free list from growing too large

pub fn len(&self) -> usize

Get the number of active clauses

pub fn is_empty(&self) -> bool

Check if empty

pub fn num_original(&self) -> usize

Get the number of original clauses

pub fn num_learned(&self) -> usize

Get the number of learned clauses

pub fn iter_ids(&self) -> impl Iterator<Item = ClauseId> + '_

Iterate over all non-deleted clause IDs

pub fn bump_activity(&mut self, id: ClauseId, increment: f64)

Bump activity of a clause

pub fn decay_activity(&mut self, factor: f64)

Decay all clause activities

Trait Implementations

impl Debug for ClauseDatabase

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for ClauseDatabase

fn default() -> Self

Returns the “default value” for a type.