Struct splr::eliminator::Eliminator

pub struct Eliminator {
    pub enable: bool,
    pub eliminate_combination_limit: usize,
    pub eliminate_grow_limit: usize,
    pub eliminate_loop_limit: usize,
    pub subsume_literal_limit: usize,
    pub subsume_loop_limit: usize,
    // some fields omitted
}

Literal eliminator

Fields

enable: bool

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_loop_limit: usize

subsume_literal_limit: usize

Stop subsumption if the size of a clause is over this

subsume_loop_limit: usize

Trait Implementations

impl EliminatorIF for Eliminator

fn new(config: &Config, nv: usize) -> Eliminator

return a new instance.

fn activate(&mut self)

set eliminater's mode to ready.

fn is_running(&self) -> bool

check if the eliminator is running.

fn is_waiting(&self) -> bool

check if the eliminator is active and waits for next eliminate.

fn stop(&mut self, cdb: &mut ClauseDB, vars: &mut VarDB)

set eliminater's mode to dormant.

fn prepare(&mut self, cdb: &mut ClauseDB, vars: &mut VarDB, force: bool)

rebuild occur lists.

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

enqueue a clause into eliminator's clause queue.

fn clear_clause_queue(&mut self, cdb: &mut ClauseDB)

clear eliminator's clause queue.

fn enqueue_var(&mut self, vars: &mut VarDB, vi: VarId, upward: bool)

enqueue a var into eliminator's var queue.

fn clear_var_queue(&mut self, vars: &mut VarDB)

clear eliminator's war queue

fn clause_queue_len(&self) -> usize

return the length of eliminator's clause queue.

fn var_queue_len(&self) -> usize

return the length of eliminator's clause queue.

fn eliminate(
    &mut self,
    asgs: &mut AssignStack,
    cdb: &mut ClauseDB,
    state: &mut State,
    vars: &mut VarDB
) -> MaybeInconsistent

run clause subsumption and variable elimination.

fn extend_model(&mut self, model: &mut Vec<i32>)

add assignments for eliminated vars to model.

fn add_cid_occur(
    &mut self,
    vars: &mut VarDB,
    cid: ClauseId,
    c: &mut Clause,
    enqueue: bool
)

register a clause id to all corresponding occur lists.

fn remove_lit_occur(&mut self, vars: &mut VarDB, l: Lit, cid: ClauseId)

remove a clause id from literal's occur list.

fn remove_cid_occur(&mut self, vars: &mut VarDB, cid: ClauseId, c: &mut Clause)

remove a clause id from all corresponding occur lists.

impl Default for Eliminator

fn default() -> Eliminator

Returns the "default value" for a type.

impl Debug for Eliminator

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

Formats the value using the given formatter.