Trait splr::processor::EliminateIF[−][src]

pub trait EliminateIF: Instantiate {
    fn activate(&mut self);

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

    fn is_running(&self) -> bool;

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

    fn enqueue_var<A>(&mut self, asg: &mut A, vi: VarId, upward: bool)
    where
        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;

    fn add_cid_occur<A>(
        &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;

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

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

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

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]

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]

rebuild occur lists.

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

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]

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]

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]

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.

Loading content...

Implementors

impl EliminateIF for Eliminator[src]

Loading content...