package why3

  1. Overview
  2. Docs
package why3
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.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct