Struct varisat::prop::assignment::Trail

pub struct Trail {
    trail: Vec<Lit>,
    queue_head_pos: usize,
    decisions: Vec<LitIdx>,
    units_removed: usize,
}

Decision and propagation history.

Fields

trail: Vec<Lit>

Stack of all propagated and all enqueued assignments

queue_head_pos: usize

Next assignment in trail to propagate

decisions: Vec<LitIdx>

Decision levels as trail indices.

units_removed: usize

Number of unit clauses removed from the trail.

Methods

impl Trail

pub fn queue_head(&self) -> Option<Lit>

Return the next assigned literal to propagate.

pub fn pop_queue(&mut self) -> Option<Lit>

Return the next assigned literal to propagate and remove it from the queue.

pub fn reset_queue(&mut self)

Re-enqueue all assigned literals.

pub fn trail(&self) -> &[Lit]

Assigned literals in assignment order.

pub fn clear(&mut self)

Clear the trail.

This simply removes all entries without performing any backtracking. Can only be called with no active decisions.

pub fn new_decision_level(&mut self)

Start a new decision level.

Does not enqueue the decision itself.

pub fn current_level(&self) -> usize

Current decision level.

pub fn top_level_assignment_count(&self) -> usize

The number of assignments at level 0.

pub fn fully_propagated(&self) -> bool

Whether all assignments are processed.

Trait Implementations

impl Default for Trail

fn default() -> Trail

Returns the "default value" for a type.