Struct XorEngine 

pub struct XorEngine { /* private fields */ }

A GF(2) constraint system with Gaussian reasoning under a partial assignment.

Implementations

impl XorEngine

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

Build the engine from recovered XOR equations over num_vars variables. Equations with a variable out of range are dropped (defensive; callers pass in-range systems).

pub fn is_active(&self) -> bool

Is this system non-trivial enough to be worth running (≥1 equation)?

pub fn analyze(&self, assign: &[Option<bool>]) -> XorStep

The core query: under partial assignment assign (None = unassigned), return the first XOR-forced literal or a conflict, each with an implied, correctly-shaped clause. Complete — it finds every linear consequence, not just per-equation ones — via Gaussian elimination over the unassigned variables with provenance tracking.

pub fn all_consequences( &self, assign: &[Option<bool>], ) -> Result<Vec<(Lit, Vec<Lit>)>, Vec<Lit>>

Every XOR-forced literal under assign (with implied unit reasons), or Err(conflict clause) if the system is contradicted. This is the complete, oracle-checkable consequence set.

Trait Implementations

impl Theory for XorEngine

DPLL(XOR): the engine plugs into CDCL’s theory hook. At each Boolean fixpoint it hands back the first XOR-forced unit clause, or a conflict clause, or nothing — every clause implied by the formula, so the solver stays sound while gaining Gaussian reasoning resolution cannot do.

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”.