# Module `TestgenSolver`

Wraps a solver and provides a convenient interface for test generation.

The goal is to be able to trigger the transition relations up to some `k`

. The wrapper thus maintains a list of actlits `a0 ; a1 ; a2 ; ... ; aN`

such that, in the solver: a0 => Init(0) a1 => (and a0 T(0,1)) a2 => (and a1 T(1,2)) ... aN => (and aN-1 T(N-1,N))

The client does not see this however, only the `k`

at which the query should be made is specified. The wrapper unrolls the transition relation lazily whenever it is needed. See `nth_actlit_of`

.

Note: `a0`

is not really needed but is here for consistency.

`val mk : TransSys.t -> t`

Creates a new solver wrapper. The first actlit activates init@0.

`val rm : t -> unit`

Destroys the underlying solver.

`val comment : t -> string -> unit`

Comment trace for the underlying solver.

`val checksat : t -> Numeral.t -> Term.t -> Term.t list -> ('a * Term.t) list -> (SMTSolver.t -> 'b) -> (('a * Term.t) list * 'b) option`

`checksat t n term actlits terms`

Checks the satisfiability of term`term`

in conjunction with activation literals`actlits`

with the system unrolled up to`n`

. A fresh actlit is created for`term`

, and a check-sat with assumptions`term :: actlits`

will be performed. The fresh actlit is deactivated at the end of the check.If sat, returns some of an association list yielding the values of

`terms`

. Returns none otherwise.