Module Algebra.Tropical_bv

Bounded tropical semiring — bitvector encoding.

The tropical semiring is (ℕ ∪ {∞}, min, +, ∞, 0): addition is min, multiplication is integer addition (with infinity as an absorbing element for multiplication). This module provides a bounded variant with universe {Inf} ∪ {0,…,bound} and encodes values as bitvectors of width bits = ⌈log₂(bound + 2)⌉ + 1.

The infinity sentinel is represented as bound + 1 (the first value outside 0,bound). All arithmetic operations check for this sentinel using unsigned bitvector comparisons. Logic is QF_BV.

get bound returns a first-class semiring module for the given bound. Contrast with Tropical_lia which uses integer arithmetic (QF_LIA) for both bounded and unbounded tropical.