Module `Encoding.Gen`

Generative encoding (Section 4.2, Figure 1 of the paper).

Instead of encoding the full WFA run directly (as Naive does), this encoding works with state languages: for each state q and suffix word w, a fresh SMT variable gen_q_w represents the value g_q(w) — the weight assigned to w by the sub-automaton rooted at q. Two families of constraints then characterize a consistent WFA:

Span constraints (Φ-span, Figure 1): for each observed word w with value s, assert Σᵢ ιᵢ · gᵢ(w) = s.
Stability constraints (Φ-stable, Figure 1): for each suffix a.w and every state q, assert g_q(a.w) = Σⱼ δ_{a,q,j} · gⱼ(w).

Together these constraints correspond to the equation system Φ(n, O) of Figure 1, where n is the hypothesis size and O is the observation set. A satisfying assignment is precisely an n-state WFA consistent with all observations.

module Make
  (S : Algebra.Semiring.T)
  (A : Automata.WFA.T with type s = S.t) : 
  Intf.T with type s = S.t and type a = A.t