This library provides the two encoding strategies that translate a set of membership observations into an SMT constraint system whose satisfying assignments are WFAs consistent with those observations. This corresponds to the getAutomaton abstraction of Definition 5 in the paper.
Encoding.Intf defines Encoding.Intf.T, the shared interface for both strategies. An encoding value of type t accumulates SMT variables and constraint batches. The learner calls:
Encoding.Intf.T.mk â once per hypothesis size to allocate fresh variables.Encoding.Intf.T.add â after each counterexample to incorporate new membership observations.Encoding.Intf.T.get (incremental mode) or Encoding.Intf.T.all (non-incremental mode) to extract constraints for the solver.Encoding.Intf.T.aut â after a SAT result to reconstruct the hypothesis WFA from the model.Encoding.Naive â Direct WFA semantics encoding (Section 4.1 of the paper). For each observed word w with value s, asserts Κ ¡ M(w) ¡ Îť = s. Simple but quadratic in observations Ă states.Encoding.Gen â Generative / state-language encoding (Section 4.2, Figure 1). Introduces state-language variables gᾢ(w) representing the weight of suffix w from state i, then emits span and stability constraints. Shares sub-computations across observations, giving much smaller systems in practice.Encoding.get returns a first-class module (module Intf.T) for the chosen strategy. This is called in bin/main.ml based on the --encoding flag.