Learner.SWALSWAL algorithm (Algorithm 1 of the paper).
Learns a minimal WFA over a semiring S by iteratively: 1. Extending the observation set with membership queries derived from counterexamples. 2. Asking the SMT solver for a WFA of the current hypothesis size consistent with all observations. 3. If UNSAT, incrementing the state count and retrying. 4. If SAT, extracting a hypothesis WFA and submitting it to the teacher. 5. On equivalence, terminating; on a new counterexample, looping to (1).
The encoding E is a first-class module (either Naive or Gen) chosen at the call site in bin/main.ml; the SMT backend SMT is similarly injected. This parametricity is the key to SWAL's generality over semirings and encoding strategies.
module S : Algebra.Semiring.Tmodule E : Encoding.T with type a = Automata.WFA.Make(S).t and type s = S.ttype aut = Automata.WFA.Make(S).ttype teacher = Teacher.Make(S).tval mk :
teacher ->
seed:Base.int ->
logic:Base.bool ->
inc:Base.bool ->
exts:(Automata.Word.t -> Automata.Word.set) ->
tmk teacher ~seed ~logic ~inc ~exts initializes a learner.
seed: SMT solver random seed (for reproducibility).logic: if true, pass the semiring-specific SMT logic to the solver (tighter than Logic.ALL, may speed up solving).inc: use incremental SMT mode (push/pop instead of re-asserting).exts: counterexample extension function; maps a counterexample word to the set of words whose membership values are added to the observation set. Choices are Id (just the cex), Prefixes, or Suffixes (controlled by --exts).