Frontend.Make
module SAT : Sat_solver_sig.S
type sat_env = SAT.t
type status =
| Unsat of Commands.sat_tdecl * Explanation.t
| Inconsistent of Commands.sat_tdecl
| Sat of Commands.sat_tdecl * sat_env
| Unknown of Commands.sat_tdecl * sat_env
| Timeout of Commands.sat_tdecl option
| Preprocess
val process_decl :
(status -> int -> unit) ->
used_context ->
(res * Explanation.t) Stdlib.Stack.t ->
(sat_env * res * Explanation.t) ->
Commands.sat_tdecl ->
sat_env * res * Explanation.t
val print_status : status -> int -> unit
val init_all_used_context : unit -> used_context
val choose_used_context : used_context -> goal_name:string -> used_context