Nat_nasty (SWAL.Lang.Nat

NatNasty benchmark — bounded natural-number WFA.

A 6-state WFA over the single-letter alphabet {a} using the bounded natural-number semiring (Nat.get (Some 12000), QF_NIA). The hand-crafted transition matrix contains large coefficients (125, 5) that make the learner's SMT constraint system harder to satisfy, stressing the solver with a tight bound of 12 000. Used to benchmark SWAL's performance on challenging integer arithmetic instances.

module S : sig ... end

module Matrix : sig ... end

module Aut : sig ... end

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

val bound : int

val aut : Aut.t

val out : Automata.Word.t -> Aut.s