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 -> int64 -> unit ) ->
used_context ->
(sat_env * bool * Explanation.t) ->
Commands.sat_tdecl ->
sat_env * bool * Explanation.t
val print_status : status -> int64 -> unit
val init_all_used_context : unit -> used_context
val choose_used_context : used_context -> goal_name:string -> used_context