Deterministic xorshift PRNG so the fuzz corpus is reproducible.

RAII guard: sets the thread-local silence flag and restores its prior value on drop (including on unwind).

Deterministic xorshift64* PRNG — reproducible, no dependency.

Wrapper over the list of variables appearing in a polynomial. Supports both `.is_empty()` and iteration over `usize` variable indices.

Interning table: maps canonical atom keys to SAT variables.

A misconfigured algorithm that advertises tracing support but leaves `compute_traced` at its default. The trait contract requires an implementor that

Internal basis element: the polynomial, its cached leading monomial, the lazy-deactivation flag, and the sugar degree at insertion.

State for bit propagation across multiple GBs.

Brancher: lazily produces (var_idx, value) candidates. Three modes: - `Roots`: pre-computed root list (from univariate factoring or min-poly). - `Rou

Stateful sparse Buchberger run. Mirrors the dense `buchberger::BuchbergerState` shape: a basis with non-strict deactivation, a sugar-ordered open queu

Homogenise → Buchberger on `P[h]` (DegRevLex) → dehomogenise → interreduce. Wins on bit-decomposition shaped ideals where sugar mis-prediction stalls

Plain Buchberger on `P` in the requested order. The default.

Observer hook for tracking the polynomial dependency DAG (used by the UNSAT-core tracer).

Cached state computed from the constraint side of one [`ConstraintSystem`] (everything except `disequalities`).

A parsed command (e.g. `assert`, `check-sat`, `declare-const`). Commands are produced by [`InputParser::next_command`] and can be executed on a solve

RAII override: installs `new` for the lifetime of the guard, then restores the previous config on drop. Tests use this to flip a single knob without l

What the GM / B criteria need from an S-pair, independent of the monomial representation.

Build a fresh `PropagationCtx` view over caller-owned slots. Convention: we pre-populate `unknown` so promotions become visible.

A resolved datatype. Obtained from a sort via [`Sort::datatype`] after the datatype has been created with [`TermManager::mk_dt_sort`](crate::TermMana

A constructor of a resolved datatype.

A declaration for a datatype constructor (before the datatype is resolved).

A declaration for a datatype (before it is resolved into a sort).

A selector of a resolved datatype constructor.

A recognised binary decomposition `target = Σ 2^k · bits[k]`.

Encoded polynomial system ready for GB computation.

Union-find equality engine with same-polynomial atom dedup.

View of a basis element for F4 consumption. Indexed parallel to `BuchbergerState::basis` so `SPair::{i, j}` remain valid. `active = true` means the e

A multivariate polynomial ring GF(p)[x_0, ..., x_{n-1}]. `pr.ring` is a thin facade around the underlying [`crate::ff::polynomial::PolyRing`] context

FF theory plug-in: maintains an asserted-fact trail and dispatches `post_check` to [`solve_encoded_with_cancel`].

Multi-prime FF theory router. One [`PrimeSlot`] per distinct GF(p).

Each stack frame holds: (bases, partial_assignment, brancher)

Pluggable Groebner-basis algorithm. Every public GB entry point (`compute_gb_with_order` and its traced sibling) routes through [`compute_gb_dispatch

Result of a Groebner basis computation.

Result of a traced Groebner basis computation.