Trait Theory 

pub trait Theory {
    // Required method
    fn propagate(&mut self, trail: &[Lit]) -> Vec<Vec<Lit>>;
}

A theory propagator (the DPLL(T) seam). The SAT core calls Theory::propagate at each fixpoint of Boolean propagation; a theory returns a fresh clause to add (an explanation/conflict) or None if it has nothing to say. AllDifferent GAC, EUF, and LIA all implement this without the core knowing the theory.

Required Methods

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

Implementors

impl Theory for SymmetryTheory

impl Theory for CardinalityTheory

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

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.