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

pub trait AssignIF: ActivityIF<VarId> + Instantiate + PropagateIF + VarManipulateIF + PropertyDereference<Tusize, usize> + PropertyReference<TEma, Ema> {
    fn stack(&self, i: usize) -> Lit;

    fn stack_range(&self, r: Range<usize>) -> &[Lit];

    fn stack_len(&self) -> usize;

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

    fn stack_is_empty(&self) -> bool;

    fn stack_iter(&self) -> Iter<'_, Lit>;

    fn decision_level(&self) -> DecisionLevel;

    fn decision_vi(&self, lv: DecisionLevel) -> VarId;

    fn remains(&self) -> bool;

    fn assign_ref(&self) -> &[Option<bool>];

    fn level_ref(&self) -> &[DecisionLevel];

    fn best_assigned(&mut self) -> Option<usize>;

    fn extend_model<C>(&mut self, c: &mut C, lits: &[Lit]) -> Vec<Option<bool>>
    where
        C: ClauseDBIF;

    fn satisfies(&self, c: &[Lit]) -> bool;

    fn locked(&self, c: &Clause, cid: ClauseId) -> bool;
}

API about assignment like decision_level, stack, best_assigned, and so on.

Required methods

fn stack(&self, i: usize) -> Lit[src]

return a literal in the stack.

fn stack_range(&self, r: Range<usize>) -> &[Lit][src]

return literals in the range of stack.

fn stack_len(&self) -> usize[src]

return the number of assignments.

fn len_upto(&self, n: DecisionLevel) -> usize[src]

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

Caveat

  • it emits a panic by out of index range.
  • it emits a panic if the level is 0.

fn stack_is_empty(&self) -> bool[src]

return true if there’s no assignment.

fn stack_iter(&self) -> Iter<'_, Lit>[src]

return an iterator over assignment stack.

fn decision_level(&self) -> DecisionLevel[src]

return the current decision level.

fn decision_vi(&self, lv: DecisionLevel) -> VarId[src]

return the decision var’s id at that level.

fn remains(&self) -> bool[src]

return true if there are un-propagated assignments.

fn assign_ref(&self) -> &[Option<bool>][src]

return a reference to assign.

fn level_ref(&self) -> &[DecisionLevel][src]

return a reference to level.

fn best_assigned(&mut self) -> Option<usize>[src]

fn extend_model<C>(&mut self, c: &mut C, lits: &[Lit]) -> Vec<Option<bool>> where
    C: ClauseDBIF, [src]

inject assignments for eliminated vars.

fn satisfies(&self, c: &[Lit]) -> bool[src]

return true if the set of literals is satisfiable under the current assignment.

fn locked(&self, c: &Clause, cid: ClauseId) -> bool[src]

return true is the clause is the reason of the assignment.

Loading content...

Implementors

impl AssignIF for AssignStack[src]

Loading content...