Struct splr::cdb::ClauseDB

pub struct ClauseDB {
    pub eliminated_permanent: Vec<Vec<Lit>>,
    /* private fields */
}

Clause database

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

Fields

eliminated_permanent: Vec<Vec<Lit>>

Trait Implementations

impl ClauseDBIF for ClauseDB

fn remove_clause(&mut self, cid: ClauseId)

Warning

this function is the only function that makes dead clauses

fn reduce(&mut self, asg: &mut impl AssignIF, setting: ReductionType)

reduce the number of ‘learnt’ or removable clauses.

fn dump_cnf(&self, asg: &impl AssignIF, fname: &Path)

dump all active clauses and assertions as a CNF file.

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 binary_links(&self, l: Lit) -> &BinaryLinkList

return binary links: BinaryLinkList connected with a Lit.

fn fetch_watch_cache_entry(&self, lit: Lit, wix: usize) -> (ClauseId, Lit)

fn watch_cache_iter(&mut self, l: Lit) -> WatchCacheIterator

replace the mutable watcher list with an empty one, and return the list

fn detach_watch_cache(&mut self, l: Lit, iter: &mut WatchCacheIterator)

detach the watch_cache referred by the head of a watch_cache iterator

fn merge_watch_cache(&mut self, p: Lit, wc: Vec<(ClauseId, Lit)>)

Merge two watch cache

fn swap_watch(&mut self, cid: ClauseId)

swap the first two literals in a clause.

fn new_clause( &mut self, asg: &mut impl AssignIF, vec: &mut Vec<Lit>, learnt: bool ) -> RefClause

allocate a new clause and return its id. Note this removes an eliminated Lit p from a clause. 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 new_clause_sandbox( &mut self, asg: &mut impl AssignIF, vec: &mut Vec<Lit> ) -> RefClause

fn remove_clause_sandbox(&mut self, cid: ClauseId)

un-register a clause cid from clause database and make the clause dead.

fn transform_by_restoring_watch_cache( &mut self, l: Lit, iter: &mut WatchCacheIterator, op: Option<Lit> )

push back a watch literal cache by adjusting the iterator for lit

fn transform_by_elimination(&mut self, cid: ClauseId, p: Lit) -> RefClause

update watches of the clause

fn transform_by_replacement( &mut self, cid: ClauseId, new_lits: &mut Vec<Lit> ) -> RefClause

generic clause transformer (not in use)

fn transform_by_simplification( &mut self, asg: &mut impl AssignIF, cid: ClauseId ) -> RefClause

check satisfied and nullified literals in a clause

fn transform_by_updating_watch( &mut self, cid: ClauseId, old: usize, new: usize, removed: bool )

swap i-th watch with j-th literal then update watch caches correctly

fn update_at_analysis(&mut self, asg: &impl AssignIF, cid: ClauseId) -> bool

update flags. return true if it’s learnt.

fn reset(&mut self)

remove all learnt clauses.

fn certificate_add_assertion(&mut self, lit: Lit)

record an asserted literal to unsat certification.

fn certificate_save(&mut self)

save the certification record to a file.

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 minimize_with_bi_clauses(&mut self, asg: &impl AssignIF, vec: &mut Vec<Lit>)

minimize a clause.

fn complete_bi_clauses(&mut self, asg: &mut impl AssignIF)

complete bi-clause network

impl Clone for ClauseDB

fn clone(&self) -> ClauseDB

Returns a copy of the value.

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

impl PropertyReference<TEma, EmaView> for ClauseDB

fn refer(&self, k: TEma) -> &EmaView

impl StochasticLocalSearchIF for ClauseDB

fn stochastic_local_search( &mut self, _asg: &impl AssignIF, assignment: &mut HashMap<VarId, bool>, limit: usize ) -> (usize, usize)

returns the decision level of the given assignment and the one of the final assignment. Note: the lower level a set of clauses make a conflict at, the higher learning rate a solver can keep and the better learnt clauses we will have. This would be a better criteria that can be used in CDCL solvers.

impl VivifyIF for ClauseDB

fn vivify( &mut self, asg: &mut AssignStack, state: &mut State ) -> MaybeInconsistent

vivify clauses under asg