package why3

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type config
exception ConfigFailure of string * string
exception DuplicateShortcut of string
val read_config : string option -> config
val merge_config : config -> string -> config
val save_config : config -> unit
val default_config : string -> config
val get_conf_file : config -> string
type main
val get_main : config -> main
val set_main : config -> main -> config
val set_stdlib : bool -> config -> config
val set_load_default_plugins : bool -> config -> config
val set_load_default_config : bool -> config -> config
val libdir : main -> string
val datadir : main -> string
val loadpath : main -> string list
val set_loadpath : main -> string list -> main
val timelimit : main -> int
val memlimit : main -> int
val running_provers_max : main -> int
val set_limits : main -> int -> int -> int -> main
val default_editor : main -> string
val set_default_editor : main -> string -> main
val plugins : main -> string list
val pluginsdir : main -> string
val set_plugins : main -> string list -> main
val add_plugin : main -> string -> main
val load_plugins : main -> unit
type prover = {
  1. prover_name : string;
  2. prover_version : string;
  3. prover_altern : string;
}
val print_prover : Format.formatter -> prover -> unit
val print_prover_parseable_format : Format.formatter -> prover -> unit
val prover_parseable_format : prover -> string
module Prover : sig ... end
module Mprover : sig ... end
module Sprover : sig ... end
module Hprover : sig ... end
type config_prover = {
  1. prover : prover;
  2. command : string;
  3. command_steps : string option;
  4. driver : string;
  5. in_place : bool;
  6. editor : string;
  7. interactive : bool;
  8. extra_options : string list;
  9. extra_drivers : string list;
  10. detected_at_startup : bool;
}
val get_complete_command : config_prover -> with_steps:bool -> string
val get_provers : config -> config_prover Mprover.t
val get_prover_config : config -> prover -> config_prover
val set_provers : config -> ?shortcuts:prover Wstdlib.Mstr.t -> config_prover Mprover.t -> config
val is_prover_known : config -> prover -> bool
val get_prover_shortcuts : config -> prover Wstdlib.Mstr.t
val set_prover_shortcuts : config -> prover Wstdlib.Mstr.t -> config
type config_editor = {
  1. editor_name : string;
  2. editor_command : string;
  3. editor_options : string list;
}
module Meditor : sig ... end
val set_editors : config -> config_editor Meditor.t -> config
val get_editors : config -> config_editor Meditor.t
val editor_by_id : config -> string -> config_editor
type prover_upgrade_policy =
  1. | CPU_keep
  2. | CPU_upgrade of prover
  3. | CPU_duplicate of prover
  4. | CPU_remove
val print_prover_upgrade_policy : Format.formatter -> prover_upgrade_policy -> unit
val set_prover_upgrade_policy : config -> prover -> prover_upgrade_policy -> config
val get_prover_upgrade_policy : config -> prover -> prover_upgrade_policy
val get_policies : config -> prover_upgrade_policy Mprover.t
val set_policies : config -> prover_upgrade_policy Mprover.t -> config
type config_strategy = {
  1. strategy_name : string;
  2. strategy_desc : string;
  3. strategy_code : string;
  4. strategy_shortcut : string;
}
val get_strategies : config -> config_strategy Wstdlib.Mstr.t
val add_strategy : config -> config_strategy -> config
type detected_prover = {
  1. exec_name : string;
  2. version : string;
}
val set_detected_provers : config -> detected_prover list -> config
val get_detected_provers : config -> detected_prover list
type filter_prover
val mk_filter_prover : ?version:string -> ?altern:string -> string -> filter_prover
val print_filter_prover : Format.formatter -> filter_prover -> unit
val parse_filter_prover : string -> filter_prover
val filter_prover_with_shortcut : config -> filter_prover -> filter_prover
val filter_prover : filter_prover -> prover -> bool
val filter_provers : config -> filter_prover -> config_prover Mprover.t
exception ProverNotFound of config * filter_prover
exception ProverAmbiguity of config * filter_prover * config_prover Mprover.t
exception ParseFilterProver of string
val filter_one_prover : config -> filter_prover -> config_prover
val why3_regexp_of_string : string -> Re.Str.regexp
val get_section : config -> string -> Rc.section option
val get_family : config -> string -> Rc.family
val set_section : config -> string -> Rc.section -> config
val set_family : config -> string -> Rc.family -> config
module Args : sig ... end
val load_driver : main -> Env.env -> string -> string list -> Driver.driver
val unknown_to_known_provers : config_prover Mprover.t -> prover -> prover list * prover list * prover list
val provers_from_detected_provers : (config -> config) ref
OCaml

Innovation. Community. Security.