`coeff * prod(vars)` as a `PolyTerm`, collapsing repeated name occurrences into `(VarIdx, exp)` pairs.

SMT-LIB-compatible textual form. `Silent` returns an empty string; other variants emit one or more lines matching the expected response shape.

Run the existing depth-first triangular search on a freshly-computed Lex Gröbner basis. The Lex order makes every internal node univariate in the smal

Triangular model construction for a zero-dimensional ideal (cvc5 `multi_roots` style): solve variable-by-variable using univariate roots of the substi

Canonical name for the original-copy variable of wire `wire` (e.g. `x5`).

Canonical name for the alt-copy variable of wire `wire` (e.g. `y5`).

Synthetic ABOZ trap: with `sel = 0` the bilinear products vanish and the linear sum admits multiple `(y0, y1)` pairs.

Reduce each generator by the current basis, then integrate it: drop zeros, collapse to the trivial ideal on a constant, otherwise generate its S-pairs

Observed variant of [`Self::add_generators`]: the supplied observer receives `on_initial_basis` / `on_new_poly` / `on_inter_reduce` callbacks during t

Add a descending-sorted, nonzero-coefficient term list, cascading merges up through the buckets on overflow.

Index of the `y_i` variable in the underlying ring.

Reorder a Brancher::Roots so the saved phase for a variable (if any) is moved to the back of the Vec, so Vec::pop tries it first.

Assert `a != b`.

Stronger: every FGLM output element must lie in the SOURCE DRL ideal. This catches a class of bug where FGLM emits a polynomial that happens to equal

