── reduction (normal form modulo divisors) ─────────────────────

Mutable borrow of a slot's atom table for atom interning by the caller.

Expand to disjunctive normal form. Caller must call [`nnf`] first. The result is `Vec<Vec<Literal>>` where the outer list is the disjuncts and each in

Convert to the sparse representation (boundary helper).

Coefficient vector (lowest degree first) of `p` viewed as a univariate polynomial in `var_idx`; `None` if any other variable appears. Shared by model

Per-wire connectivity score: the count of distinct constraints whose support touches the wire. Used by the counter-style signal selector to prefer wir

Record that wire `w` has been proved unique by the DPVL outer loop. Appends `x_w - y_w = 0` to [`Self::equalities`] so the next backend call sees it a

All lemmas discovered via the inventory registry, sorted by name so execution order is reproducible across runs.

── dense-flavoured readers (sparse arm materialises) ───────────

SPEC: FGLM output must generate the same ideal as direct Lex Buchberger of the same generators. Probe via mutual ideal-membership instead of canonical

Compute branching candidates using the same 3-case strategy as cvc5's `applyRule` (and the in-tree `split_gb::apply_rule`), extended with a Case 2.5 F

Construct a default PropagationCtx for `n_wires` wires with the given binary-set on `bit_wires` (mirroring what binary01 produces) and the given known

Assign `lit` to True with the given reason. Returns `false` when the assignment conflicts with the existing value of `lit.var()` (i.e. we are trying t

If `sort` is `(_ FiniteField <p>)`, return the prime literal `<p>` as a string; otherwise `None`. Centralises the shape detection repeated at every so

`x*y - 1 = 0` over GF(7) — non-homogeneous, so the Auto resolver would pick `ByHomog` and the two strategies take different intermediate paths (final

Tighten this range by intersecting with `new_vals`. A `Bottom` range adopts `new_vals` wholesale.

Coerce to the ring's configured arm (no-op when already correct). Used to reconcile a representation-neutral `zero()` with operands built over the rin

Deterministic LCG (no `rand` dependency; reproducible across runs).

Build a `PartialBuild` for a small constraint system and feed it to `continue_partial`. Mirrors what `rebuild_base` would save on cancellation, but co

Build a tiny PolyIR with a hand-crafted equality list. Uses `n_wires` wires (so the ring carries `2 * n_wires` variables). `equalities` is built by t

Move-based merge for cases where both inputs are owned. Recycles each input's `FieldElem` allocations into the output rather than cloning them, elimin

Populate a `BitProp` by scanning the encoded polynomials for bit constraints (`x*(x-1) = 0`) and bitsum patterns.

Reduce `p` modulo the ideal. Returns the *normal form* of `p`.

Single-vector reduction with fused `merge_sub_scaled_tail`. The cross-validation reference for the geobucket-based `reduce_by_refs`.

Resolve a registry index back to its matrix order. Panics in debug if the index was never interned on this thread.

Set the current uniqueness target. Updates `target_signal` and rebuilds `disequalities` to point at the new target's `(x, y)` pair. The constraint set

In-place tail-reduce all active basis elements. For each active element `i`, computes the normal form of `basis[i].poly` modulo all OTHER active elem

Current value of a variable.

Verify that an assignment satisfies all polynomials. The model must assign every variable appearing in `polys`. A variable missing from the model is

Tiny xorshift used to build deterministic random Boolean inputs.

Incrementally update `self = N(I)` to `N(I ∪ {new_gens})` using the Bigatti–Caboara–Robbiano recursion ```text N(I ∪ {g}) = N(I) − t^deg(g) · N(I : g

Accumulate `c · monomial(k)` into `m`, reduced mod `p`.

Merge an overlay (one config layer) onto this config; only the overlay's `Some` fields override. A bad enum string in the analysis layer surfaces as [

Single-term constraint block: `factor * x_wid`.

Build a synthetic R1CS over GF(7) encoding the trivial constraint `x_1 * x_1 = x_2` over 3 wires (wire 0 is the one-wire, wire 1 is the input, wire 2

Construct a builder pre-populated with the given var names.

Compute a Groebner basis without timeout.

Tier 2: a positive multi-var atom A on the trail reduces under `pinned` to `a·v + c = 0` (single unpinned linear var `v`, `a ≠ 0`). Solve `v = −c · a⁻

Non-strict deactivation: deactivate every active element in `0..upto` whose leading monomial is divisible by `lt`. Run after `generate_pairs_against`,

Eliminate the linear part of `polys` by Gaussian elimination and substitute the result into the nonlinear part. See the module docs.

Per-run profiling counters accumulated across every `add_generators` / `run_only` call. Pure telemetry — no field drives engine logic; counters only a

Decompose a polynomial into a list of linear monomials and a list of "rest" (constant + non-linear) terms (each rest term as a single-term polynomial)

Monic GCD of `self` and `other` (Euclidean algorithm).

Value of the graded Hilbert function `HF(S/I)(d)` in `n_vars` variables, where `self = N(t)` is the Hilbert numerator: the coefficient of `t^d` in `N(

Intern a matrix order, returning its registry index for use as `MonomialOrder::Matrix(idx)`.

`true` iff `v` is a Tseitin / orchestration auxiliary variable rather than an FF atom.

Has the formula been proved UNSAT at the root?

Lift a polynomial from `P` into `Ph` (φ). This is the embedding `x_i ↦ x_i`, leaving the `h` exponent at 0 in every term. Implementation: walks `ter

`x = 1` ∧ `x = 2` over GF(7); UNSAT.

Map a theory UNSAT core (polynomial indices into `encoded`) back to the trail atom variables responsible, via per-polynomial provenance. `Equality(j)

Match one CompConstant `parts_i` equality over the bit pair `(sl, sm)` (canonical low/high digit bits). On success returns the base-4 digit `c_i ∈ {0,

Merge `incoming` (sorted descending by [`CriterionPair::cmp_key`]) into `dst` (also sorted descending), preserving descending order. O(n + m).

Compute the minimal polynomial of `var_idx` in `R/I`.

Modular inverse of `a` mod `p` via the extended Euclidean algorithm, or `None` when `a` is not invertible (not coprime to `p`). Shared by the lemmas t

Multiply two `Vec<PolyTerm>` lists. For each cross-product `t_a * t_b`, merge exponents per variable via `BTreeMap` (so `x*x` stays as `(x_idx, 2)` ra

Length of the variable-indexed atom slot vector. Callers iterate `0..n_atom_slots()` and use `atom(Var(i))` to skip aux slots.

`x·y - 1 = 0` over GF(7) (nonlinear); SAT.