Module `Algebra.Nat`

Natural-number semiring: (ℕ, +, ×, 0, 1), optionally bounded.

When bound = Some b, addition and multiplication are capped at b, giving the bounded semiring {0,…,b} used for the NatNasty benchmark. When bound = None, the semiring is ℕ (unbounded), used by the Gerco and Primes benchmarks.

SMT encoding uses QF_NIA (non-linear integer arithmetic) because symbolic multiplication can produce non-linear terms. Each symbol sym gets domain constraint sym ≥ 0 (and sym ≤ b when bounded).

module Log : sig ... end

module T : sig ... end

val get : Base.Int.t Base.Option.t -> (module Semiring.T with type t = T.t)

get bound returns a first-class semiring module for the given optional bound. The functor pattern (returning a module) is necessary because the bound is a runtime value but the semiring must be a compile-time module.