package why3

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type proof_attempt_status =
  1. | Undone
  2. | Scheduled
  3. | Running
  4. | Done of Call_provers.prover_result
  5. | Interrupted
  6. | Detached
  7. | InternalFailure of exn
  8. | Uninstalled of Whyconf.prover
  9. | UpgradeProver of Whyconf.prover
  10. | Removed of Whyconf.prover
val print_status : Format.formatter -> proof_attempt_status -> unit
type transformation_status =
  1. | TSscheduled
  2. | TSdone of Session_itp.transID
  3. | TSfailed of Session_itp.proofNodeID * exn
  4. | TSfatal of Session_itp.proofNodeID * exn
val print_trans_status : Format.formatter -> transformation_status -> unit
type strategy_status =
  1. | STSgoto of Session_itp.proofNodeID * int
  2. | STShalt
  3. | STSfatal of string * Session_itp.proofNodeID * exn
val print_strategy_status : Format.formatter -> strategy_status -> unit
val default_delay_ms : int
module type Scheduler = sig ... end
type controller = private {
  1. mutable controller_session : Session_itp.session;
  2. mutable controller_config : Whyconf.config;
  3. mutable controller_env : Env.env;
  4. controller_provers : (Whyconf.config_prover * Driver.driver) Whyconf.Hprover.t;
  5. controller_strategies : (string * string * string * Strategy.instruction array) Wstdlib.Hstr.t;
  6. 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
OCaml

Innovation. Community. Security.