package why3

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

Parameters

module S : Scheduler

Signature

val register_observer : (int -> int -> int -> unit) -> unit
val interrupt : unit -> unit
val schedule_proof_attempt : controller -> Session_itp.proofNodeID -> Whyconf.prover -> ?save_to:string -> limit:Call_provers.resource_limit -> callback:(Session_itp.proofAttemptID -> proof_attempt_status -> unit) -> notification:Session_itp.notifier -> unit
val schedule_edition : controller -> Session_itp.proofNodeID -> Whyconf.prover -> callback:(Session_itp.proofAttemptID -> proof_attempt_status -> unit) -> notification:Session_itp.notifier -> unit
val prepare_edition : controller -> ?file:string -> Session_itp.proofNodeID -> Whyconf.prover -> notification:Session_itp.notifier -> Session_itp.proofAttemptID * string * Call_provers.prover_result option
exception TransAlreadyExists of string * string
exception GoalNodeDetached of Session_itp.proofNodeID
val schedule_transformation : controller -> Session_itp.proofNodeID -> string -> string list -> callback:(transformation_status -> unit) -> notification:Session_itp.notifier -> unit
val run_strategy_on_goal : controller -> Session_itp.proofNodeID -> Strategy.t -> callback_pa:(Session_itp.proofAttemptID -> proof_attempt_status -> unit) -> callback_tr:(string -> string list -> transformation_status -> unit) -> callback:(strategy_status -> unit) -> notification:Session_itp.notifier -> unit
val clean : controller -> removed:Session_itp.notifier -> Session_itp.any option -> unit
val mark_as_obsolete : notification:Session_itp.notifier -> controller -> Session_itp.any option -> unit
exception BadCopyPaste
val copy_paste : notification:Session_itp.notifier -> callback_pa:(Session_itp.proofAttemptID -> proof_attempt_status -> unit) -> callback_tr:(string -> string list -> transformation_status -> unit) -> controller -> Session_itp.any -> Session_itp.any -> unit
type report =
  1. | Result of Call_provers.prover_result * Call_provers.prover_result
  2. | CallFailed of exn
  3. | Replay_interrupted
  4. | Prover_not_installed
  5. | Edited_file_absent of string
  6. | No_former_result of Call_provers.prover_result
val replay : valid_only:bool -> obsolete_only:bool -> ?use_steps:bool -> ?filter:(Session_itp.proof_attempt_node -> bool) -> controller -> callback:(Session_itp.proofAttemptID -> proof_attempt_status -> unit) -> notification:Session_itp.notifier -> final_callback: (bool -> (Session_itp.proofNodeID * Whyconf.prover * Call_provers.resource_limit * report) list -> unit) -> any:Session_itp.any option -> unit
exception CannotRunBisectionOn of Session_itp.proofAttemptID
val bisect_proof_attempt : callback_tr:(string -> string list -> transformation_status -> unit) -> callback_pa:(Session_itp.proofAttemptID -> proof_attempt_status -> unit) -> notification:Session_itp.notifier -> removed:Session_itp.notifier -> controller -> Session_itp.proofAttemptID -> unit
OCaml

Innovation. Community. Security.