Struct Trail 

pub struct Trail<L: Literal, S: LiteralStorage<L>> {
    pub curr_idx: usize,
    pub lit_to_pos: Vec<usize>,
    /* private fields */
}

The trail itself, storing the sequence of assignments and related metadata.

The trail is a fundamental data structure in a CDCL SAT solver. It maintains the current partial assignment, the reasons for implications, and decision levels. L is the literal type, and S is the literal storage type used by clauses.

Fields

curr_idx: usize

Index pointing to the next literal to be propagated in t. Assignments from t[0] to t[curr_idx - 1] have been processed (propagated). Assignments from t[curr_idx] onwards are pending propagation.

lit_to_pos: Vec<usize>

Maps a variable (by its u32 ID) to its position (index) in the t vector. lit_to_pos[var_id] = index_in_t. Stores 0 if the variable is unassigned (as t[0] is a valid position, this relies on checking lit_to_level or other means to confirm assignment for var at pos 0). More accurately, a non-zero value means it’s assigned and on the trail.

Implementations

impl<L: Literal, S: LiteralStorage<L>> Trail<L, S>

pub fn decision_level(&self) -> usize

Returns the current decision level.

The decision level is determined by the last assignment on the trail. If the trail is empty or only contains assignments at level 0, it returns 0. Otherwise, it returns the decision level of the assignment at curr_idx - 1.

pub const fn len(&self) -> usize

Returns the total number of assignments currently on the trail.

pub const fn is_empty(&self) -> bool

Checks if the trail is empty (contains no assignments).

pub fn level(&self, v: u32) -> usize

Returns the decision level at which variable v was assigned. Returns 0 if the variable is unassigned or was assigned at level 0.

Safety

This function uses get_unchecked and assumes v (cast to usize) is a valid index into lit_to_level. This means v must be less than num_vars used to initialise the Trail.

pub fn solutions(&self) -> Solutions

Constructs a Solutions object from the current assignments on the trail. This represents a complete model if the solver found satisfiability.

pub fn new(clauses: &[Clause<L, S>], num_vars: usize) -> Self

Creates a new Trail.

Initialises the trail, potentially adding assignments from unit clauses found in the initial clauses set. These initial assignments are at decision level 0.

Arguments

• clauses: A slice of initial clauses. Unit clauses from this set will be added to the trail.
• num_vars: The total number of variables in the problem. This is used to size internal mapping vectors.

Safety

The internal initialisation of lit_to_pos for unit clauses uses get_unchecked_mut. This is safe if lit.variable() from a unit clause is less than num_vars.

pub fn push(&mut self, lit: L, decision_level: usize, reason: Reason)

Pushes a new assignment (literal) onto the trail.

If the variable of the literal is already assigned, this function does nothing. Otherwise, it adds a new Part to the trail and updates lit_to_level and lit_to_pos.

Arguments

• lit: The literal being assigned.
• decision_level: The decision level at which this assignment occurs.
• reason: The reason for this assignment.

Safety

Uses get_unchecked to check lit_to_pos and get_unchecked_mut to update lit_to_level and lit_to_pos.

pub fn reset(&mut self)

Resets the trail to an empty state.

Clears all assignments and resets curr_idx, lit_to_level, and lit_to_pos. This is used during solver restarts.

pub fn backstep_to<A: Assignment>(&mut self, a: &mut A, level: usize)

Backtracks assignments to a specified decision level.

Removes all assignments made at decision levels greater than or equal to level. For each removed assignment, it unassigns the corresponding variable in the Assignment object a. Updates curr_idx to point to the new end of the (propagated) trail.

Arguments

• a: A mutable reference to the Assignment object to update.
• level: The decision level to backtrack to. Assignments at this level and higher will be removed.

Safety

Uses get_unchecked and get_unchecked_mut on lit_to_level and lit_to_pos. Assumes variable IDs from self[i].lit.variable() are valid indices.

pub fn get_locked_clauses(&self) -> SmallVec<[usize; 16]>

Returns a list of clause indices that are “locked”.

A clause is considered locked if one of its literals is on the trail, and that literal was assigned as a result of an implication (i.e. Reason::Clause). Such clauses cannot be removed during database cleaning if the literal they implied is still on the trail, as they are part of the justification for the current assignment.

pub fn remap_clause_indices(&mut self, map: &FxHashMap<usize, usize>)

Remaps clause indices stored in Reason::Clause variants on the trail.

This is necessary after clause database cleanup operations (like removing redundant learnt clauses) where clause indices might change. Only indices of learnt clauses (those with original index >= self.cnf_non_learnt_idx) are considered for remapping.

Arguments

• map: A hash map where keys are old clause indices and values are new clause indices.

Trait Implementations

impl<L: Clone + Literal, S: Clone + LiteralStorage<L>> Clone for Trail<L, S>

fn clone(&self) -> Trail<L, S>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<L: Debug + Literal, S: Debug + LiteralStorage<L>> Debug for Trail<L, S>

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

Formats the value using the given formatter.

impl<L: Default + Literal, S: Default + LiteralStorage<L>> Default for Trail<L, S>

fn default() -> Trail<L, S>

Returns the “default value” for a type.

impl<L: Literal, S: LiteralStorage<L>> Index<usize> for Trail<L, S>

fn index(&self, index: usize) -> &Self::Output

Accesses a Part of the trail by its index.

Panics

This method will panic if index is out of bounds.

Safety

The unsafe block is used for a potential micro-optimisation by using get_unchecked.

type Output = Part<L>

The returned type after indexing.

impl<L: Literal, S: LiteralStorage<L>> IndexMut<usize> for Trail<L, S>

fn index_mut(&mut self, index: usize) -> &mut Self::Output

Mutably accesses a Part of the trail by its index.

Panics

This method will panic if index is out of bounds.

Safety

Similar to Index::index, this uses get_unchecked_mut.

impl<L: PartialEq + Literal, S: PartialEq + LiteralStorage<L>> PartialEq for Trail<L, S>

fn eq(&self, other: &Trail<L, S>) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl<L: Eq + Literal, S: Eq + LiteralStorage<L>> Eq for Trail<L, S>

impl<L: Literal, S: LiteralStorage<L>> StructuralPartialEq for Trail<L, S>