sig
  type proof_attempt_status =
      Undone
    | Scheduled
    | Running
    | Done of Why3.Call_provers.prover_result
    | Interrupted
    | Detached
    | InternalFailure of exn
    | Uninstalled of Why3.Whyconf.prover
    | UpgradeProver of Why3.Whyconf.prover * Why3.Whyconf.prover
    | Removed of Why3.Whyconf.prover
  val print_status :
    Stdlib.Format.formatter -> Controller_itp.proof_attempt_status -> unit
  type transformation_status =
      TSscheduled
    | TSdone of Why3.Session_itp.transID
    | TSfailed of (Why3.Session_itp.proofNodeID * exn)
    | TSfatal of (Why3.Session_itp.proofNodeID * exn)
  val print_trans_status :
    Stdlib.Format.formatter -> Controller_itp.transformation_status -> unit
  type strategy_status =
      STSgoto of Why3.Session_itp.proofNodeID * int
    | STShalt
    | STSfatal of string * Why3.Session_itp.proofNodeID * exn
  val print_strategy_status :
    Stdlib.Format.formatter -> Controller_itp.strategy_status -> unit
  val default_delay_ms : int
  module type Scheduler =
    sig
      val blocking : bool
      val multiplier : int
      val timeout : ms:int -> (unit -> bool) -> unit
      val idle : prio:int -> (unit -> bool) -> unit
    end
  type controller = private {
    mutable controller_session : Why3.Session_itp.session;
    mutable controller_config : Why3.Whyconf.config;
    mutable controller_env : Why3.Env.env;
    controller_provers :
      (Why3.Whyconf.config_prover * Why3.Driver.driver)
      Why3.Whyconf.Hprover.t;
    controller_strategies :
      (string * string * string * Why3.Strategy.instruction array)
      Why3.Wstdlib.Hstr.t;
    controller_running_proof_attempts : unit Why3.Session_itp.Hpan.t;
  }
  val create_controller :
    Why3.Whyconf.config ->
    Why3.Env.env -> Why3.Session_itp.session -> Controller_itp.controller
  val set_session_max_tasks : int -> unit
  val set_session_memlimit : Controller_itp.controller -> int -> unit
  val set_session_timelimit : Controller_itp.controller -> float -> unit
  val set_session_prover_upgrade_policy :
    Controller_itp.controller ->
    Why3.Whyconf.prover -> Why3.Whyconf.prover_upgrade_policy -> unit
  val print_session :
    Stdlib.Format.formatter -> Controller_itp.controller -> unit
  exception Errors_list of exn list
  val reload_files :
    ?hard_reload:bool ->
    ?reparse_file_fun:(Why3.Session_itp.session ->
                       Why3.Env.env ->
                       Why3.Session_itp.file -> Why3.Theory.theory list) ->
    ignore_shapes:bool -> Controller_itp.controller -> bool * bool
  val add_file :
    Controller_itp.controller -> ?format:Why3.Env.fformat -> string -> unit
  val remove_subtree :
    notification:Why3.Session_itp.notifier ->
    removed:Why3.Session_itp.notifier ->
    Controller_itp.controller -> Why3.Session_itp.any -> unit
  val get_undetached_children_no_pa :
    Why3.Session_itp.session ->
    Why3.Session_itp.any -> Why3.Session_itp.any list
  val set_partial_config :
    Controller_itp.controller -> Why3.Whyconf.config -> unit
  module Make :
    Scheduler ->
      sig
        val register_observer : (int -> int -> int -> unit) -> unit
        val interrupt : Controller_itp.controller -> unit
        val interrupt_proof_attempts_for_goal :
          Controller_itp.controller -> Why3.Session_itp.proofNodeID -> unit
        val schedule_proof_attempt :
          ?adjust_limits:bool ->
          ?proof_script_filename:string ->
          Controller_itp.controller ->
          Why3.Session_itp.proofNodeID ->
          Why3.Whyconf.prover ->
          limits:Why3.Call_provers.resource_limits ->
          callback:(Why3.Session_itp.proofAttemptID ->
                    Controller_itp.proof_attempt_status -> unit) ->
          notification:Why3.Session_itp.notifier -> unit
        val schedule_edition :
          Controller_itp.controller ->
          Why3.Session_itp.proofNodeID ->
          Why3.Whyconf.prover ->
          callback:(Why3.Session_itp.proofAttemptID ->
                    Controller_itp.proof_attempt_status -> unit) ->
          notification:Why3.Session_itp.notifier -> unit
        val prepare_edition :
          Controller_itp.controller ->
          ?file:Why3.Sysutil.file_path ->
          Why3.Session_itp.proofNodeID ->
          Why3.Whyconf.prover ->
          notification:Why3.Session_itp.notifier ->
          Why3.Session_itp.proofAttemptID * string *
          Why3.Call_provers.prover_result option
        exception GoalNodeDetached of Why3.Session_itp.proofNodeID
        val schedule_transformation :
          Controller_itp.controller ->
          Why3.Session_itp.proofNodeID ->
          string ->
          string list ->
          callback:(Controller_itp.transformation_status -> unit) ->
          notification:Why3.Session_itp.notifier -> unit
        val run_strategy_on_goal :
          Controller_itp.controller ->
          Why3.Session_itp.proofNodeID ->
          Why3.Strategy.t ->
          callback_pa:(Why3.Session_itp.proofAttemptID ->
                       Controller_itp.proof_attempt_status -> unit) ->
          callback_tr:(string ->
                       string list ->
                       Controller_itp.transformation_status -> unit) ->
          callback:(Controller_itp.strategy_status -> unit) ->
          notification:Why3.Session_itp.notifier ->
          removed:Why3.Session_itp.notifier -> unit
        val run_strat_on_goal :
          Controller_itp.controller ->
          Why3.Session_itp.proofNodeID ->
          string ->
          Why3.Strategy.gen_strat ->
          string list ->
          callback_pa:(Why3.Session_itp.proofAttemptID ->
                       Controller_itp.proof_attempt_status -> unit) ->
          callback_tr:(string ->
                       string list ->
                       Controller_itp.transformation_status -> unit) ->
          callback:(Controller_itp.strategy_status -> unit) ->
          notification:Why3.Session_itp.notifier -> unit
        val clean :
          Controller_itp.controller ->
          removed:Why3.Session_itp.notifier ->
          Why3.Session_itp.any option -> unit
        val reset_proofs :
          Controller_itp.controller ->
          removed:Why3.Session_itp.notifier ->
          notification:Why3.Session_itp.notifier ->
          Why3.Session_itp.any option -> unit
        val mark_as_obsolete :
          notification:Why3.Session_itp.notifier ->
          Controller_itp.controller -> Why3.Session_itp.any option -> unit
        exception BadCopyPaste
        val copy_paste :
          notification:Why3.Session_itp.notifier ->
          callback_pa:(Why3.Session_itp.proofAttemptID ->
                       Controller_itp.proof_attempt_status -> unit) ->
          callback_tr:(string ->
                       string list ->
                       Controller_itp.transformation_status -> unit) ->
          Controller_itp.controller ->
          Why3.Session_itp.any -> Why3.Session_itp.any -> unit
        type report =
            Result of Why3.Call_provers.prover_result *
              Why3.Call_provers.prover_result
          | CallFailed of exn
          | Replay_interrupted
          | Prover_not_installed
          | Edited_file_absent of string
          | No_former_result of Why3.Call_provers.prover_result
        val replay_print :
          Stdlib.Format.formatter ->
          (Why3.Session_itp.proofNodeID * Why3.Whyconf.prover *
           Why3.Call_provers.resource_limits * Controller_itp.Make.report)
          list -> unit
        val set_time_factor : float -> unit
        val replay :
          valid_only:bool ->
          obsolete_only:bool ->
          ?use_steps:bool ->
          ?filter:(Why3.Session_itp.proof_attempt_node -> bool) ->
          Controller_itp.controller ->
          callback:(Why3.Session_itp.proofAttemptID ->
                    Controller_itp.proof_attempt_status -> unit) ->
          notification:Why3.Session_itp.notifier ->
          final_callback:(Controller_itp.proof_attempt_status list ->
                          (Why3.Session_itp.proofNodeID *
                           Why3.Whyconf.prover *
                           Why3.Call_provers.resource_limits *
                           Controller_itp.Make.report)
                          list -> unit) ->
          any:Why3.Session_itp.any option -> unit
        exception CannotRunBisectionOn of Why3.Session_itp.proofAttemptID
        val bisect_proof_attempt :
          callback_tr:(string ->
                       string list ->
                       Controller_itp.transformation_status -> unit) ->
          callback_pa:(Why3.Session_itp.proofAttemptID ->
                       Controller_itp.proof_attempt_status -> unit) ->
          notification:Why3.Session_itp.notifier ->
          removed:Why3.Session_itp.notifier ->
          Controller_itp.controller ->
          Why3.Session_itp.proofAttemptID -> unit
      end
end