Struct splr::processor::Eliminator

pub struct Eliminator {
    pub enable: bool,
    pub to_simplify: f64,
    pub eliminate_var_occurrence_limit: usize,
    pub eliminate_combination_limit: usize,
    pub eliminate_grow_limit: usize,
    pub eliminate_occurrence_limit: usize,
    // some fields omitted
}

Literal eliminator

Fields

enable: bool

to_simplify: f64

eliminate_var_occurrence_limit: usize

Maximum number of clauses to try to eliminate a var

eliminate_combination_limit: usize

0 for no limit Stop elimination if a generated resolvent is larger than this 0 means no limit.

eliminate_grow_limit: usize

Stop elimination if the increase of clauses is over this

eliminate_occurrence_limit: usize

A criteria by the product’s of its positive occurrences and negative ones

Implementations

impl Eliminator

pub fn try_subsume<A, C>(
    &mut self,
    asg: &mut A,
    cdb: &mut C,
    cid: ClauseId,
    did: ClauseId
) -> MaybeInconsistent where
    A: AssignIF,
    C: ClauseDBIF, 

impl Eliminator

pub fn eliminate_satisfied_clauses<A, C>(
    &mut self,
    asg: &mut A,
    cdb: &mut C,
    update_occur: bool
) where
    A: AssignIF,
    C: ClauseDBIF, 

delete satisfied clauses at decision level zero.

Trait Implementations

impl Clone for Eliminator

fn clone(&self) -> Eliminator

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for Eliminator

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

Formats the value using the given formatter.

impl Default for Eliminator

fn default() -> Eliminator

Returns the “default value” for a type.

impl EliminateIF for Eliminator

fn activate(&mut self)

set eliminator’s mode to ready.

fn is_running(&self) -> bool

check if the eliminator is running.

fn stop<A, C>(&mut self, asg: &mut A, cdb: &mut C) where
    A: AssignIF,
    C: ClauseDBIF, 

set eliminator’s mode to dormant.

fn prepare<A, C>(&mut self, asg: &mut A, cdb: &mut C, force: bool) where
    A: AssignIF,
    C: ClauseDBIF, 

rebuild occur lists.

fn enqueue_var<A>(&mut self, asg: &mut A, vi: VarId, upward: bool) where
    A: AssignIF, 

enqueue a var into eliminator’s var queue.

fn simplify<A, C, R>(
    &mut self,
    asg: &mut A,
    cdb: &mut C,
    rst: &mut R,
    state: &mut State
) -> MaybeInconsistent where
    A: AssignIF,
    C: ClauseDBIF,
    R: RestartIF, 

simplify database by:

fn add_cid_occur<A>(
    &mut self,
    asg: &mut A,
    cid: ClauseId,
    c: &mut Clause,
    enqueue: bool
) where
    A: AssignIF, 

register a clause id to all corresponding occur lists.

fn remove_cid_occur<A>(&mut self, asg: &mut A, cid: ClauseId, c: &mut Clause) where
    A: AssignIF, 

remove a clause id from all corresponding occur lists.

fn sorted_iterator(&self) -> Iter<'_, usize>

return the order of vars based on their occurrences

fn stats(&self, vi: VarId) -> Option<(usize, usize)>

return vi’s stats

fn eliminated_lits(&self) -> &[Lit]

return the constraints on eliminated literals.

impl Index<&'_ Lit> for Eliminator

type Output = LitOccurs

The returned type after indexing.

fn index(&self, l: &Lit) -> &Self::Output

Performs the indexing (container[index]) operation.

impl Index<&'_ usize> for Eliminator

type Output = LitOccurs

The returned type after indexing.

fn index(&self, i: &VarId) -> &Self::Output

Performs the indexing (container[index]) operation.

impl Index<Lit> for Eliminator

type Output = LitOccurs

The returned type after indexing.

fn index(&self, l: Lit) -> &Self::Output

Performs the indexing (container[index]) operation.

impl Index<Range<usize>> for Eliminator

type Output = [LitOccurs]

The returned type after indexing.

fn index(&self, r: Range<usize>) -> &Self::Output

Performs the indexing (container[index]) operation.

impl Index<RangeFrom<usize>> for Eliminator

type Output = [LitOccurs]

The returned type after indexing.

fn index(&self, r: RangeFrom<usize>) -> &Self::Output

Performs the indexing (container[index]) operation.

impl Index<usize> for Eliminator

type Output = LitOccurs

The returned type after indexing.

fn index(&self, i: VarId) -> &Self::Output

Performs the indexing (container[index]) operation.

impl IndexMut<&'_ Lit> for Eliminator

fn index_mut(&mut self, l: &Lit) -> &mut Self::Output

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

impl IndexMut<&'_ usize> for Eliminator

fn index_mut(&mut self, i: &VarId) -> &mut Self::Output

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

impl IndexMut<Lit> for Eliminator

fn index_mut(&mut self, l: Lit) -> &mut Self::Output

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

impl IndexMut<Range<usize>> for Eliminator

fn index_mut(&mut self, r: Range<usize>) -> &mut Self::Output

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

impl IndexMut<RangeFrom<usize>> for Eliminator

fn index_mut(&mut self, r: RangeFrom<usize>) -> &mut Self::Output

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

impl IndexMut<usize> for Eliminator

fn index_mut(&mut self, i: VarId) -> &mut Self::Output

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

impl Instantiate for Eliminator

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

make and return an object from Config and CNFDescription.

fn handle(&mut self, e: SolverEvent)

update by a solver event.

impl PropertyDereference<Tusize, usize> for Eliminator

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