Module Algebra.Prob

Probabilistic semiring: (0,1 ∩ ℚ, min(·+·, 1), ×, 0, 1).

Addition is truncating rational sum (capped at 1), multiplication is rational multiplication. This models probabilistic automata where weights are acceptance probabilities.

Like Rat, SMT variables are represented as (numerator, denominator) integer pairs. The additional domain constraints num ≥ 0 and den ≥ num (i.e. num/den ≤ 1) enforce that every symbol denotes a probability in 0, 1. Logic is QF_NIA.

module Log : sig ... end
module T : sig ... end
include module type of struct include T end
type t = Q.t
val compare : t -> t -> Base.int
val equal : t -> t -> Base.bool
val hash : Q.t -> int
val hash_fold_t : Base.Hash.state -> Q.t -> Base.Hash.state
val sexp_of_t : Q.t -> Sexplib0__.Sexp.t
include sig ... end
type comparator_witness = Base__Comparator.Make(T).comparator_witness
val comparator : (T.t, comparator_witness) Base__Comparator.comparator
val zero : Q.t
val one : Q.t
val rand : ?non_zero:Base__Float.t -> ?max:Base.Int.t -> unit -> Q.t
val add : Q.t -> Q.t -> Q.t

Truncating addition: min(a + b, 1).

val mul : Q.t -> Q.t -> Q.t
val elements : unit -> 'a
val to_string : Q.t -> string
module SMT : sig ... end