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 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

during_vivification: bool

eliminated_permanent: Vec<Vec<Lit>>

Trait Implementations

impl ActivityIF for ClauseDB

type Ix = ClauseId

type for index

type Inc = ()

an extra parameter for bumping

pub fn activity(&mut self, ci: Self::Ix) -> f64

return the current activity of an element.

pub fn set_activity(&mut self, ci: Self::Ix, val: f64)

set activity forcibly.

pub fn bump_activity(&mut self, cid: Self::Ix, _: Self::Inc)

update an element's activity.

pub fn scale_activity(&mut self)

increment activity step.

impl ClauseDBIF for ClauseDB

pub fn len(&self) -> usize

return the length of clause.

pub fn is_empty(&self) -> bool

return true if it's empty.

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

return an iterator.

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

return a mutable iterator.

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

return a watcher list

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

return the list of bin_watch lists

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

return the list of watch lists

pub fn garbage_collect(&mut self)

delete dead clauses from database, which are made by:

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

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

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

allocate a new clause and return its id.

pub 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.

pub fn count(&self) -> usize

return the number of alive clauses in the database.

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

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

pub 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.

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

check a condition to reduce.

pub fn reset(&mut self)

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

record a clause to unsat certification.

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

record a deleted clause to unsat certification.

pub fn touch_var(&mut self, vi: VarId)

flag positive and negative literals of a var as dirty

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

check the number of clauses

pub 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.

pub 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.

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

minimize a clause.

impl Debug for ClauseDB

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

Formats the value using the given formatter.

impl Default for ClauseDB

pub fn default() -> ClauseDB

Returns the "default value" for a type.

impl Export<(usize, usize, usize, usize, usize, usize), bool> for ClauseDB

pub fn exports(&self) -> (usize, usize, usize, usize, usize, usize)

exports:

1. the number of active clauses
2. the number of binary clauses
3. the number of binary learnt clauses
4. the number of clauses which LBDs are 2
5. the number of learnt clauses
6. the number of clause reductions

 use crate::{splr::config::Config, splr::types::*};
 use crate::splr::cdb::ClauseDB;
 let cdb = ClauseDB::instantiate(&Config::default(), &CNFDescription::default());
 let (_active, _bi_clause, _bi_learnt, _lbd2, _learnt, _reduction) = cdb.exports();

pub fn mode(&self) -> bool

return the value of use_chan_seok

impl Index<&'_ ClauseId> for ClauseDB

type Output = Clause

The returned type after indexing.

pub 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.

pub 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.

pub 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.

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

Performs the indexing (container[index]) operation.

impl IndexMut<&'_ ClauseId> for ClauseDB

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

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

impl IndexMut<ClauseId> for ClauseDB

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

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

impl IndexMut<Range<usize>> for ClauseDB

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

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

impl IndexMut<RangeFrom<usize>> for ClauseDB

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

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

impl Instantiate for ClauseDB

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

make and return an object from Config and CNFDescription.

pub fn handle(&mut self, e: SolverEvent)

update by a solver event.

impl LBDIF for ClauseDB

pub fn compute_lbd<A>(&mut self, asg: &A, vec: &[Lit]) -> usize where
    A: AssignIF, 

return the LBD value for a set of literals.

pub fn compute_lbd_of<A>(&mut self, asg: &A, cid: ClauseId) -> usize where
    A: AssignIF, 

return the LBD value of clause cid.

pub fn reset_lbd<A>(&mut self, asg: &A, all: bool) where
    A: AssignIF, 

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