why3 1.1.1 · OCaml Package

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 =

| Result of Call_provers.prover_result * Call_provers.prover_result
| CallFailed of exn
| Replay_interrupted
| Prover_not_installed
| Edited_file_absent of string
| No_former_result of Call_provers.prover_result

val replay_print : 
  Format.formatter ->
  (Session_itp.proofNodeID
   * Whyconf.prover
   * Call_provers.resource_limit
   * report)
    list ->
  unit

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

package why3

Parameters

Signature