Module type Frontend.S

type sat_env
type used_context
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