Module _.Enumeration

type t

The current state of the value enumeration.

val next : t -> (Binsec_kernel.Bitvector.t * Model.t) option

next e gives the following value possible for the enumeration e. If there is no remaining value, it returns None.

  • raises Unknown

    when no solution is found within the current resource budget (see SetSMTSolverTimeout).

val suspend : t -> unit

suspend e pauses the enumeration e and releases the external ressources (e.g. solver session).

It can be used to release ressources as soon as the enumeration is no longer used or will not be used for a long time. Calling next resumes a suspended enumeration where it was paused.