Struct splr::processor::Eliminator

pub struct Eliminator {
    pub num_subsumed: usize,
    /* private fields */
}

Literal eliminator

Fields

num_subsumed: usize

Implementations

impl Eliminator

pub fn add_cid_occur( &mut self, asg: &mut impl AssignIF, cid: ClauseId, c: &mut Clause, enqueue: bool )

register a clause id to all corresponding occur lists.

pub fn remove_cid_occur( &mut self, asg: &mut impl AssignIF, cid: ClauseId, c: &mut Clause )

remove a clause id from all corresponding occur lists.

pub fn backward_subsumption_check( &mut self, asg: &mut impl AssignIF, cdb: &mut impl ClauseDBIF, timedout: &mut usize ) -> MaybeInconsistent

returns false if solver is inconsistent

• calls clause_queue.pop

pub fn remove_lit_occur( &mut self, asg: &mut impl AssignIF, l: Lit, cid: ClauseId )

remove a clause id from literal’s occur list.

pub fn enqueue_clause(&mut self, cid: ClauseId, c: &mut Clause)

clause queue operations

enqueue a clause into eliminator’s clause queue.

impl Eliminator

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

Trait Implementations

impl Clone for Eliminator

fn clone(&self) -> Eliminator

Returns a copy of the value.

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 is_running(&self) -> bool

check if the eliminator is running.

fn prepare( &mut self, asg: &mut impl AssignIF, cdb: &mut impl ClauseDBIF, force: bool )

rebuild occur lists.

fn enqueue_var(&mut self, asg: &mut impl AssignIF, vi: VarId, upward: bool)

enqueue a var into eliminator’s var queue.

fn simplify( &mut self, asg: &mut impl AssignIF, cdb: &mut impl ClauseDBIF, state: &mut State, force_run: bool ) -> MaybeInconsistent

simplify database by:

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

return the order of vars based on their occurrences

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

return vi’s stats

fn eliminated_lits(&mut self) -> &mut Vec<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.