Module `Lang.Rand_tropical_100`

Random tropical WFA benchmark — bounded tropical, bitvector encoding.

Like Rand_tropical but uses the bounded tropical semiring with bound = 100 encoded as bitvectors (Tropical_bv.get 100, QF_BV). Individual transition weights are capped to avoid overflow: max = bound / (q * 2).

The bitvector encoding (QF_BV) is typically faster than the integer arithmetic encoding (QF_LIA) for bounded tropical instances because bitvector reasoning is highly optimized in modern SMT solvers.

module Log : sig ... end

val semi_bound : int

module S : sig ... end

module Matrix : sig ... end

module Aut : sig ... end

val alpha : 
  int ->
  (Automata.Char.t, Automata.Char.comparator_witness) Base.Set.t

val aut : Base.Int.t -> int -> Aut.t

val get : Base.Int.t -> Base__Int.t -> (module Intf.T)