The prime field, read from the shared ring context.

Intern a variable name, returning its index. Repeated calls with the same name return the same index.

Save a checkpoint. Subsequent `pop` returns to this state.

Polynomial multiplication: returns `self * other`. Per-pair `i64::saturating_mul` followed by per-cell `i64::saturating_add`.

Build a `Poly` representing the constant `c`.

The constant polynomial `1`.

Save a checkpoint for backtracking. Clones the surviving basis elements (with their polynomial bodies) and the open S-pair queue, so cost is O(sum of

Number of divisors the index was built over.

i-th indeterminate as a polynomial.

Construct a [`PolyIR`] from a parsed R1CS file in a single pass over the constraint blocks: each `A * B = C` constraint becomes one polynomial equalit

Raw pointer for read-only access.

Multiply the signature's monomial by `m` (the S-poly cofactor).

Solve a `Formula` over GF(`prime`) via CDCL(T) with the FF theory. `var_names` is the producing builder's variable frame (used by the SAT-side atom ta

Get the sort of this term.

Register a known bitsum (variable indices, lowest bit first).

The zero polynomial.

Atom variable for `(= var const)` over the given table + SAT.

Encode a [`ConstraintSystem`] into polynomials. Pre-encode pipeline: 1. `compact_used_vars`: drop variables from `var_names` that no equality / diseq

Parse an SMT-LIB v2 QF_FF source with full Boolean structure.

Ideal membership: returns `true` iff `p ∈ I`.

Allocate a fresh propositional variable.

Returns (cdclt_verdict, dnf_verdict). Asserts both paths return the same verdict; panics with a diagnostic if they disagree.

Parse and evaluate every top-level S-expression in `src`, returning the outputs of every non-silent command in order. Processing stops as soon as `(ex

Compute a split GB from scratch. `generator_sets[i]` is the initial generator set for partition `i`. On cancel, falls back to an empty split GB (one

Run CDCL to completion. Returns `Sat` once every variable has a value, `Unsat` on a root-level conflict, or `Unknown` if an external limit (none defin

Parse an SMT-LIB v2 QF_FF source and produce a [`ConstraintSystem`]. Threads a single `ConstraintSystemBuilder` through `build_poly` so each variable

Mark `var` as bit-constrained.

Compare under the ring order: index-major (a higher module index dominates), then the monomial order on the multiplier.

Inter-reduce a basis into the canonical reduced Gröbner basis: drop zeros, collapse to `{1}` if the ideal is the whole ring, make every element monic,

Build a small set of representative field elements covering 0, 1, the multiplicative generator-region (small ints), and `p - 1` (== -1 mod p). Pure: n

Build a fresh PolyIR with `n_wires` wires under prime `p`, then drop the equalities so callers can inject exactly the polys they want to test. Wire-0

Save a checkpoint matching a SAT push.

Encode `(orig_polys, bitsums)` into a split GB, run the propagation fixpoint, then [`split_zero_extend`] to extract a model.

Derive new equalities (as polynomials whose `=0` form is asserted) from the structure of the bitsums and the current GB. See cvc5's `BitProp::getBitE

Construct a single-name-keyed term list `coeff * x` for var index 0 (the test's only variable). `vars = &[]` yields a constant term.

Every registered lemma enabled.

Intern an equality atom and return the SAT variable that represents it. Repeated calls with equivalent canonical polynomials return the same variable.

GF(7) prime.

Read a snapshot of the current thread's config.

A Gröbner basis of the ideal generated by `gens` (Buchberger with the product / Gebauer-Möller M / B criteria and sugar selection). The result is a —

Look up the canonical atom for a SAT variable. Returns `None` for auxiliary variables (Tseitin or other) and out-of-range indices.