Module AltErgoLib.Frontend

type used_context
val init_all_used_context : unit -> used_context
val choose_used_context : used_context -> goal_name:string -> used_context
type 'a status =
  1. | Unsat of Commands.sat_tdecl * Explanation.t
  2. | Inconsistent of Commands.sat_tdecl
  3. | Sat of Commands.sat_tdecl * 'a
  4. | Unknown of Commands.sat_tdecl * 'a
  5. | Timeout of Commands.sat_tdecl option
  6. | Preprocess
val print_status : 'a status -> int -> unit
module type S = sig ... end
module Make (SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t