module TestgenSolver:`sig`

..`end`

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.

`type `

t

`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 restart : ``t -> t`

Restarts a 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.