Struct splr::clause::ClauseDB

pub struct ClauseDB {
    pub touched: Vec<bool>,
    pub watcher: Vec<Vec<Watch>>,
    pub num_active: usize,
    pub num_learnt: usize,
    pub certified: Vec<(CertifiedRecord, Vec<i32>)>,
    pub activity_inc: f64,
    pub activity_decay: f64,
    pub inc_step: usize,
    pub soft_limit: usize,
    pub co_lbd_bound: usize,
    pub lbd_frozen_clause: usize,
    pub first_reduction: usize,
    pub next_reduction: usize,
    pub glureduce: bool,
    // some fields omitted
}

Clause database

Fields

touched: Vec<bool>

watcher: Vec<Vec<Watch>>

num_active: usize

num_learnt: usize

certified: Vec<(CertifiedRecord, Vec<i32>)>

activity_inc: f64

activity_decay: f64

inc_step: usize

soft_limit: usize

co_lbd_bound: usize

lbd_frozen_clause: usize

first_reduction: usize

next_reduction: usize

glureduce: bool

Trait Implementations

impl ClauseDBIF for ClauseDB

fn new(config: &Config, nv: usize, nc: usize) -> ClauseDB

return a new instance.

fn len(&self) -> usize

return the length of clause.

fn is_empty(&self) -> bool

return true if it's empty.

fn garbage_collect(&mut self)

delete dead clauses from database, which are made by: * reduce * simplify * kill

fn new_clause(&mut self, v: &[Lit], rank: usize, learnt: bool) -> ClauseId

allocate a new clause and return its id.

fn reset_lbd(&mut self, vars: &VarDB, temp: &mut [usize])

re-calculate the lbd values of all (learnt) clauses.

fn bump_activity(&mut self, cid: ClauseId)

update clause activity.

fn scale_activity(&mut self)

increment activity step.

fn count(&self, alive: bool) -> usize

return the number of alive clauses in the database. Or return the database size if active is false.

fn countf(&self, mask: Flag) -> usize

return the number of clauses which satisfy given flags and aren't DEAD.

fn attach(
    &mut self,
    state: &mut State,
    vars: &mut VarDB,
    lbd: usize
) -> ClauseId

make a new clause from state.new_learnt and register it to clause database.

fn detach(&mut self, cid: ClauseId)

unregister a clause cid from clause database and make the clause dead.

fn reduce(&mut self, state: &mut State, vars: &mut VarDB)

halve the number of 'learnt' or removable clauses.

fn simplify(
    &mut self,
    asgs: &mut AssignStack,
    elim: &mut Eliminator,
    state: &mut State,
    vars: &mut VarDB
) -> MaybeInconsistent

simplify database by: * removing satisfiable clauses * calling exhaustive simplifier that tries clause subsumption and variable elimination.

fn reset(&mut self)

fn certificate_add(&mut self, vec: &[Lit])

record a clause to unsat certification.

fn certificate_delete(&mut self, vec: &[Lit])

record a deleted clause to unsat certification.

fn eliminate_satisfied_clauses(
    &mut self,
    elim: &mut Eliminator,
    vars: &mut VarDB,
    update_occur: bool
)

delete satisfied clauses at decision level zero.

fn check_size(&self) -> MaybeInconsistent

emit an error if the db size (the number of clauses) is over the limit.

fn make_permanent(&mut self, reinit: bool)

change good learnt clauses to permanent one.

impl Debug for ClauseDB

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

Formats the value using the given formatter.

impl Index<u32> for ClauseDB

type Output = Clause

The returned type after indexing.

fn index(&self, cid: ClauseId) -> &Clause

Performs the indexing (container[index]) operation.

impl Index<Range<usize>> for ClauseDB

type Output = [Clause]

The returned type after indexing.

fn index(&self, r: Range<usize>) -> &[Clause]

Performs the indexing (container[index]) operation.

impl Index<RangeFrom<usize>> for ClauseDB

type Output = [Clause]

The returned type after indexing.

fn index(&self, r: RangeFrom<usize>) -> &[Clause]

Performs the indexing (container[index]) operation.

impl IndexMut<u32> for ClauseDB

fn index_mut(&mut self, cid: ClauseId) -> &mut Clause

Performs the mutable indexing (container[index]) operation.

impl IndexMut<Range<usize>> for ClauseDB

fn index_mut(&mut self, r: Range<usize>) -> &mut [Clause]

Performs the mutable indexing (container[index]) operation.

impl IndexMut<RangeFrom<usize>> for ClauseDB

fn index_mut(&mut self, r: RangeFrom<usize>) -> &mut [Clause]

Performs the mutable indexing (container[index]) operation.