Number of indeterminates.

Canonical lowercase name. Matches the `name` field on the backend's `inventory::submit!`'d [`backends::SolverBackendDescriptor`] (except `None`, which

Iterator over the terms of `p` in descending order, yielding `(coefficient, monomial)` pairs. The monomial is freshly cloned per term (cheap; a small

Compute a Groebner basis of `generators` from scratch.

Returns `true` iff `I = R` (i.e. `1 ∈ I`).

Parse a `--lemmas` spec. Formats: - `all` — enable every registered lemma - `none` — disable every registered lemma - `all-X,Y` — all except `X` and

A standard sample polynomial in 3 vars used across property tests: 2*x0^2*x1 + 3*x1*x2 + 5*x0 + 7

Build a sparse polynomial from `(exponents, coeff_u64)` triples.

Sum a list of polys into one.

Assert CDCL(T) and DNF agree, skipping when DNF gave up at the size cap.

Reference to the underlying `ff::PolyRing` context.

Access the underlying `(var_index, max_degree)` pair at position `i`. Used by callers that index `appearing[0]` directly (e.g. univariate-detection pa

`metric::*!` take the typed counter path and lower to a gated direct atomic update. Per-test gating is the thread-local gb_stats flag; each test uses

Build a `ParseCtx` with the given prime, declared vars, and macros.

Rewrite equalities to extract bitsum subpatterns into `ConstraintSystem::bitsums`. Operates on [`PolyTerm`] lists: `bits: HashSet<VarIdx>`, chain exte

Create a term with the given kind and children.

Exponent of variable `var` in monomial `m`. Accepts both `&Monomial` and `Monomial` so callers iterating over [`Self::terms`], which yields owned `Mon

Read an R1CS binary file from a byte slice.

Solve a system of polynomial constraints using the Split GB algorithm. `original_polys` is the full list of input polynomial generators (in the same

Materialise a dense polynomial with the same terms.

Variables that actually appear in `p` (delegates to the inner [`PolyRingFacade`]). Exposed here so the IR ring — which is just an `FfPolyRing` — offer

View as the dense arm, materialising the sparse arm if needed. For the rare dense-flavoured readers.

Build a `ParseCtx` with declared FF variables `xs` under `prime`, then build the polynomial for the given source fragment. Returns the polynomial plus

Build a small PolyIR over GF(p) with `n_wires` wires, no constraints, the inputs from `inputs`, and a target signal. Convenient for unit tests of acce

`true` when the index is empty.

Build a minimal in-memory R1csFile with the supplied prime, n_wires, inputs, and constraints (each as triples of (a, b, c) blocks).

Iterate every term of `poly` as `(coeff, vars_with_exp)` where `vars_with_exp` lists the variables that actually appear in this monomial together with

Take the current accumulated profile, clearing the table. Returns rows sorted by total time descending.

Iterate terms in descending order.

Adds `x != 0` to `lin_eq_sys`; still SAT (x = 4 ≠ 0).

Snapshot the logical state into an owned form (for caching).

Build an FF polynomial recursively. Threads `ctx.builder` so every FF-typed leaf reference goes through `builder.var(name)`, producing index-keyed `Ve

Compare under the given ordering.

Atom variable for arbitrary `(= sum_lhs sum_rhs)` from `&[(coeff, &[var_names])]` term specs.

Multiplicative inverse. Returns `None` if `a` is zero.

Multiply by a single (monomial, coefficient) term. Result preserves sorted order.

Process one F4 batch. Returns the new basis generators produced by the batch (already monic, not inter-reduced — integration is the caller's responsib

Build a ring over GF(prime) with `n_vars` variables x0..x_{n-1} in DegRevLex order. Mirrors the file-local `ring(n)` helper but parameterises the prim

Apply Tseitin to `formula`, registering atoms in `atoms` and emitting clauses into `sat`. `var_names` is the producing builder's variable frame, used

Leading coefficient (None for the zero polynomial).

Number of variables interned so far.

Discard all facts added since the most recent `push`. No-op if no checkpoint exists.

The `idx`-th `(monomial, coeff)` term in descending ring order, or `None` past the end. Lets a positional iterator walk the terms without exposing the

Variable-name frame interned so far. Used by callers like `BooleanQuery` to feed the SAT-side `AtomTable` for reverse-resolving `PolyTerm` indices to

Add `other` into `self` in place. Per-coefficient `i64::saturating_add` clamps to `i64::{MIN, MAX}` on overflow.

Canonical-variable map: union-find over pure two-term linear identities `c1·x_i + c2·x_j = 0` with `c1 + c2 ≡ 0` (i.e. `x_i = x_j`). `canon[v]` is the

Build a fresh solver, add `n_vars` propositional vars, then add all `clauses`. Returns the solver and the var vector. None of the clauses may triviall

Inter-reduce a basis (make every element's tail reduced w.r.t. all others; make monic).

Peek at the leading term. Implemented on top of `pop_leading_term` — resolves any pending cancellations, then re-inserts the surviving term.