[−][src]Trait splr::assign::PropagateIF
API for Boolean Constraint Propagation like propagate
, assign_by_decision
, cancel_until
, and so on.
Required methods
pub 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.
pub fn assign_by_implication(
&mut self,
l: Lit,
reason: AssignReason,
lv: DecisionLevel
)
[src]
&mut self,
l: Lit,
reason: AssignReason,
lv: DecisionLevel
)
unsafe enqueue (assign by implication); doesn't emit an exception.
Warning
Callers must assure the consistency after this assignment.
pub 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.
pub 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.
pub fn cancel_until(&mut self, lv: DecisionLevel)
[src]
execute backjump.
pub fn propagate<C>(&mut self, cdb: &mut C) -> ClauseId where
C: ClauseDBIF,
[src]
C: ClauseDBIF,
execute boolean constraint propagation or unit propagation.
Implementors
impl PropagateIF for AssignStack
[src]
pub fn assign_at_root_level(&mut self, l: Lit) -> MaybeInconsistent
[src]
pub fn assign_by_implication(
&mut self,
l: Lit,
reason: AssignReason,
lv: DecisionLevel
)
[src]
&mut self,
l: Lit,
reason: AssignReason,
lv: DecisionLevel
)
pub fn assign_by_decision(&mut self, l: Lit)
[src]
pub fn assign_by_unitclause(&mut self, l: Lit)
[src]
pub fn cancel_until(&mut self, lv: DecisionLevel)
[src]
pub fn propagate<C>(&mut self, cdb: &mut C) -> ClauseId where
C: ClauseDBIF,
[src]
C: ClauseDBIF,
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.