why3 1.3.2 · OCaml Package

type proof_attempt_status =

val print_status : Format.formatter -> proof_attempt_status -> unit

type transformation_status =

val print_trans_status : Format.formatter -> transformation_status -> unit

type strategy_status =

val print_strategy_status : Format.formatter -> strategy_status -> unit

val default_delay_ms : int

module type Scheduler = sig ... end

type controller = private {

mutable controller_session : Session_itp.session;
mutable controller_config : Whyconf.config;
mutable controller_env : Env.env;
controller_provers : (Whyconf.config_prover * Driver.driver) Whyconf.Hprover.t;
controller_strategies : (string * string * string * Strategy.instruction array) Wstdlib.Hstr.t;
controller_running_proof_attempts : unit Session_itp.Hpan.t;

}

val create_controller : 
  Whyconf.config ->
  Env.env ->
  Session_itp.session ->
  controller

val set_session_max_tasks : int -> unit

val set_session_memlimit : controller -> int -> unit

val set_session_timelimit : controller -> int -> unit

val set_session_prover_upgrade_policy : 
  controller ->
  Whyconf.prover ->
  Whyconf.prover_upgrade_policy ->
  unit

val print_session : Format.formatter -> controller -> unit

exception Errors_list of exn list

val reload_files : 
  ?hard_reload:bool ->
  controller ->
  shape_version:int option ->
  bool * bool

val add_file : controller -> ?format:Env.fformat -> string -> unit

val remove_subtree : 
  notification:Session_itp.notifier ->
  removed:Session_itp.notifier ->
  controller ->
  Session_itp.any ->
  unit

val get_undetached_children_no_pa : 
  Session_itp.session ->
  Session_itp.any ->
  Session_itp.any list

val set_partial_config : controller -> Whyconf.config -> unit

module Make (_ : Scheduler) : sig ... end

package why3