Module type Intf.T

The semiring over which the target WFA is defined. Determines which SMT encoding / solver logic will be used.

val alpha : Automata.Char.set

The input alphabet Σ.

val bound : Base.int

Recommended upper bound on the number of words to enumerate during equivalence checking. Chosen per-language to be large enough to exercise the target WFA but not so large as to make equivalence queries dominate runtime. Overridable via --bound.

val out : Automata.Word.t -> S.t

out w returns the weight assigned to word w by the target language. This is the oracle function wrapped by Teacher.Make.