Run DPVL on a parsed R1CS file.

Assert a polynomial equation `sum(terms) == 0`.

Cancel assignments down to (but not including) `level + 1`, so the next decision will be at level `level + 1`. `qhead` is reset to the current trail l

Pick test values for a large prime: 0, 1, several small constants, and `p - 1`. Constants chosen independently of the field's behaviour.

Record the outcome of a solver call on `signal`.

Modular exponentiation by a `u64` exponent.

Two-tier propagation; reasons cached in `pending_reasons` for `explain()`. See [`compute_tier1`] and [`compute_tier2`].

Geobucket-based reduction: the shared implementation every `reduce_by_refs[_cancel|_counted|…]` wrapper forwards to (each selecting a different `(canc

Evaluate a slice of `BigUint` values (interpreted modulo the ring's prime) as a `FieldElem` vector of length `n_vars`. Indices past the supplied slice

Assert `var = value`.

Whether `self` divides `other` in the module — same index and `self.monom` divides `other.monom`. Used to test whether `other` is a multiple of a reco

Return `true` if this is a null (empty) command.

Build a `Poly` representing the linear polynomial `coeff * x` for variable index `var`. Used by lemmas that need to emit a learned constraint from a `

Build a `PolyIR` with `n_wires` wires and an explicit `equalities` list built via the supplied closure.

Modular exponentiation `a^exp mod p`.

Try to extend `cur_r` into a complete zero of the ideal whose generators are `orig_polys`.

Map a ring variable index back to its underlying wire index. `x_i` (index `i`) and `y_i` (index `n_wires + i`) both refer to the same wire `i` from a

All registered lemma names, sorted. Used by `LemmaSet::parse` to validate `--lemmas` flags against the live registry.

Assert a formula to the solver.

Request cancellation.

Hash an [`ConstraintSystem`]'s constraint side (everything except `disequalities`) into a 128-bit cache key. Self-consistent: two systems agreeing on

Gebauer-Möller M-criterion insertion. A pair with a smaller `lcm` dominates pairs with larger `lcm`s: `lcm(LT_a, LT_b)` dividing `lcm(LT_c, LT_d)` ma

Workspace-threaded variant of [`process_batch`]. Caches the reducer-row computation across calls in `workspace.reducer_cache`; output matches [`proces

Random terms shared by both representations, so dense and sparse are built from identical input and can be compared directly.

Large-prime ring helper (BN254 needs a string-parsed prime).

Lower this `PolyIR` to a [`ConstraintSystem`] via the `ConstraintSystemBuilder`. Variable names are interned in `ring.var_names()` order so builder in

Add a clause from the input formula. Returns `false` if the formula is trivially UNSAT at the root level (an empty clause was added, or unit propagati

Add a polynomial. Amortized O(L * log(N/L)) where L = len(p), N = total size.

Mutual ideal-membership assertion: every element of `a` reduces to 0 mod `b` and vice versa. SPEC: bidirectional ideal-membership is the defining prop

Solve the current fact set. Encodes from scratch and dispatches to the Split GB engine.

Degree of the polynomial; `None` for the zero polynomial.

Convert the (reduced) Gröbner basis held by `ideal` to a reduced Lex Gröbner basis via FGLM. Returns `None` if the ideal is not zero-dimensional (the

Consolidate every bucket into a single canonical `DensePoly`.

Pop the leading term across all buckets. Cancellations are resolved here: if multiple buckets share the leading monomial, their coefficients are summe

Watched-literal unit propagation. Returns `Some(conflict)` for the first clause whose literals are all False under the current assignment, or `None` w

Like `reduce_by` but takes references to divisors — avoids cloning the divisor list when the caller already holds polynomials inside some larger conta

Register `(var, atom_key)`. If another registered atom has the same canonical poly, `var` is unioned into that atom's class. Returns [`RegisterOutcome

Build a per-call `ff::PolyRing` whose monomial order matches `order`. Cheap (an `Arc<PolyRing>` with the same field/var-name data).

Polynomial ring builder for a given prime + variable count.

A second sample in 3 vars: x0*x2 + 4*x1 - 1

DNF-enumeration path: try each DNF disjunct in order through the GB solver. Returns `Sat` on the first SAT disjunct, `Unsat` only if every disjunct is

Solve an `EncodedSystem` directly. Convenience wrapper.

Solve an `EncodedSystem` with cooperative timeout. Returns `SolveOutcome::Unknown` if the cancel token fires.

1-UIP conflict analysis. Returns `(learnt, bt_level)` where `learnt[0]` is the asserting literal (negated 1-UIP), `learnt[1..]` are lower-level litera

Constant polynomial from a field element.

Helper: compute the reduced dense GB via the per-pair path; lift back to sparse.

`coeff * <var idx> = rhs_const`.

Substitute the partial assignment into a polynomial and evaluate it. Returns `Some(value)` if all variables in `p` are assigned (so it can be fully ev

Looks for `c·b_0 + 2c·b_1 + ... + 2^(k-1)·c·b_{k-1}` where each `b_i` is a known bit (degree 1 in a single index, coefficient `(2^i · base) mod p`). S

Resolve a GB `Result` into a basis under the soundness contract shared by every public GB entry point: on **cancellation** return `backup` (the caller

Create a finite field element from a string value in the given base.

Normalize an `PolyTerm` list in place. Each term's `vars: Vec<(VarIdx, u16)>` is sorted by index and entries with the same index are merged by adding

Parse `ffN`, `ff-N`, `#fNmP`, or `#f-NmP` constant. Negative forms return `(p - N) mod p`. Returns `None` for non-constant symbols.