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.

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.