Trait splr::processor::EliminateIF [−][src]
API for Eliminator like activate
, stop
, eliminate
and so on.
use crate::{splr::config::Config, splr::types::*}; use crate::splr::processor::{Eliminator, EliminateIF}; use crate::splr::solver::Solver; let mut s = Solver::instantiate(&Config::default(), &CNFDescription::default()); let elim = &mut s.elim; assert_eq!(elim.is_running(), false); elim.activate(); // At this point, the `elim` is in `ready` mode, not `running`. assert_eq!(elim.is_running(), false); assert_eq!(elim.simplify(&mut s.asg, &mut s.cdb, &mut s.rst, &mut s.state), Ok(()));
Required methods
fn activate(&mut self)
[src]
set eliminator’s mode to ready.
fn stop<A, C>(&mut self, asg: &mut A, cdb: &mut C) where
A: AssignIF,
C: ClauseDBIF,
[src]
A: AssignIF,
C: ClauseDBIF,
set eliminator’s mode to dormant.
fn is_running(&self) -> bool
[src]
check if the eliminator is running.
fn prepare<A, C>(&mut self, asg: &mut A, cdb: &mut C, force: bool) where
A: AssignIF,
C: ClauseDBIF,
[src]
A: AssignIF,
C: ClauseDBIF,
rebuild occur lists.
fn enqueue_var<A>(&mut self, asg: &mut A, vi: VarId, upward: bool) where
A: AssignIF,
[src]
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,
[src]
&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:
- removing satisfiable clauses
- calling exhaustive simplifier that tries clause subsumption and variable elimination.
Errors
if solver becomes inconsistent.
fn add_cid_occur<A>(
&mut self,
asg: &mut A,
cid: ClauseId,
c: &mut Clause,
enqueue: bool
) where
A: AssignIF,
[src]
&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,
[src]
A: AssignIF,
remove a clause id from all corresponding occur lists.
fn sorted_iterator(&self) -> Iter<'_, usize>
[src]
return the order of vars based on their occurrences
fn stats(&self, vi: VarId) -> Option<(usize, usize)>
[src]
return vi’s stats
fn eliminated_lits(&self) -> &[Lit]
[src]
return the constraints on eliminated literals.
Implementors
impl EliminateIF for Eliminator
[src]
fn activate(&mut self)
[src]
fn is_running(&self) -> bool
[src]
fn stop<A, C>(&mut self, asg: &mut A, cdb: &mut C) where
A: AssignIF,
C: ClauseDBIF,
[src]
A: AssignIF,
C: ClauseDBIF,
fn prepare<A, C>(&mut self, asg: &mut A, cdb: &mut C, force: bool) where
A: AssignIF,
C: ClauseDBIF,
[src]
A: AssignIF,
C: ClauseDBIF,
fn enqueue_var<A>(&mut self, asg: &mut A, vi: VarId, upward: bool) where
A: AssignIF,
[src]
A: AssignIF,
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,
[src]
&mut self,
asg: &mut A,
cdb: &mut C,
rst: &mut R,
state: &mut State
) -> MaybeInconsistent where
A: AssignIF,
C: ClauseDBIF,
R: RestartIF,
fn add_cid_occur<A>(
&mut self,
asg: &mut A,
cid: ClauseId,
c: &mut Clause,
enqueue: bool
) where
A: AssignIF,
[src]
&mut self,
asg: &mut A,
cid: ClauseId,
c: &mut Clause,
enqueue: bool
) where
A: AssignIF,
fn remove_cid_occur<A>(&mut self, asg: &mut A, cid: ClauseId, c: &mut Clause) where
A: AssignIF,
[src]
A: AssignIF,