Struct splr::cdb::ClauseDB

pub struct ClauseDB {
    pub bin_watcher: Vec<Vec<Watch>>,
    pub watcher: Vec<Vec<Watch>>,
    pub certified: Vec<(CertifiedRecord, Vec<i32>)>,
    pub lbd_of_dp_ema: Ema,
    pub during_vivification: bool,
    pub eliminated_permanent: Vec<Vec<Lit>>,
    // some fields omitted
}

Clause database

 use crate::{splr::config::Config, splr::types::*};
 use crate::splr::cdb::ClauseDB;
 let cdb = ClauseDB::instantiate(&Config::default(), &CNFDescription::default());

Fields

bin_watcher: Vec<Vec<Watch>>

container of watch literals for binary clauses

watcher: Vec<Vec<Watch>>

container of watch literals

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

clause history to make certification

lbd_of_dp_ema: Ema

EMA of LBD of clauses used in conflict analysis (dependency graph)

during_vivification: bool

eliminated_permanent: Vec<Vec<Lit>>

Trait Implementations

impl ActivityIF<ClauseId> for ClauseDB

fn activity(&mut self, cid: ClauseId) -> f64

return one’s activity.

fn average_activity(&self) -> f64

return average activity

fn set_activity(&mut self, cid: ClauseId, val: f64)

set activity

fn reward_at_analysis(&mut self, cid: ClauseId)

modify one’s activity at conflict analysis in conflict_analyze in solver.

fn update_rewards(&mut self)

update internal counter.

fn reward_at_assign(&mut self, _ix: Ix)

modify one’s activity at value assignment in assign.

fn reward_at_propagation(&mut self, _ix: Ix)

modify one’s activity at value assignment in unit propagation.

fn reward_at_unassign(&mut self, _ix: Ix)

modify one’s activity at value un-assignment in cancel_until.

fn update_activity_decay(&mut self, _index: Option<usize>)

update reward decay.

impl ClauseDBIF for ClauseDB

fn len(&self) -> usize

return the length of clause.

fn is_empty(&self) -> bool

return true if it’s empty.

fn iter(&self) -> Iter<'_, Clause>

return an iterator.

fn iter_mut(&mut self) -> IterMut<'_, Clause>

return a mutable iterator.

fn watcher_list(&self, l: Lit) -> &[Watch]

return a watcher list

fn bin_watcher_lists(&self) -> &[Vec<Watch>]

return the list of bin_watch lists

fn watcher_lists_mut(&mut self) -> &mut [Vec<Watch>]

return the list of watch lists

fn garbage_collect(&mut self)

delete dead clauses from database, which are made by:

fn registered_bin_clause(&self, l0: Lit, l1: Lit) -> bool

return true if a literal pair (l0, l1) is registered.

fn new_clause<A>(
    &mut self,
    asg: &mut A,
    vec: &mut Vec<Lit>,
    learnt: bool,
    level_sort: bool
) -> ClauseId where
    A: AssignIF, 

allocate a new clause and return its id.

fn mark_clause_as_used<A>(&mut self, asg: &mut A, cid: ClauseId) -> bool where
    A: AssignIF, 

update LBD then convert a learnt clause to permanent if needed.

fn count(&self) -> usize

return the number of alive clauses in the database.

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

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

fn detach(&mut self, cid: ClauseId)

Warning

this function is the only function that turns Flag::DEAD on without calling garbage_collect which erases all the DEAD flags. So you must care about how and when garbage_collect is called.

fn reduce<A>(&mut self, asg: &mut A, nc: usize) -> bool where
    A: AssignIF, 

check a condition to reduce.

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 touch_var(&mut self, vi: VarId)

flag positive and negative literals of a var as dirty

fn check_size(&self) -> Result<bool, SolverError>

check the number of clauses

fn validate(&self, model: &[Option<bool>], strict: bool) -> Option<ClauseId>

returns None if the given assignment is a model of a problem. Otherwise returns a clause which is not satisfiable under a given assignment. Clauses with an unassigned literal are treated as falsified in strict mode.

fn strengthen(&mut self, cid: ClauseId, p: Lit) -> bool

removes Lit p from Clause self. This is an O(n) function! This returns true if the clause became a unit clause. And this is called only from Eliminator::strengthen_clause.

fn minimize_with_biclauses<A>(&mut self, asg: &A, vec: &mut Vec<Lit>) where
    A: AssignIF, 

minimize a clause.

impl Clone for ClauseDB

fn clone(&self) -> ClauseDB

Returns a copy of the value.

pub fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for ClauseDB

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

Formats the value using the given formatter.

impl Default for ClauseDB

fn default() -> ClauseDB

Returns the “default value” for a type.

impl Index<&'_ ClauseId> for ClauseDB

type Output = Clause

The returned type after indexing.

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

Performs the indexing (container[index]) operation.

impl Index<ClauseId> 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<&'_ ClauseId> for ClauseDB

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

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

impl IndexMut<ClauseId> 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.

impl Instantiate for ClauseDB

fn instantiate(config: &Config, cnf: &CNFDescription) -> ClauseDB

make and return an object from Config and CNFDescription.

fn handle(&mut self, e: SolverEvent)

update by a solver event.

impl PropertyDereference<Tf64, f64> for ClauseDB

fn derefer(&self, k: Tf64) -> f64

impl PropertyDereference<Tusize, usize> for ClauseDB

fn derefer(&self, k: Tusize) -> usize