This library defines the benchmark WFAs used in the paper's evaluation. Every module implements Lang.Intf.T, which bundles a semiring, an alphabet, a counterexample bound, and the semantic function.
Lang.Intf — the T module type that all benchmarks satisfy.
Lang.Gerco — Unbounded natural-number WFA, 1 letter, 2 states. Simple smoke-test.Lang.Primes — Unbounded natural-number WFA, 4 letters, 2 states. Output is the product of prime weights of letters.Lang.Nat_nasty — Bounded natural-number WFA (cap 12 000), 1 letter, 6 states. Hard coefficients stress the QF_NIA solver.Lang.Rat_nasty — Rational-number WFA, same structure as Nat_nasty. Cross-multiplication constraints make it harder.Lang.Probs — Probabilistic 2-state Markov chain, 1 letter.Lang.Residual — Denis et al. minimal NFA family (Boolean semiring), parameterized by state count n and alphabet size k. Invoked as residual:N:K.Lang.Debug — Small hand-crafted tropical WFA used for debugging.All random benchmarks use the transition-density heuristic: each (state, character) transition entry is non-zero independently with probability 1.5 / q, where q is the number of states.
Lang.Rand_tropical — Unbounded tropical QF_LIA. Invoked as rand_tropical:Q:S.Lang.Rand_tropical_100 — Bounded tropical (cap 100) QF_BV. Invoked as rand_tropical_100:Q:S.Lang.Rand_tropical_lia_100 — Bounded tropical (cap 100) QF_LIA. Invoked as rand_tropical_lia_100:Q:S.Lang.Rand_tropical_1000 — Bounded tropical (cap 1000) QF_BV. Invoked as rand_tropical_1000:Q:S.Lang.Rand_tropical_lia_1000 — Bounded tropical (cap 1000) QF_LIA. Invoked as rand_tropical_lia_1000:Q:S.Lang.Rand_bottleneck — Bottleneck semiring QF_LIA. Invoked as rand_bottleneck:Q:S.Implement Lang.Intf.T, add a variant to Lang.t, and add a case to Lang.get.