Struct ClauseActivityManager 

pub struct ClauseActivityManager { /* private fields */ }

Clause activity manager

Manages activity scores for clauses, used in clause deletion policies.

Implementations

impl ClauseActivityManager

pub fn new() -> Self

Create a new clause activity manager

Default decay factor: 0.999 (slower than variable decay)

pub fn with_decay(decay: f64) -> Self

Create with custom decay factor

pub fn bump(&mut self, clause_id: ClauseId)

Bump activity of a clause

pub fn decay(&mut self)

Decay all clause activities

pub fn activity(&self, clause_id: ClauseId) -> f64

Get activity of a clause

pub fn set_activity(&mut self, clause_id: ClauseId, activity: f64)

Set activity of a clause

pub fn stats(&self) -> &ActivityStats

Get statistics

pub fn reset(&mut self)

Reset all activities

Trait Implementations

impl Debug for ClauseActivityManager

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

Formats the value using the given formatter.

impl Default for ClauseActivityManager

fn default() -> Self

Returns the “default value” for a type.