Trait splr::assign::AssignIF [−][src]
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]
C: ClauseDBIF,
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.
Implementors
impl AssignIF for AssignStack
[src]
fn stack(&self, i: usize) -> Lit
[src]
fn stack_range(&self, r: Range<usize>) -> &[Lit]
[src]
fn stack_len(&self) -> usize
[src]
fn len_upto(&self, n: DecisionLevel) -> usize
[src]
fn stack_is_empty(&self) -> bool
[src]
fn stack_iter(&self) -> Iter<'_, Lit>
[src]
fn decision_level(&self) -> DecisionLevel
[src]
fn decision_vi(&self, lv: DecisionLevel) -> VarId
[src]
fn remains(&self) -> bool
[src]
fn assign_ref(&self) -> &[Option<bool>]
[src]
fn level_ref(&self) -> &[DecisionLevel]
[src]
fn best_assigned(&mut self) -> Option<usize>
[src]
fn extend_model<C>(&mut self, cdb: &mut C, lits: &[Lit]) -> Vec<Option<bool>> where
C: ClauseDBIF,
[src]
C: ClauseDBIF,