Module type Intf.T

The module type shared by both encoding strategies (naive and gen).

An encoding accumulates SMT variables and constraints that, when satisfiable, yield a WFA consistent with all membership observations seen so far. This is the getAutomaton abstraction of Definition 5 in the paper: given a set of (word, value) pairs, produce a system of SMT constraints whose solutions correspond to WFAs of the current hypothesis size.

The two implementations are:

type s

Semiring element type.

type a

WFA type (produced by aut when the solver finds a model).

type t

Opaque encoding state: holds all SMT variables and accumulated constraint batches for the current hypothesis size.

val mk : alpha:Automata.Char.set -> states:Base.int -> t

mk ~alpha ~states creates a fresh encoding for a WFA with states states over alphabet alpha. Allocates all SMT variables and emits domain constraints (from Semiring.T.SMT.mk) but no observation constraints yet.

val add : t -> s Automata.Word.map -> t

add enc obs incorporates a new batch of membership observations (word, value) into the encoding. Returns an updated t with new SMT variables (if the gen encoding needs additional generator symbols) and a new constraint batch appended. Pure: enc is not mutated.

val get : t -> Smtml.Expr.t Base.list

get enc returns only the constraints added by the most recent call to add. Used in incremental solving mode (--inc) to push only new assertions onto the solver stack via SMT.add.

val all : t -> Smtml.Expr.t Base.list

all enc returns the full conjunction of all constraints accumulated since mk. Used in non-incremental mode: the entire system is re-asserted on each SMT.check call.

val aut : t -> Smtml.Model.t -> a

aut enc model reconstructs a concrete WFA from a satisfying assignment model by reading back the values of the SMT variables in enc. Called immediately after SMT.check returns `Sat.