Lang.Rand_tropical_lia_100Random tropical WFA benchmark — bounded tropical, integer-arithmetic encoding.
Like Rand_tropical_100 but uses Tropical_lia.get (Some 100) (QF_LIA) instead of the bitvector encoding. Exists to allow a direct comparison between QF_BV and QF_LIA on the same target WFA family.
module Log : sig ... endmodule S : sig ... endmodule Matrix : sig ... endmodule Aut : sig ... endval alpha :
int ->
(Automata.Char.t, Automata.Char.comparator_witness) Base.Set.tval aut : Base.Int.t -> int -> Aut.tval get : Base.Int.t -> Base__Int.t -> (module Intf.T)