Algebra.BottleneckBottleneck semiring: ({-∞} ∪ ℤ ∪ {+∞}, max, min, -∞, +∞).
Addition is max, multiplication is min. This models bottleneck-capacity shortest-path problems. The semiring is unbounded (only NegInf and PosInf as sentinels) so elements is not supported.
SMT encoding maps the three-constructor type to integers via sentinel values: NegInf → -2, PosInf → -1. Ordinary integer weights live in 0, +∞). Every arithmetic operation branches on the sentinel values via ITE guards. Logic is [QF_LIA].
module Log : sig ... endmodule T : sig ... endinclude sig ... endval comparator : (T.t, comparator_witness) Base__Comparator.comparatorval zero : tAdditive identity: max(NegInf, x) = x for all x.
val one : tMultiplicative identity: min(PosInf, x) = x for all x.
val rand : ?non_zero:Base__Float.t -> ?max:Base.Int.t -> unit -> tval to_string : t -> stringmodule SMT : sig ... end