Module `Why3find.Prover`Source

Types representing provers and associated operations

Prover descriptions

Sourcetype desc

The type of prover descriptions, identifying a unique prover version.

Sourceexception InvalidPattern of string

Sourceexception InvalidProverDescription of string

Raised on invalid pattern or prover description, see below. The argument is the erroneous string.

Sourceval desc_to_string : desc -> string

Sourceval desc_of_string : string -> desc

Converts prover descriptions to and from string. The syntax is the same as patterns below, but the version part is mandatory.

raises InvalidProverDescription
when the string description is invalid.

Sourceval desc_name : desc -> string

Sourceval desc_version : desc -> string

Sourceval pp_desc : Format.formatter -> desc -> unit

Sourceval compare_desc : desc -> desc -> int

Prover descriptions comparison function. Different provers are ordered alphabetically by names, and different version of a same prover by reverse version order. Thus, when sorting, the latest version come before older ones.

module Mdesc : Why3.Extmap.S with type key = desc

Provers

Sourcetype prover = private {

desc : desc;
config : Why3.Whyconf.config_prover;
driver : Why3.Driver.driver;
digest : string;

}

The type of provers.

digest is an hexadecimal digest of the prover and its config. For now, drivers are not completly taken into account, for instance modifying a driver which is imported into the main driver won't change the digest.

Sourceval why3_desc : prover -> string

The prover descriptions in Why3 syntax.

Sourceval name : prover -> string

Sourceval version : prover -> string

Sourceval fullname : prover -> string

Sourceval infoname : prover -> string

Sourceval pp_prover : Format.formatter -> prover -> unit

Prints prover fullname.

Patterns

Patterns identify provers. The syntax is prover-name@prover-version. The prover-name match the prover name case-insensitively. (eg alt-ergo match the prover of Why3 name Alt-Ergo) The version part, starting from the '@', is optional. If omitted, it generally means the last available version.

Sourceval pattern_name : string -> string

Sourceval pattern_version : string -> string option

Sourceval pmatch : pattern:string -> desc -> bool

Whether the given pattern match the prover description.

raises InvalidPattern
when the pattern is invalid.

Retrieving available provers

Sourceval all : Config.wenv -> prover Mdesc.t

Returns the set of all available provers for the given Why3 environment.

Sourceval select : Config.wenv -> patterns:string list -> prover list

Selects the provers that match one of the patterns. For each pattern in order, if the pattern is invalid or the prover is not in the map, a warning is emitted, otherwise one prover is appended to the return list, either the one specified or the latest available version in case of a version-less pattern.

Sourceval default : Config.wenv -> prover list

Returns the set of available "default" provers.

Source

val check_and_get_prover : 
  Config.wenv ->
  patterns:string list ->
  desc ->
  prover option

Returns the requested prover from the provers list. Warn if the prover is not found.

package why3find

Module Why3find.ProverSource

Prover descriptions

Provers

Patterns

Retrieving available provers

Module `Why3find.Prover`Source