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