Struct splr::cdb::ClauseDB

pub struct ClauseDB {
    pub bi_clause: Vec<HashMap<Lit, ClauseId>>,
    pub watch_cache: Vec<Vec<(ClauseId, Lit)>>,
    pub lbd_of_dp_ema: Ema,
    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

bi_clause: Vec<HashMap<Lit, ClauseId>>

hashed representation of binary clauses.

Note

This means a biclause [l0, l1] is stored at bi_clause[l0] instead of bi_clause[!l0].

watch_cache: Vec<Vec<(ClauseId, Lit)>>

container of watch literals

lbd_of_dp_ema: Ema

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

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 detach_clause(&mut self, cid: ClauseId) -> (Lit, Lit)

remove a clause temporally

fn reattach_clause(&mut self, cid: ClauseId, (l0, l1): (Lit, Lit))

push back a clause

fn remove_clause(&mut self, cid: ClauseId)

Warning

this function is the only function that makes dead clauses

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 bi_clause_map(&self, l: Lit) -> &HashMap<Lit, ClauseId>

return a watcher list for bi-clauses

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 reregister_watch_cache(&mut self, _: Lit, _: Option<usize>)

register the clause to the previous watch cache

fn restore_detached_watch_cache(&mut self, _: Lit, _: WatchCacheIterator)

restore detached watch cache

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<A>(
    &mut self,
    asg: &mut A,
    vec: &mut Vec<Lit>,
    learnt: bool
) -> RefClause where
    A: AssignIF, 

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

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<A>(
    &mut self,
    asg: &mut A,
    cid: ClauseId
) -> RefClause where
    A: AssignIF, 

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 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 reduce<A>(&mut self, asg: &mut A, num_conflicts: usize) -> bool where
    A: AssignIF, 

check the condition to reduce.

fn reset(&mut self)

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

minimize a clause.

fn complete_bi_clauses<A>(&mut self, asg: &mut A) where
    A: 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