Trait splr::assign::PropagateIF[−][src]

pub trait PropagateIF {
    fn assign_at_root_level(&mut self, l: Lit) -> MaybeInconsistent;

    fn assign_by_implication(
        &mut self, 
        l: Lit, 
        reason: AssignReason, 
        lv: DecisionLevel
    );

    fn assign_by_decision(&mut self, l: Lit);

    fn assign_by_unitclause(&mut self, l: Lit);

    fn cancel_until(&mut self, lv: DecisionLevel);

    fn backtrack_sandbox(&mut self);

    fn propagate<C>(&mut self, cdb: &mut C) -> ClauseId
    where
        C: ClauseDBIF;
}

API for Boolean Constraint Propagation like propagate, assign_by_decision, cancel_until, and so on.

Required methods

fn assign_at_root_level(&mut self, l: Lit) -> MaybeInconsistent[src]

add an assignment at level 0 as a precondition.

Errors

emit SolverError::Inconsistent exception if solver becomes inconsistent.

fn assign_by_implication(
    &mut self,
    l: Lit,
    reason: AssignReason,
    lv: DecisionLevel
)[src]

unsafe enqueue (assign by implication); doesn’t emit an exception.

Warning

Callers must assure the consistency after this assignment.

fn assign_by_decision(&mut self, l: Lit)[src]

unsafe assume (assign by decision); doesn’t emit an exception.

Caveat

Callers have to assure the consistency after this assignment.

fn assign_by_unitclause(&mut self, l: Lit)[src]

fix a var’s assignment by a unit learnt clause.

Caveat

  • Callers have to assure the consistency after this assignment.
  • No need to restart; but execute propagate just afterward.

fn cancel_until(&mut self, lv: DecisionLevel)[src]

execute backjump.

fn backtrack_sandbox(&mut self)[src]

execute backjump in vivifiacion sandbox

fn propagate<C>(&mut self, cdb: &mut C) -> ClauseId where
    C: ClauseDBIF, [src]

execute boolean constraint propagation or unit propagation.

Loading content...

Implementors

impl PropagateIF for AssignStack[src]

fn propagate<C>(&mut self, cdb: &mut C) -> ClauseId where
    C: ClauseDBIF, [src]

UNIT PROPAGATION. Note:

  • Precondition: no checking dead clauses. They cause crash.
  • This function assumes there’s no dead clause. So Eliminator should call garbage_collect before me.
  • The order of literals in binary clauses will be modified to hold propagation order.
Loading content...