Why3 API documentation

Util

Useful functions

Opt

Useful option combinators

Lists

Useful list combinators

Strings

Additional Useful Functions on Character Strings

Getopt

Parsing of command-line options.

Extmap

Association tables over ordered types

Extset

Sets over ordered types

Exthtbl

Association tables over hashable types

Weakhtbl

Hashtables with weak key used for memoization

Wstdlib

Specific instances of Set, Map, Hashtbl on int, string, float, and tagged types

Rc

Rc file management

Debug

Debug flag handling

Loc

Source locations

Pp

Helpers for formatted pretty-printing

BigInt

Wrapper for big nums, implemented either with OCaml's Nums or ZArith

Number

General functions for representations of numeric values

Mlmpfr_wrapper
Ident

Identifiers

Ty

Types

Term

Terms and Formulas

Decl

Logic Declarations

Coercion
Theory

Theories and Namespaces

Env

Environments

Task

Proof Tasks, Cloning and Meta History

Trans

Task transformations

Pretty

Pretty-printing various objects from Why3's core logic

Printer
Model_parser

Counter-example model values

Ptree_helpers
Typing

Typing parse trees

Mlw_printer

Pretty printing of Why3 parse trees as WhyML source code

Whyconf

Managing the configuration of Why3

Call_provers

Call provers and parse their outputs

Driver

Managing the drivers for external provers

Args_wrapper

Pre-processing of transformations with arguments, including parsing and typing in the context of a task.

Ity
Expr
Pdecl
Pmodule
Vc
Pinterp_core

Basic definitions for Pinterp and Rac

Rac

RAC implementation(s)

Pinterp

Interpretation of Why3 programs

Check_ce

Validation of candidate counterexamples and classification of proof failures using runtime-assertion checking

Session_itp

Proof sessions

Controller_itp

Controller to run provers and transformations asynchronously on goals of a session

Itp_communication
Itp_server

Server for a client/server communication with an external graphical interface

Ptree

Parse trees