Struct splr::assign::AssignStack

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 */
}

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

impl AssignStack

pub fn rescale_activity(&mut self, scaling: f64)

Trait Implementations

impl ActivityIF<usize> for AssignStack

fn activity(&self, vi: VarId) -> f64

return one’s activity.

fn set_activity(&mut self, vi: VarId, val: f64)

set activity

fn reward_at_analysis(&mut self, vi: VarId)

modify one’s activity at conflict analysis in conflict_analyze in solver.

fn reward_at_assign(&mut self, _vi: VarId)

modify one’s activity at value assignment in assign.

fn reward_at_propagation(&mut self, _vi: VarId)

modify one’s activity at value assignment in unit propagation.

fn reward_at_unassign(&mut self, vi: VarId)

modify one’s activity at value un-assignment in cancel_until.

fn update_activity_decay(&mut self, scaling: f64)

update reward decay.

fn update_activity_tick(&mut self)

update internal counter.

impl AssignIF for AssignStack

fn root_level(&self) -> DecisionLevel

return root level.

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

return a literal in the stack.

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

return literals in the range of stack.

fn stack_len(&self) -> usize

return the number of assignments.

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

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

fn stack_is_empty(&self) -> bool

return true if there’s no assignment.

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

return an iterator over assignment stack.

fn decision_level(&self) -> DecisionLevel

return the current decision level.

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

return the decision var’s id at that level.

fn remains(&self) -> bool

return true if there are un-propagated assignments.

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

return a reference to assign.

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

return a reference to level.

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

fn best_phases_invalid(&self) -> bool

return true if no best_phases

fn extend_model(&mut self, cdb: &mut impl ClauseDBIF) -> Vec<Option<bool>>

inject assignments for eliminated vars.

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

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

impl Clone for AssignStack

fn clone(&self) -> AssignStack

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for AssignStack

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for AssignStack

fn default() -> AssignStack

Returns the “default value” for a type.

impl Display for AssignStack

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl From<&mut AssignStack> for Vec<i32>

fn from(asg: &mut AssignStack) -> Vec<i32>

Converts to this type from the input type.

impl Instantiate for AssignStack

fn instantiate(config: &Config, cnf: &CNFDescription) -> AssignStack

make and return an object from Config and CNFDescription.

fn handle(&mut self, e: SolverEvent)

update by a solver event.

impl<'a> IntoIterator for &'a mut AssignStack

type Item = &'a Lit

The type of the elements being iterated over.

type IntoIter = Iter<'a, Lit>

Which kind of iterator are we turning this into?

fn into_iter(self) -> Self::IntoIter

Creates an iterator from a value.

impl PropagateIF for AssignStack

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.

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

add an assignment at root level as a precondition.

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

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

fn assign_by_decision(&mut self, l: Lit)

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

fn cancel_until(&mut self, lv: DecisionLevel)

execute backjump.

fn backtrack_sandbox(&mut self)

execute backjump in vivification sandbox

fn propagate_sandbox(&mut self, cdb: &mut impl ClauseDBIF) -> PropagationResult

propagate for vivification, which allows dead clauses.

fn clear_asserted_literals( &mut self, cdb: &mut impl ClauseDBIF ) -> MaybeInconsistent

propagate then clear asserted literals

impl PropertyDereference<Tf64, f64> for AssignStack

fn derefer(&self, k: Tf64) -> f64

impl PropertyDereference<Tusize, usize> for AssignStack

fn derefer(&self, k: Tusize) -> usize

impl PropertyReference<TEma, EmaView> for AssignStack

fn refer(&self, k: TEma) -> &EmaView

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)

impl VarManipulateIF for AssignStack

fn assigned(&self, l: Lit) -> Option<bool>

return the value of a literal.

fn assign(&self, vi: VarId) -> Option<bool>

return the assignment of var.

fn level(&self, vi: VarId) -> DecisionLevel

return the assign level of var.

fn reason(&self, vi: VarId) -> AssignReason

return the reason of assignment.

fn var(&self, vi: VarId) -> &Var

return the var.

fn var_mut(&mut self, vi: VarId) -> &mut Var

return the var.

fn var_iter(&self) -> Iter<'_, Var>

return an iterator over Vars.

fn var_iter_mut(&mut self) -> IterMut<'_, Var>

return an mutable iterator over Vars.

fn make_var_asserted(&mut self, vi: VarId)

set var status to asserted.

fn make_var_eliminated(&mut self, vi: VarId)

set var status to eliminated.

impl VarSelectIF for AssignStack

fn best_phases_ref( &mut self, default_value: Option<bool> ) -> HashMap<VarId, bool>

return best phases

fn override_rephasing_target( &mut self, assignment: &HashMap<VarId, bool> ) -> usize

force an assignment obtained by SLS

fn reward_by_sls(&mut self, assignment: &HashMap<VarId, bool>) -> usize

give rewards to vars selected by SLS

fn select_rephasing_target(&mut self)

select rephasing target

fn check_consistency_of_best_phases(&mut self)

check the consistency

fn select_decision_literal(&mut self) -> Lit

select a new decision variable.

fn update_order(&mut self, v: VarId)

update the internal heap on var order.

fn rebuild_order(&mut self)

rebuild the internal var_order