Module Gen.Make

Parameters

module A : Automata.WFA.T with type s = S.t

Signature

type s = S.t

Semiring element type.

type a = A.t

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.