[−][src]Trait splr::traits::PropagatorIF

pub trait PropagatorIF {
    fn new(n: usize) -> Self;

    fn len(&self) -> usize;

    fn is_empty(&self) -> bool;

    fn level(&self) -> usize;

    fn is_zero(&self) -> bool;

    fn num_at(&self, n: usize) -> usize;

    fn remains(&self) -> bool;

    fn assigned(&self, l: Lit) -> Lbool;

    fn propagate(
        &mut self, 
        cdb: &mut ClauseDB, 
        state: &mut State, 
        vars: &mut VarDB
    ) -> ClauseId;

    fn cancel_until(&mut self, vars: &mut VarDB, lv: usize);

    fn enqueue(
        &mut self, 
        v: &mut Var, 
        sig: Lbool, 
        cid: ClauseId, 
        dl: usize
    ) -> MaybeInconsistent;

    fn enqueue_null(&mut self, v: &mut Var, sig: Lbool);

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

    fn uncheck_assume(&mut self, vars: &mut VarDB, l: Lit);

    fn update_order(&mut self, vec: &VarDB, v: VarId);

    fn select_var(&mut self, vars: &VarDB) -> VarId;

    fn dump_cnf(
        &mut self, 
        cdb: &ClauseDB, 
        state: &State, 
        vars: &VarDB, 
        fname: &str
    );
}

API for assignment like propagate, enqueue, cancel_until, and so on.

Required methods

fn new(n: usize) -> Self

return a new instance.

fn len(&self) -> usize

return the number of assignments.

fn is_empty(&self) -> bool

return true if there's no assignment.

fn level(&self) -> usize

return the current decision level.

fn is_zero(&self) -> bool

return true if the current decision level is zero.

fn num_at(&self, n: usize) -> usize

return the number of assignments at a given decision level u.

fn remains(&self) -> bool

return true if there are unpropagated assignments.

fn assigned(&self, l: Lit) -> Lbool

return the value of a given literal.

fn propagate(
    &mut self,
    cdb: &mut ClauseDB,
    state: &mut State,
    vars: &mut VarDB
) -> ClauseId

execute propagate.

fn cancel_until(&mut self, vars: &mut VarDB, lv: usize)

execute backjump.

fn enqueue(
    &mut self,
    v: &mut Var,
    sig: Lbool,
    cid: ClauseId,
    dl: usize
) -> MaybeInconsistent

add an assignment caused by a clause; emit an exception if solver becomes inconsistent.

Errors

if solver becomes inconsistent by the new assignment.

fn enqueue_null(&mut self, v: &mut Var, sig: Lbool)

add an assignment with no reason clause without inconsistency check.

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

unsafe enqueue; doesn't emit an exception.

fn uncheck_assume(&mut self, vars: &mut VarDB, l: Lit)

unsafe assume; doesn't emit an exception.

fn update_order(&mut self, vec: &VarDB, v: VarId)

update the internal heap on var order.

fn select_var(&mut self, vars: &VarDB) -> VarId

select a new decision variable.

fn dump_cnf(&mut self, cdb: &ClauseDB, state: &State, vars: &VarDB, fname: &str)

dump all active clauses and fixed assignments in solver to a CNF file fname.

Loading content...

Implementors

impl PropagatorIF for AssignStack[src]

fn propagate(
    &mut self,
    cdb: &mut ClauseDB,
    state: &mut State,
    vars: &mut VarDB
) -> ClauseId[src]

propagate without checking dead clauses Note: this function assumes there's no dead clause. So Eliminator should call garbage_collect before me.

Loading content...