Translate each DNF disjunct (a conjunction of literals) into a stand-alone [`ConstraintSystem`]. Each disjunct clones the query-level builder (inherit

Number of literals on the trail.

F4-lite default toggle. Reads [`crate::config::RuntimeConfig::use_f4`]. Used by all default `BuchbergerConfig` construction sites so the F4 path is co

Empty (zero) constraint block.

In-flight timers (id -> (label, start_instant)). Used so a SIGTERM dump can include time spent in calls that haven't returned yet.

── arithmetic (operands coerced to a common arm) ───────────────

Default split-admission predicate. `admit(i, p) = deg(p) <= 1 && (i == 0 || numTerms(p) <= 2)` - basis 0 (linear): admits `p` iff `deg(p) <= 1`.

Wire layout: 1=xout, 2=yout, 3=x1, 4=y1, 5=x2, 6=y2, 7=β, 8=γ, 9=δ, 10=τ.

Synthetic basis2 trap: GF(11) with 4 bits, where `2^4 = 16 > 11` admits two distinct bit decompositions of the same target.

Builds `k` bit constraints `b_i·(b_i − 1) = 0` plus one equality `s − (b_0 + 2·b_1 + ... + 2^{k-1}·b_{k-1}) = 0` over GF(`prime`). Returns the system

Construct the polynomial `b_0 + 2*b_1 + ... + 2^k*b_k` for a bitsum.

Build the linear polynomial `sum_i coeff_i * var_i` for one R1CS constraint block. Inputs use the original `x_i` index in both copies (they share the

Returns a safe `Vec::with_capacity` hint: `min(claimed, data_len)`, further capped at [`ABSOLUTE_COUNT_CAP`]. Adversarial headers claiming 4 G constra

Sort of an `=` / `distinct` chain, checked for consistency. SMT-LIB requires every operand to share one sort; classifying by the first argument alone

Check uniqueness on a pre-parsed R1csFile. Useful when you want to inspect the R1CS structure before running the analysis, or when running multiple a

Classify whether candidate `p` (with precomputed `p_hash`) should be queued as a new generator of partition `j`, updating `contains_memo`. The memo r

Slice view of the coefficient vector after trimming. Exposed for tests and diagnostic comparisons.

Compute a Groebner basis with optional timeout. Phase 1: DegRevLex GB (faster ordering for reduction). Phase 2: Lex GB from Phase 1 output (needed fo

Full bench corpus as `(family, label, source)` triples.

Curve25519 base field prime (2^255 - 19).

Dehomogenize a polynomial in `Ph` back to `P` by setting `h := 1`. Implementation: walks `terms(q)` and rebuilds with the leading `n` exponents, drop

Upper-bound estimate of `self.to_dnf().len()`, computed without materializing the DNF. Saturates at `cap` (returned as `cap`). `True` evaluates to 1,

In-place sparse row echelon reduction over GF(p), tracking provenance. `rows` and `provs` are parallel; `provs[i]` accumulates the inputs whose contr

Like [`encode`], but passes `emit_rabinowitsch = false` to `encode_impl` so no Rabinowitsch witnesses are emitted for disequalities.

Independent math reference: evaluate an `equality` (list of `PolyTerm`) at a `BigUint`-indexed assignment, modulo `p`. The caller is responsible for s

Evaluate `p` at the given point (length = n_vars). Returns the field element.

Cancel-aware FGLM: same as [`fglm_to_lex`] but bails out with `None` when `cancel` fires mid-walk (large staircases on big primes can otherwise run fo

Modular inverse of `coeff` in GF(`prime`) via Fermat's little theorem (`coeff^(prime-2) mod prime`). Returns `None` when no inverse is computable by t

`{x^2 - x, x*y - 1}` over GF(7): non-homogeneous, so by-homog takes a genuinely different intermediate path from direct.

Build a `PartialBuild` over the given ring, with control over the inflight bases (seeded via `add_generators`) and the pending generator lists, so the

Seed `ctx.ranges` with the values forced by the IR's structural pins (wire 0 = 1). Called once by the DPVL driver before the propagation loop starts.

Intern the negation of this atom's polynomial into `builder`. Used by `ff_theory` to assemble the Rabinowitsch trick body `d - lhs = 0`, where `-lhs`

Heuristic Bool-context detector: does the expression `s` produce a Bool value (rather than an FF term)? Used to dispatch `=` to iff vs. FF equality, a

Check if a GB is trivial (ideal = whole ring).

Get the leading coefficient of a polynomial in a given monomial order.

`x + 3 = 0` over GF(7); SAT (x = 4). One equality, no diseq.

`i`-th element of the Luby sequence (1-indexed): `1, 1, 2, 1, 1, 2, 4, 1, 1, 2, 1, 1, 2, 4, 8, …`.

Match `c0 * target + sum_i c_i * bit_i = 0`, where `c0` is ±1 (mod p) and the remaining coefficients (after sign normalisation) are a power-of-2 seque

Iteration cap for the split-GB propagation fixpoint as a function of the partition count `k`. A safety bound against pathological propagation loops on

Create a finite field sort of the given size (modulus) in the given base.

Build a monolithic ideal (single basis containing every original generator). Used as the spec oracle in differential tests against split-GB.

Fetch the value following the flag at position `i`, or exit with a usage error if it is missing (e.g. the flag was the final argument).

Number of terms in a polynomial.

Called immediately before [`on_initial_basis`] to report the indices of basis elements that were potentially used as reducers when the new generator w

Parse `(define-fun name ((p1 T1) ...) ret_T body)` into a `MacroDef`.

Match an equality literal of the form `x = const`. Returns `(var_idx, const_value)` on match; the index is in the input literal's frame.

Convert a PartialPoint to a compact map keyed by variable.

`poly_terms_idx` collected into the `Vec<PolyTerm>` form that `Literal` / `add_equality` consume (zero-coeff terms dropped).

`dim_k(S/I)` for the monomial ideal generated by `gens` — the number of standard monomials, i.e. the `k`-vector-space dimension of `S/I`. For `gens =

Monolithic-GB radical Safe fast-path (config `radical_membership`). `gens` is the full query system: constraint generators, bitsum definitions, and t

Build a random polynomial: `n_terms` terms, each a product of up to `max_degree` (randomly-chosen) indeterminates, with a random coefficient. Retries

Like [`Self::reduce_by_refs_counted_cancel`] but reuses the caller's precomputed leading-term DivMasks (`div_dms[i]` for `divisors[i]`), skipping the

Like [`Self::reduce_by_refs_counted`] but reuses the caller's precomputed leading-term DivMasks. Result-identical.

Reduce `s_poly` against the current active basis, returning the normal form, the active-basis index list used (reduction order), and the per-divisor u

Equivalent of cvc5's disjunctive-bit preprocessing pass. Rewrites every `(or (= x 0) (= x 1))` subformula to the polynomial equality `x * x = x` (a si

Drain the in-progress S-pair queue without adding new generators. Used by [`crate::incremental_context::IncrementalSolverContext`] to resume a previou

A third sample in 3 vars: x0 + x1 + x2

Seed the engine with a polynomial set that is already a reduced GB in the engine's order. Skips S-pair generation among these inputs entirely — the ca

Seed the cross-iteration containment memo with self-membership: every polynomial already in partition `j`'s basis trivially satisfies `contains(p, j)`

Pick the next signal from the unknown pool to send to the solver. Returns `None` when the pool is empty.

Swap in a fresh cancel token. Each [`crate::incremental_context::IncrementalSolverContext::solve`] invocation produces its own per-call cancel token;

Squarefree part: `f / gcd(f, f')`.

Like `sub_scaled` but skips the divisor's leading term — used during reduction where the LT contribution exactly cancels the polynomial's already-popp