Struct IncXor 

pub struct IncXor { /* private fields */ }

Incremental GF(2) engine — the fast DPLL(XOR) core.

The matrix is held in reduced row-echelon form and updated in O(affected-rows) work per variable assignment (each assignment is substituted out, with at most one re-pivot), not by re-running Gaussian over the whole system every call. A first-touch undo trail makes backtrack O(touched). Provenance is carried through every row XOR, so the forced/conflict explanation clauses are the same implied gadget clauses the recompute XorEngine produces. It is differentially tested against that recompute oracle under random assign/unassign sequences — the fast engine is proven equivalent to the proven-correct one before it ever drives the solver.

Implementations

impl IncXor

pub fn new(num_vars: usize, eqs: &[XorEquation]) -> Self

Build from recovered equations, reducing the matrix to RREF once.

pub fn is_active(&self) -> bool

pub fn assigned_len(&self) -> usize

pub fn assign(&mut self, var: usize, val: bool)

Assign var = val (it must currently be free), updating the matrix incrementally.

pub fn unassign(&mut self)

Undo the most recent assign. Each touched row is rolled back to its snapshot, and the occurrence index is restored by diffing the row’s current bits against that snapshot — every variable whose membership flipped is re-added or removed for that row.

pub fn density(&self) -> (usize, f64, usize)

Matrix density after the initial reduction: (rows, average row weight, max row weight). A dense reduced matrix (high average weight) is why eager Gauss-Jordan is slow and why the watch-based engine must avoid full densification.

pub fn next_branch(&self) -> Option<usize>

The next variable to branch (“break”) on: an unassigned non-pivot — a free/kernel degree of freedom the linear system does not determine. Deciding it lets Gaussian propagation force a fresh batch of pivots, collapsing the residual. Prefers a free variable that actually occurs in the matrix (a true kernel direction) over one the linear system never mentions.

pub fn decision_vars(&self) -> Vec<usize>

The variables CDCL should branch on under DPLL(XOR): every NON-pivot variable. The pivots are determined by Gaussian propagation (the theory forces them), so the search only ranges over the kernel free variables (plus any variables the linear system never mentions).

pub fn derived_clauses(&self, max_width: usize) -> Vec<Vec<Lit>>

The short implied clauses the Gaussian reduction derives — every reduced row of width 1..=max_width re-expressed as its CNF gadget. These are no-goods the linear system entails but resolution would not find (e.g. the 244 derived units of par32-1); injecting them into the CNF shares the XOR strategy’s discovered structure with CDCL. Sound: each reduced row is a GF(2) sum of implied equations, so its gadget clauses are implied by the formula.

pub fn rank(&self) -> usize

The number of pivots (= rank of the system under the current assignment).

pub fn kernel_dim(&self) -> usize

Free/kernel variables that occur in the matrix — the dimension of the choice space (each is a candidate break point).

pub fn state(&mut self) -> Result<Vec<(Lit, Vec<Lit>)>, Vec<Lit>>

The current forced literals (with implied unit reasons), or Err(conflict clause). Reads only the low-weight queue — the rows that became units/conflicts since the last call — and keeps the still-low ones for next time, so a propagation round is O(touched rows), not O(all rows).

Trait Implementations

impl Theory for IncXor

The fast path: IncXor syncs its incremental matrix to the solver’s trail each call — undoing the divergent suffix (backtrack) and applying the new literals (forward) — then returns the first XOR-forced unit clause or a conflict. O(work-per-assignment), not O(system-per-fixpoint).

fn propagate(&mut self, trail: &[Lit]) -> Vec<Vec<Lit>>

Given the solver’s current trail (assigned literals in assignment order), return a clause that is theory-entailed and currently unit or falsified (so the core will propagate or conflict on it), or None at a theory fixpoint. The trail is passed in order — and shrinks on backtrack — so an incremental theory can sync forward/undo against it (LIFO). The returned clauses MUST each be a sound consequence of the theory. Returning the whole batch of forced clauses at once (rather than one per call) lets an incremental theory amortise its work over one pass instead of rescanning per implication. An empty vec means “theory fixpoint”.