Rat_nasty (SWAL.Lang.Rat

RatNasty benchmark — rational-number WFA.

The rational analogue of Nat_nasty: the same 6-state, 1-letter WFA structure with coefficients 125, 5 and output 4, now over the rational semiring (Rat, QF_NIA). Rational values are encoded as (numerator, denominator) integer pairs in the SMT encoding, making this benchmark harder than NatNasty due to the cross-multiplication constraints.

module S = Algebra.Rat

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