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 status =
  1. | Unsat of Commands.sat_tdecl * Explanation.t
  2. | Inconsistent of Commands.sat_tdecl
  3. | Sat of Commands.sat_tdecl
  4. | Unknown of Commands.sat_tdecl
  5. | Timeout of Commands.sat_tdecl option
val print_status : status -> int -> unit
module type S = sig ... end
module Make (SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t