pub struct AssignStack {
pub stage_scale: usize,
pub eliminated: Vec<Lit>,
pub num_vars: usize,
pub num_asserted_vars: usize,
pub num_eliminated_vars: usize,
pub num_conflict: usize,
/* private fields */
}
Expand description
A record of assignment. It’s called ‘trail’ in Glucose.
Fields§
§stage_scale: usize
§eliminated: Vec<Lit>
§num_vars: usize
the number of vars.
num_asserted_vars: usize
the number of asserted vars.
num_eliminated_vars: usize
the number of eliminated vars.
num_conflict: usize
Implementations§
Source§impl AssignStack
impl AssignStack
pub fn rescale_activity(&mut self, scaling: f64)
Trait Implementations§
Source§impl ActivityIF<usize> for AssignStack
impl ActivityIF<usize> for AssignStack
Source§fn set_activity(&mut self, vi: VarId, val: f64)
fn set_activity(&mut self, vi: VarId, val: f64)
set activity
Source§fn reward_at_analysis(&mut self, vi: VarId)
fn reward_at_analysis(&mut self, vi: VarId)
modify one’s activity at conflict analysis in
conflict_analyze
in solver
.Source§fn reward_at_assign(&mut self, _vi: VarId)
fn reward_at_assign(&mut self, _vi: VarId)
modify one’s activity at value assignment in assign.
Source§fn reward_at_propagation(&mut self, _vi: VarId)
fn reward_at_propagation(&mut self, _vi: VarId)
modify one’s activity at value assignment in unit propagation.
Source§fn reward_at_unassign(&mut self, vi: VarId)
fn reward_at_unassign(&mut self, vi: VarId)
modify one’s activity at value un-assignment in
cancel_until
.Source§fn update_activity_decay(&mut self, scaling: f64)
fn update_activity_decay(&mut self, scaling: f64)
update reward decay.
Source§fn update_activity_tick(&mut self)
fn update_activity_tick(&mut self)
update internal counter.
Source§impl AssignIF for AssignStack
impl AssignIF for AssignStack
Source§fn root_level(&self) -> DecisionLevel
fn root_level(&self) -> DecisionLevel
return root level.
Source§fn len_upto(&self, n: DecisionLevel) -> usize
fn len_upto(&self, n: DecisionLevel) -> usize
return the number of assignments at a given decision level
u
. Read moreSource§fn stack_is_empty(&self) -> bool
fn stack_is_empty(&self) -> bool
return
true
if there’s no assignment.Source§fn stack_iter(&self) -> Iter<'_, Lit>
fn stack_iter(&self) -> Iter<'_, Lit>
return an iterator over assignment stack.
Source§fn decision_level(&self) -> DecisionLevel
fn decision_level(&self) -> DecisionLevel
return the current decision level.
Source§fn decision_vi(&self, lv: DecisionLevel) -> VarId
fn decision_vi(&self, lv: DecisionLevel) -> VarId
return the decision var’s id at that level.
Source§fn assign_ref(&self) -> &[Option<bool>]
fn assign_ref(&self) -> &[Option<bool>]
return a reference to
assign
.Source§fn level_ref(&self) -> &[DecisionLevel] ⓘ
fn level_ref(&self) -> &[DecisionLevel] ⓘ
return a reference to
level
.fn best_assigned(&mut self) -> Option<usize>
Source§fn best_phases_invalid(&self) -> bool
fn best_phases_invalid(&self) -> bool
return
true
if no best_phasesSource§fn extend_model(&mut self, cdb: &mut impl ClauseDBIF) -> Vec<Option<bool>>
fn extend_model(&mut self, cdb: &mut impl ClauseDBIF) -> Vec<Option<bool>>
inject assignments for eliminated vars.
Source§impl Clone for AssignStack
impl Clone for AssignStack
Source§fn clone(&self) -> AssignStack
fn clone(&self) -> AssignStack
Returns a copy of the value. Read more
1.0.0 · Source§fn clone_from(&mut self, source: &Self)
fn clone_from(&mut self, source: &Self)
Performs copy-assignment from
source
. Read moreSource§impl Debug for AssignStack
impl Debug for AssignStack
Source§impl Default for AssignStack
impl Default for AssignStack
Source§fn default() -> AssignStack
fn default() -> AssignStack
Returns the “default value” for a type. Read more
Source§impl Display for AssignStack
impl Display for AssignStack
Source§impl Instantiate for AssignStack
impl Instantiate for AssignStack
Source§fn instantiate(config: &Config, cnf: &CNFDescription) -> AssignStack
fn instantiate(config: &Config, cnf: &CNFDescription) -> AssignStack
make and return an object from
Config
and CNFDescription
.Source§fn handle(&mut self, e: SolverEvent)
fn handle(&mut self, e: SolverEvent)
update by a solver event.
Source§impl<'a> IntoIterator for &'a mut AssignStack
impl<'a> IntoIterator for &'a mut AssignStack
Source§impl PropagateIF for AssignStack
impl PropagateIF for AssignStack
Source§fn propagate(&mut self, cdb: &mut impl ClauseDBIF) -> PropagationResult
fn propagate(&mut self, cdb: &mut impl ClauseDBIF) -> PropagationResult
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.
Source§fn assign_at_root_level(&mut self, l: Lit) -> MaybeInconsistent
fn assign_at_root_level(&mut self, l: Lit) -> MaybeInconsistent
add an assignment at root level as a precondition. Read more
Source§fn assign_by_implication(&mut self, l: Lit, reason: AssignReason)
fn assign_by_implication(&mut self, l: Lit, reason: AssignReason)
unsafe enqueue (assign by implication); doesn’t emit an exception. Read more
Source§fn assign_by_decision(&mut self, l: Lit)
fn assign_by_decision(&mut self, l: Lit)
unsafe assume (assign by decision); doesn’t emit an exception. Read more
Source§fn cancel_until(&mut self, lv: DecisionLevel)
fn cancel_until(&mut self, lv: DecisionLevel)
execute backjump.
Source§fn backtrack_sandbox(&mut self)
fn backtrack_sandbox(&mut self)
execute backjump in vivification sandbox
Source§fn propagate_sandbox(&mut self, cdb: &mut impl ClauseDBIF) -> PropagationResult
fn propagate_sandbox(&mut self, cdb: &mut impl ClauseDBIF) -> PropagationResult
propagate
for vivification, which allows dead clauses.Source§fn clear_asserted_literals(
&mut self,
cdb: &mut impl ClauseDBIF,
) -> MaybeInconsistent
fn clear_asserted_literals( &mut self, cdb: &mut impl ClauseDBIF, ) -> MaybeInconsistent
propagate then clear asserted literals
Source§impl PropertyDereference<Tusize, usize> for AssignStack
impl PropertyDereference<Tusize, usize> for AssignStack
Source§impl PropertyReference<TEma, EmaView> for AssignStack
impl PropertyReference<TEma, EmaView> for AssignStack
Source§impl TrailSavingIF for AssignStack
impl TrailSavingIF for AssignStack
fn save_trail(&mut self, to_lvl: DecisionLevel)
fn reuse_saved_trail(&mut self, cdb: &impl ClauseDBIF) -> PropagationResult
fn clear_saved_trail(&mut self)
Source§impl VarManipulateIF for AssignStack
impl VarManipulateIF for AssignStack
Source§fn level(&self, vi: VarId) -> DecisionLevel
fn level(&self, vi: VarId) -> DecisionLevel
return the assign level of var.
Source§fn reason(&self, vi: VarId) -> AssignReason
fn reason(&self, vi: VarId) -> AssignReason
return the reason of assignment.
Source§fn var_iter_mut(&mut self) -> IterMut<'_, Var>
fn var_iter_mut(&mut self) -> IterMut<'_, Var>
return an mutable iterator over Vars.
Source§fn make_var_asserted(&mut self, vi: VarId)
fn make_var_asserted(&mut self, vi: VarId)
set var status to asserted.
Source§fn make_var_eliminated(&mut self, vi: VarId)
fn make_var_eliminated(&mut self, vi: VarId)
set var status to eliminated.
Source§impl VarSelectIF for AssignStack
impl VarSelectIF for AssignStack
Source§fn best_phases_ref(
&mut self,
default_value: Option<bool>,
) -> HashMap<VarId, bool>
fn best_phases_ref( &mut self, default_value: Option<bool>, ) -> HashMap<VarId, bool>
return best phases
Source§fn override_rephasing_target(
&mut self,
assignment: &HashMap<VarId, bool>,
) -> usize
fn override_rephasing_target( &mut self, assignment: &HashMap<VarId, bool>, ) -> usize
force an assignment obtained by SLS
Source§fn reward_by_sls(&mut self, assignment: &HashMap<VarId, bool>) -> usize
fn reward_by_sls(&mut self, assignment: &HashMap<VarId, bool>) -> usize
give rewards to vars selected by SLS
Source§fn select_rephasing_target(&mut self)
fn select_rephasing_target(&mut self)
select rephasing target
Source§fn check_consistency_of_best_phases(&mut self)
fn check_consistency_of_best_phases(&mut self)
check the consistency
Source§fn select_decision_literal(&mut self) -> Lit
fn select_decision_literal(&mut self) -> Lit
select a new decision variable.
Source§fn update_order(&mut self, v: VarId)
fn update_order(&mut self, v: VarId)
update the internal heap on var order.
Source§fn rebuild_order(&mut self)
fn rebuild_order(&mut self)
rebuild the internal var_order
Auto Trait Implementations§
impl Freeze for AssignStack
impl RefUnwindSafe for AssignStack
impl Send for AssignStack
impl Sync for AssignStack
impl Unpin for AssignStack
impl UnwindSafe for AssignStack
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more