Module Algebra.Tropical_lia

Tropical semiring — integer-arithmetic encoding, bounded or unbounded.

The tropical semiring is ({∞} ∪ ℕ, min, +, ∞, 0). This module covers two modes controlled by the optional bound argument to get:

• bound = None: unbounded tropical over ℕ ∪ {∞}. Infinity is represented by the sentinel integer -1; ordinary weights are ≥ 0. SMT operations use ITE guards to handle the infinity sentinel.
• bound = Some b: bounded tropical over {∞} ∪ {0,…,b}. Infinity is represented by b + 1; multiplication saturates at that value. In bounded mode the ITE guards can be omitted because overflow naturally produces a value ≤ b+1.

Logic is QF_LIA (linear integer arithmetic) in both modes. Compare with Tropical_bv which encodes the bounded case as QF_BV.