why3 1.3.2 · OCaml Package

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

val load_default_config_if_needed : config -> config

type prover = {

prover_name : string;
prover_version : string;
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 = {

prover : prover;
command : string;
command_steps : string option;
driver : string;
in_place : bool;
editor : string;
interactive : bool;
extra_options : string list;
extra_drivers : string list;
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 = {

editor_name : string;
editor_command : string;
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 =

| CPU_keep
| CPU_upgrade of prover
| CPU_duplicate of prover
| 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 = {

strategy_name : string;
strategy_desc : string;
strategy_code : string;
strategy_shortcut : string;

}

val get_strategies : config -> config_strategy Wstdlib.Mstr.t

val add_strategy : config -> config_strategy -> config

type detected_prover = {

exec_name : string;
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

package why3