Module type Semiring.T

The module type that every semiring implementation must satisfy.

A semiring is a set t equipped with two binary operations add (⊕) and mul (⊗), two distinguished elements zero (additive identity) and one (multiplicative identity), satisfying the usual semiring axioms. Every concrete module—Bool, Nat, Rat, Prob, Tropical_lia, Tropical_bv, Bottleneck—must implement this interface, making them interchangeable at the call sites in the learner and encodings.

The SMT sub-module lifts the semiring operations into Smtml expressions so that the same algebraic structure can be used both concretely (to evaluate a WFA on a word) and symbolically (to build the SMT constraint system solved by SWAL).

type t

Concrete semiring element.

type comparator_witness

Required by Base.Comparator for use as a map / set key.

val zero : t

Additive identity (⊕-neutral element).

val one : t

Multiplicative identity (⊗-neutral element).

val rand : ?non_zero:Base.float -> ?max:Base.int -> Base.unit -> t

rand ~non_zero ~max () generates a random element. non_zero is the probability that the result is non-zero (default semiring-specific). max bounds the magnitude for numeric semirings. Used by the random benchmark generators in lib/lang/rand_*.ml.

val add : t -> t -> t

Semiring addition (⊕).

val mul : t -> t -> t

Semiring multiplication (⊗).

val elements : Base.unit -> t Base.list

Enumerate all elements of the semiring. Only defined for finite semirings (Bool, bounded Nat, bounded Tropical, etc.); raises a fatal error for infinite semirings such as unbounded Nat or Rat.

module SMT : sig ... end

Lifts the semiring into SMT expressions via Smtml.

val compare : t -> t -> Base.int
val equal : t -> t -> Base.bool
val hash : t -> Base.int
val hash_fold_t : Base.Hash.state -> t -> Base.Hash.state
val to_string : t -> Base.string
val sexp_of_t : t -> Base.Sexp.t