module SAT : Sat_solver_sig.Stype sat_env = SAT.ttype 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| Preprocessval 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.tval print_status : status -> int -> unitval init_all_used_context : unit -> used_contextval choose_used_context : used_context -> goal_name:string -> used_context