Mutual ideal-membership: ideals generated by `a_basis` and `b_basis` are equal. Each basis is RE-COMPUTED as a DRL GB (the ring's stored order) before

SPEC: if 1 ∈ I, both engines must produce {1} as the reduced GB.

Build a polynomial of the form `x_var - val`.

Total number of basis elements tracked (initial + derived).

k-bit bitsum pin: `b_0 + 2·b_1 + ... = v`.

Build output model from assignment.

Index every "part-shaped" equality (exactly one degree-2 monomial over two distinct variables, no higher degree, no square) by the canonical pair of i

Build the S-polynomial of `pair`: `(lcm/LT_i)·f_i − (lc_i/lc_j)·(lcm/LT_j)·f_j`, scaled so the two leading terms cancel.

`(xor b_1 ... b_n)`: True iff an odd number of the `b_i` are True. Built as a left-associative chain of binary `xor`.

Canonical reduced-GB fingerprint: interreduce (→ monic reduced GB, which is unique for a fixed order) then sort the per-polynomial hashes.

Cantor–Zassenhaus for the squarefree polynomial `poly`. Returns its irreducible factors (over GF(p), restricted to those involved in the linear part —

Check uniqueness of output signals in an R1CS circuit from a file path. This is the main entry point for programmatic use. It reads the R1CS file, co

Build a ConstraintSystem from a `(atom, polarity)` fact trail against `atoms`, encode, dispatch to the GB solver, and map any returned UNSAT core back

Solve with a timeout duration.

Classify a sort s-expression as `Ff`, `Bool`, or unknown.

Clone a monomial. Accepts either `&Monomial` or `Monomial`.

Coefficient of `t^d`. Returns `0` for any `d` past the trailing nonzero term.

Wire indices `(a, b)` for every equality of the form `c * x_a * x_b = 0`. Skips constraints that have any other terms beyond the single bilinear monom

Compact `system.var_names` to only the variables actually referenced by some equality, disequality, assignment, or bitsum. Returns a new `ConstraintSy

Free-function port of `FfTheory::compute_tier1`.

Free-function port of `FfTheory::compute_tier2`.

Lower one R1CS constraint `A * B = C` into a polynomial equality `expand(A) * expand(B) - expand(C) = 0` in the given copy. Returns `Ok(None)` when th

Cancel-aware membership test. On cancel returns the value computed from a partial reduction, which may falsely report "not in I" if cancellation inter

`cyclic-N`: the N-variable cyclic ideal. Classical GB benchmark known to produce many same-sugar batches and a large basis.

Decide a fresh literal: open a new decision level and enqueue `lit` as a decision (no reason). Returns `false` when the literal is already assigned to

Convert a DegRevLex Gröbner basis to a Lex GB for model extraction. Uses FGLM order conversion ([`crate::gb::fglm`]) when the ideal is zero-dimension

Hand-built differential bank. Each closure returns a generator list spec'd by mathematical structure — never read back from engine output. Property: F

Compute (or return the cached) DNF expansion of `self.formula`. May allocate `O(3^k)` literal containers for k-CNF inputs.

Write the accumulated split-GB / DFS counters to stderr (if `engine.gb_stats_enabled` was set during a previous `check_r1cs` call).

Write the accumulated per-site wall-clock profile to stderr (if `engine.profile_enabled` was set during a previous `check_r1cs` call). `tag` is a free

Convenience: echelonize without provenance tracking.

Push the zero-product disjunction `(var_s = 0) ∨ (var_o = 0)` for both the original and alt copies, deduplicating on `(s, o)` so fixed-point re-runs d

Ensure the union-find has a slot for `v`. Returns its initial rep (itself).

Brute-force enumeration of standard monomials of the monomial ideal `gens`: any exponent vector with total degree ≤ `max_deg` that is NOT divisible by

Evaluate a single command. Returns `Silent` for `(exit)`; script-termination on `(exit)` is enforced by [`SmtSession::eval_script`] rather than this m

Helper: evaluate a polynomial at a point. Local copy so we don't pollute the public API. Identical math to `split_gb::tests::eval_poly`.

Resolve a macro call by alpha-substituting arguments into the body.

The set of `(name, theory)` backends expected under the current feature configuration. Always includes `(native, Ff)`; cvc5 and z3 entries are gated b

Extend an existing ideal by adding new generators incrementally. Reuses the existing reduced GB and runs incremental Buchberger seeded with the exist

Traced variant of `extend_with_cancel`. Feeds Buchberger observer events to the supplied `tracer`, which must be sized for at least `self.basis.len()

Like [`find_roots`], but also reports whether root finding was complete**. Returns `(roots, complete)`: `complete == true` — every root of `poly` in

Find the signal `S` defined by `S = Σ part_outs` (each part output appears with one shared coefficient `−k`, `S` with `+k`, no other terms). Returns t

Find the index of a nonzero constant in the basis, if any.

Now extract the formula's literal `Eq` polynomial pair and semantically compare under every x value.

First polynomial index in `encoded` whose provenance is an `Equality(_)`.

`true` iff a theory-conflict resolution bailed out (see [`Self::give_up`]). Callers must treat this as Unknown, not UNSAT.

Returns the ring slot for `name`, claiming a new slot if it is the first appearance. If `add_field_polys` is set, pushes the field polynomial `x^p − x

Get the value of a term in the current model.

Sift element at index `i` down while a child has higher activity.

Homogenize a *lifted* polynomial in `Ph` (where the `h` exponent is currently 0 in every term) by raising it to its top total degree. For every term

Single-variable monomial of degree 1.

Get the Integer sort.

Push a new (already monic, non-constant) polynomial into the basis: generate its pairs against the active basis first (so pairs against soon-to-be-dea

The active basis (a Gröbner basis, not yet inter-reduced), or `{1}` when the ideal is the whole ring.

Lower the GF(7) system, target wire 2, and inject a benign always-true disjunction `(x0 = 1) ∨ (x2 = 5)`. Wire 0 is pinned to 1, so the clause holds u

Test whether `var` is bit-constrained: either it is a globally asserted bit (`self.bits`, populated from user `x*(x-1)=0` constraints) or some basis i

Whether exhausting this brancher constitutes a proof that no extension exists. `Roots` is always exhaustive (we computed every root over F_p); `Round