Module `Encoding.Naive`

Naive encoding (Section 4.1 of the paper).

For each observed word w with value s, directly encodes the WFA semantics as the SMT constraint: iota · M(a₁) · M(a₂) · … · M(aₙ) · lambda = s where iota is the initial row-vector, lambda the output column-vector, and M(a) the transition matrix for character a.

This approach is correct and simple, but its constraint size grows as |obs| × |states|², because computing each iota · M(w) · lambda requires a full matrix-chain multiplication in SMT. The generative encoding (Gen) avoids this by introducing state-language variables that share sub-computations across 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