Compute `self^exp mod modulus` using square-and-multiply.

Read an R1CS binary file from a file path.

Reduce against a divisor set using a **prebuilt** [`ReducerIndex`] (the geobucket reducer's degree-order + DivMask-bucket lookup structure, owned so i

Cancel-aware reduce. On cancel returns whatever partial remainder the geobucket reducer had accumulated — sound (still represents the same residue cla

Replace the thread's config. The previous value is discarded; prefer [`ConfigGuard`] for scoped overrides.

Set the logic for this solver (e.g. , ).

Recursively format `s` back to SMT-LIB source. Used by `parse_boolean_multi` to rebuild per-prime subset queries.

Solve a [`BooleanQuery`]. Default path: CDCL(T) over the original formula via [`crate::cdclt::solve_formula`]. The DNF-enumeration path is retained a

If `s` matches `(! inner :named NAME [other :attr value ...])`, return `(inner, Some(NAME))`. The annotation may carry additional `:key value` pairs t

Subtract `neg_coeff * x^mul_exps * divisor` from the geobucket. Internally materializes the scaled polynomial then routes via `add_poly`.

A small nonlinear system over GF(7) whose Buchberger run does real work (S-pairs + reductions), built through the facade.

Symbolic preprocessing: given the S-polys, iteratively add reducer rows for every monomial divisible by some active basis LT. Returns: - The combined

Reference coefficient map: fold the raw terms (sum duplicates, drop zeros) mod PRIME.

Build a minimal R1CS with a single trivial `1 * 1 = 1` constraint over GF(`p`) with `n_wires` wires, the given `inputs` and `outputs`. Used as scaffol

Check if a solver+theory combination is valid.

Add a theory-supplied lemma clause. All literals must currently be False. Sorts by descending decision level, computes the assertion level (largest li

Turn an atom-core into a SAT lemma and apply it. On success returns `Some(trail_len_before_asserting)` (the position the lemma's asserting literal sit

FGLM-converted Lex GB must equal the directly-computed Lex GB (reduced GBs are unique up to ordering + monic normalisation).

Mutual-ideal-membership over Dense polys: every element of `a` reduces to zero modulo `b` AND vice versa. Stronger than LT-set equality; pins ideal eq

Binomial coefficient `C(m, r)` as `i128`, saturating on overflow. Iterates over `min(r, m − r)` terms via the integer recurrence `C(m, i+1) = C(m, i)

Ring index of the auxiliary variable for the `bitsum_i`-th bitsum, given the user-variable count and the disequality count. Single source of the encod

BN128 / BN254 scalar field prime (~2^254). Used as a real ZK use case.

Build a small consistent system on a freshly-built ring (sparse).

Build the default two-partition split-GB generator sets and their per-generator provenance. - basis 0 (linear): the bitsum definition polys, then

Canonical sort key: sparse polys → ordered, monic, sorted-by-LT-desc form.

Solve the current fact set with cooperative cancellation.

Each term as `(coeff, sorted nonzero (var, exp) pairs)` — the representation-native read the IR lowering / SMT backends use.

Raw *direct* Gröbner basis (plain Buchberger, no strategy dispatch) on `poly_ring`, routed to the sparse or dense engine per the active representation

Tier 1: atom polynomial fully reduces under `pinned`; derive its truth from the constant result. Reason = pinning sources.

Build a monomial from an exponent slice. Exponents are cast from `usize` down to `u16`.

Helper: compute the reduced dense GB via the F4-lite path; lift to sparse.

Match `b·(b - 1) = 0` on an [`PolyTerm`] list. The list is expected to already be normalised by `rewrite_system`, so `b^2` lives as `[(b_idx, 2)]` and

Polynomial long division: returns `(q, r)` such that `self = q * other + r` with `deg(r) < deg(other)`. Panics if `other` is zero.

Encode this `PolyIR` into an [`EncodedSystem`] ready for the GB engine. Internally builds a `ConstraintSystem` via [`Self::to_constraint_system`] and

Build a real `EncodedSystem` with one equality (`x - 5 = 0`) and one disequality (`x != 0`) so its provenance carries an `Equality(_)` and a `Rabinowi

Enter one macro expansion; errors if the recursion is too deep (a recursive `define-fun`, which SMT-LIB forbids). Pair with [`ParseCtx::exit_expansion

Cached reason for an atom returned by the most recent `propagate()`. Empty result on cache miss is treated as a contract violation by `enqueue_theory`

Cancel-aware model search.

Component-wise minimum: the GCD in monomial-land.

Compute a Gröbner basis of `generators` in `order` via GVW. The result is a (not necessarily reduced) GB; the caller interreduces.

Inter-reduce with cooperative cancellation. Returns the partially-reduced basis (still valid generators, just not yet inter-reduced) on cancel.

Same as `into_lit_pos` but with negative polarity (disequality).

Convert into a Lit assuming polarity-positive interpretation. Returns `Some(Lit::pos(v))` for a real atom; `None` for a trivially-true atom (caller mu

Component-wise maximum: the LCM in monomial-land.

Multiply in place by `t^d` (shift coefficients up by `d`).

Negate every coefficient in place.

Allocate a fresh auxiliary SAT variable that has no associated atom (used by Tseitin transformations).

Called immediately before [`on_new_poly`] to report the active-basis indices that contributed to reducing the S-polynomial to its normal form. Observe

`var_names = ["x"]` but the single equality references var index 5. `compact_used_vars` collects `{5}` whose count equals `var_names.len()`, so it ear

Pop the highest-activity Undef variable from the heap, applying the saved phase (positive when none was saved).

Convert a polynomial to sparse row form (column-ascending). The polynomial's terms are stored in monomial-DESCENDING order and columns are assigned wi

Linear (Gaussian) pre-elimination — the in-tree analogue of cvc5's `theory/ff/gauss.cpp`. Computes a Gröbner basis of the linear equality subsystem (f

Per-pair S-poly construction + geobucket reduction. Shared with `run()` so `run_f4` can fall back to it for batches below [`F4_MIN_BATCH`], where the

If `poly` has exactly one product monomial and it is a product of two distinct degree-1 variables (no squares, no higher degree), return that variable

Cancel-aware variant of [`Self::reduce_by_refs`]. On cancel, returns the partial remainder accumulated so far — sound (same residue class) but not nec

Variant of [`Self::reduce_by_refs_cancel`] that also records, in `use_counts`, how many times each divisor was selected as the reducer during this cal

Resync after a lemma forced a backjump: rewind the theory trail to the new decision level and rewind `notified` so the next pass re-notifies from the

Normalize every equality in a [`ConstraintSystem`]. Equalities whose term list collapses to empty are dropped.

Drive sparse_gb on each system, drive dense Buchberger on the dense lift, compare via mutual ideal-membership.

Monic-normalised S-polynomial of two nonzero polynomials: `(1/lc(f))·(L/lm(f))·f − (1/lc(g))·(L/lm(g))·g`, `L = lcm(lm(f), lm(g))`.

Seed a fresh `BuchbergerState` with `n` distinct single-variable generators x0..x_{n-1}. They are mutually coprime, so none deactivates another and al

Set a solver option (e.g. `"produce-models"`, `"true"`).

Update the builder's prime in place. Used by long-lived builders (e.g. `SmtSession::builder`) whose prime is only known after a `define-sort` or first

Multi-prime entry: solve a list of per-prime `(prime, var_names, formula)` triples against a single SAT solver and a [`FfTheoryRouter`]. Tseitin runs

Single Groebner basis solver. Uses Buchberger observer hooks to trace which input polynomials contribute to an UNSAT proof.

Subtract `other` from `self` in place. Per-coefficient `i64::saturating_sub`.

Lower this `PolyIR` to a CDCL(T) [`BooleanQuery`] for the native solver's disjunction-aware path. The conjunctive constraints (`equalities`, `assignme