Minimal R1CS with a single trivial constraint, used to obtain a valid PolyIR with the requested wire count and prime so we can test the companion reco

Reuse-friendly samples: a Gröbner-basis-shaped (unique-LT-divides) set.

Unwrap a vector of solve-core `Poly` to the dense `DensePoly` the Gröbner engine consumes. On the dense path every element is already the `Dense` arm;

Build a fresh `RangeValue::Values` containing the given small values.

GF(7) ABOZ-shape system mirroring the prose: sel*y0 = 0, sel*y1 = 0, (y0 + sel + c_extra + y1)*1 = 0 Wires: 0 = one, 1 = y0 (output), 2 = sel (input

Detect bitsums in a polynomial. Given `p`, look for a sub-sum of the form `coeff * (b_0 + 2*b_1 + ... + 2^k * b_k)` where the `b_i` are distinct lin

Current decision level (0 = root).

Drive `cdclt_loop` over a hand-built SAT instance with `th`. Mirrors `solve_formula`'s loop call so the loop's own branches are exercised without rout

Find all roots of a univariate polynomial over GF(p). `coeffs[i]` is the coefficient of x^i.

Map a signed integer into the field (negatives become `p - |v|`).

Build a linear polynomial `c · x_var` from a BigUint coefficient.

`var_name -> (value, source_atom)` from positive single-variable equalities on the trail.

Roll back to the most recent push. Polarities and witnesses asserted since are reverted; union-find structure is not (atom registration is monotonic a

Build the cache via the fast path ([`split_gb_cancel`]). On cancellation, save a `PartialBuild` so the next solve call with matching digest can resume

Helper: compute the reduced sparse GB.

Cancel-aware model search. Returns `Sat / Unsat / Unknown` on success; `Err(Cancelled)` on timeout.

Wrap dense engine output back into solve-core `Poly`.

Iterate every backend descriptor registered via `inventory`. Stable order by `(name, theory)` for reproducible dispatch.

Merge the `Some` fields of `o` onto `self`; `None` fields are left untouched. Enum-valued fields arrive as strings (matching the CLI and TOML surface)

Apply branching rule on a single basis. (1) if `gb` has a univariate polynomial in some unassigned variable, enumerate its roots over GF(p); (2) if `

Convert to `BigUint`. Allocates.

If this atom canonically pins one variable to a specific field constant (i.e. `a·x + c = 0` with `a ≠ 0` and `x` a single degree-1 variable), return `

Assemble a 3-section R1CS (types 1/2/3) from raw payloads.

Whether a `len`-bit unsigned bitsum embeds into GF(p) without mod-p aliasing: needs `2^len <= p`, so distinct bit patterns have distinct residues. Whe

Extract `(name, sort, inferred prime)` from a `declare-fun` / `declare-const` form: `name` is the declared symbol, `sort` its classified sort (`None`

Collect the modulus P from every `#fNmP` literal in `s` (recursively). Used by the pre-scan to infer the session prime when no FF sort declaration is

Like [`compute_gb_with_timeout`], but with UNSAT core tracing enabled. When the DegRevLex phase produces a trivial basis (UNSAT), the tracer is used

Resume a partial build. Re-attaches the new cancel token to all in-flight `IncrementalGB`s, runs the fixpoint loop. On completion, produces a `CachedB

Look up a backend by `(name, theory)`. Returns the factory's freshly-built instance, or `None` if no descriptor matches.

Independent polynomial evaluator: maps every (idx -> value) and returns `sum_i coeff_i * prod_j x_j^e_j (mod prime)`. Pure math — used as the referen

Introduce the witness pair for encoding `lhs != 0`: a fresh `__diseq_d_{seq}` variable `d` (the caller then constrains `d = lhs` via [`Self::add_equal

Returns `true` iff `R/I` is a finite-dimensional `K`-vector space.

Build a Lit::Eq for `coeff * <var_idx> == rhs_const`.

Create a named constant (free variable) of the given sort.

Push negations to the leaves (negation-normal form). Negated literals flip `Eq`↔`Neq`.

Backtrack to level 0 and bump the next Luby restart threshold. Callers in CDCL(T) must also pop any theory-level state down to match the new decision

Index-keyed term constructor for tests. `idx_vars` is a list of `(VarIdx, exp)` pairs.

Build an R1CS over GF(`p`) with `n_wires` total wires, the given constraints, and the listed `inputs` (must include wire 0).

Non-cancel-aware version of [`Self::reduce_by_refs_counted_cancel`].

Reference multivariate division: keep the partially-reduced polynomial in one descending-sorted vector, cancelling the leading term against the first

Polynomial ring builder for prime `p` and `n_vars` variables.

Multiply polynomial by a scalar.

Seed the Buchberger state with polynomials that are already a reduced GB under [`Self.ring`]'s monomial order. Bypasses S-pair generation: an already-

Spec of ideal-membership: each input generator reduces to zero modulo any GB of the ideal it generates (Buchberger).

Register that the SAT variable `var` belongs to the prime at `slot_idx`. A [`Theory::notify_fact`] for a `var` without prior registration trips the `d

Buchberger B-criterion. Walks `pairs` (the currently-pending S-pair queue) and erases every pair that the newly-added basis element's leading term `ne

Build an R1CS encoding `(b0 + 2 b1 + ... + 2^{k-1} b_{k-1}) * 1 = target` together with `b_i (b_i - 1) = 0` for every bit. Wire 0 is the one-wire; bi

Create the appropriate solver backend for a solver+theory combination. Returns `None` for `SolverKind::None` (propagation-only mode). Dispatch is via

Build a polynomial holding a single term `coeff * monomial`.

Find all roots of `poly` in GF(p). Returns an empty vector if `poly` is the zero polynomial (every element is a root, which is not a useful answer; ca

Try to find a common zero of the polynomials that generated `initial_gb`. At each branch `x - val` is added to the generators and the GB is recompute

Incrementally extend a reduced Gröbner basis `known_gb` with `new_gens`: seed the engine with `known_gb` (pair-free) and run Buchberger only on the cr

Header payload with prime 7 and the given wire/IO counts.

Add a learnt clause and enqueue its asserting literal (`lits[0]`). Assumes the solver has already backtracked to the asserting level (i.e. all literal

Value of a literal under the current assignment.

Parse an SMT-LIB v2 query with one or more `(_ FiniteField p)` sorts. Returns a `Vec<BooleanQuery>` with one entry per declared prime, in ascending p

Iterate every term of `poly` as `(coeff, monomial_vars)`, where `monomial_vars` is a flat `Vec<String>` listing each variable's canonical name once pe