A | |
abs [Mlmpfr_wrapper] | |
abs [BigInt] | |
abs_int [Number] | |
abs_real [Number] | |
add [Coercion] | adds a new coercion from function |
add [Mlmpfr_wrapper] | |
add [BigInt] | |
add [Extset.S] |
|
add [Extmap.S] |
|
add_body [Ptree_helpers.I] | |
add_body [Ptree_helpers.F] | |
add_builtin [Env] |
|
add_clone_internal [Theory] | |
add_command [Whyconf.Args] | |
add_data_decl [Task] | |
add_data_decl [Theory] | |
add_decl [Typing] | |
add_decl [Task] | |
add_decl [Theory] | |
add_decl_with_tuples [Theory] | |
add_decls [Trans] | |
add_extra_config [Whyconf] |
|
add_file [Controller_itp] |
|
add_file_section [Session_itp] |
|
add_flush [Pp] | |
add_ind_decl [Task] | |
add_ind_decl [Theory] | |
add_int [BigInt] | |
add_left [Extset.S] |
|
add_logic_decl [Task] | |
add_logic_decl [Theory] | |
add_meta [Pmodule] | |
add_meta [Task] | |
add_meta [Theory] | |
add_new [Extset.S] |
|
add_new [Extmap.S] |
|
add_param_decl [Task] | |
add_param_decl [Theory] | |
add_pdecl [Pmodule] |
|
add_plugin [Whyconf] | |
add_post [Ptree_helpers.I] | |
add_post [Ptree_helpers.F] | |
add_pre [Ptree_helpers.I] | |
add_pre [Ptree_helpers.F] | |
add_prop [Ptree_helpers.I] | |
add_prop [Ptree_helpers.F] | |
add_prop_decl [Task] | |
add_prop_decl [Theory] | |
add_registered_lang [Itp_server] | |
add_rliteral_map [Printer] | |
add_strategy [Whyconf] | |
add_syntax_map [Printer] | |
add_tdecl [Task] | |
add_tdecls [Trans] |
|
add_ty_decl [Task] | |
add_ty_decl [Theory] | |
all [Util] | |
all2 [Util] | |
all2_fn [Util] |
|
all_fn [Util] |
|
all_options [Whyconf.Args] | |
alld [Util] | |
alt [Pp] | |
alt2 [Pp] | |
annot_attr [Ity] | |
ansi_color_tags [Util] | Functions to interpret tags as ANSI terminal color codes. |
any [Util] | |
any2 [Util] | |
any2_fn [Util] |
|
any_fn [Util] |
|
any_iter_proof_attempt [Session_itp] | |
any_proved [Session_itp] | |
anyd [Util] | |
append_to_model_element_name [Ident] | The returned set of attributes will contain the same set of attributes
as argument attrs except that an attribute of the form |
append_to_model_trace_attr [Ident] | The returned set of attributes will contain the same set of attributes
as argument attrs except that an attribute of the form |
apply [Trans] | |
apply [Lists] |
|
apply [Opt] | |
apply2 [Opt] | |
apply_trans_to_goal [Session_itp] |
|
apply_transform [Trans] | apply a registered 1-to-1 or a 1-to-n, directly. |
apply_transform_args [Trans] | apply a registered 1-to-1 or a 1-to-n or a trans with args, directly |
aprinter [Pretty.Printer] | |
array_add_element [Model_parser] | Adds an element to the array. |
array_create_constant [Model_parser] | Creates constant array with all indices equal to the parameter value. |
arrow [Pp] | |
asd [Pp] | add string delimiter " " |
asym_split [Term] | |
attr_compare [Ident] | |
attr_equal [Ident] | |
attr_hash [Ident] | |
attr_w_non_conservative_extension_no [Theory] | |
axiom_of_invariant [Pdecl] |
|
B | |
base_language [Env] |
|
base_language_builtin [Env] |
|
begin_let [Ptree_helpers.I] | |
begin_let [Ptree_helpers.F] | |
begin_module [Ptree_helpers.I] | see |
begin_module [Ptree_helpers.F] | |
bind [Trans] | |
bind [Opt] | |
bind_comp [Trans] | |
bindings [Extmap.S] | Return the list of all bindings of the given map. |
bisect_proof_attempt [Controller_itp.Make] |
|
blocking [Controller_itp.Scheduler] | Set to true when the scheduler should wait for results of why3server (script), false otherwise (ITP which needs reactive scheduling) |
bool [Pp] | |
bool_module [Pmodule] | |
bool_theory [Theory] | |
bool_value [Pinterp] | |
bounded_split [Strings] |
|
break_attr [Ity] | |
build_naming_tables [Args_wrapper] | builds a naming tabl from a task, suitable for both parsing/typing transformation arguments and for printing the task, with coherent identifiers names. |
builtin_module [Pmodule] | |
builtin_theory [Theory] | |
C | |
c_any [Expr] | |
c_app [Expr] | |
c_fun [Expr] | |
c_ghost [Expr] | |
c_pur [Expr] | |
c_rs_subst [Expr] | |
call_editor [Call_provers] | |
call_on_buffer [Call_provers] | Build a prover call on the task already printed in the |
capitalize [Strings] | |
cardinal [Extset.S] | Return the number of elements in a set. |
cardinal [Extmap.S] | Return the number of bindings of a map. |
catch_unsupportedDecl [Printer] | same as |
catch_unsupportedTerm [Printer] | same as |
catch_unsupportedType [Printer] |
|
ce_summary [Counterexample] | |
change [Extset.S] |
|
change [Extmap.S] |
|
change_prover [Session_itp] |
|
char_is_uppercase [Strings] | |
char_to_alnum [Ident] | |
char_to_alnumus [Ident] | |
char_to_alpha [Ident] | |
char_to_lalnum [Ident] | |
char_to_lalnumus [Ident] | |
char_to_lalpha [Ident] | |
char_to_ualpha [Ident] | |
check_exhaustive [Rc] |
|
check_float [Number] |
|
check_if_already_exists [Session_itp] | |
check_literal [Term] | |
check_model [Counterexample] | |
check_range [Number] |
|
check_syntax_logic [Printer] | |
check_syntax_type [Printer] | |
choose [Extset.S] | Return one element of the given set, or raise |
choose [Extmap.S] | Return one binding of the given map, or raise |
chop [Lists] | removes the first n elements of a list; raises Invalid_argument if the list is not long enough |
chop_last [Lists] | removes (and returns) the last element of a list |
clean [Controller_itp.Make] | Remove each proof attempt or transformation that are below proved goals, that are either obsolete or not valid. |
clear [Weakhtbl.S] | |
clone_export [Pmodule] | |
clone_export [Task] | |
clone_export [Theory] | |
clone_meta [Theory] |
|
clone_post_result [Ity] | |
clone_theory [Theory] | |
close_file [Typing] | |
close_file_and_formatter [Pp] | |
close_formatter [Pp] | |
close_log [Pinterp.Log] | |
close_module [Pmodule] | |
close_module [Typing] | |
close_scope [Pmodule] | |
close_scope [Typing] | |
close_scope [Theory] | |
close_theory [Theory] | |
cmp [Util] | Create a comparison function using lexical order defined by a list of comparators |
cmp_lists [Util] | Create a comparison function for lists using lexical order defined by a list of comparators |
cmptr [Util] | Create a comparator by a projection and a comparison function between projected values |
cmptr_direct [Util] | |
coercion_attr [Pretty] | |
colon [Pp] | |
comma [Pp] | |
commands [Getopt] |
|
common_options [Whyconf.Args] | |
compare [BigInt] | |
compare [Loc] | |
compare [Wstdlib.OrderedHashedType] | |
compare [Extset.S] | Total ordering between sets. |
compare [Extmap.S] | Total ordering between maps. |
compare [Lists] | |
compare [Opt] | |
compare_real [Number] | structural comparison; two ordered values might compare differently |
complete_initialization [Whyconf.Args] | |
compose [Trans] | |
compose_l [Trans] | |
compute_float [Number] |
|
compute_model_trace_field [Ident] | Take an optional projection name and the depths of its occurence and return the built field attribute associated |
computer_div [BigInt] | |
computer_div_mod [BigInt] | "computer" division, i.e division rounds towards zero, and thus |
computer_mod [BigInt] | |
cons [Lists] | |
const [Ptree_helpers] | |
const [Util] | |
const2 [Util] | |
const3 [Util] | |
const_pi [Mlmpfr_wrapper] | |
constant_formatted [Pp] | |
constant_string [Pp] | |
constr_value [Pinterp] | |
contains [Extset.S] |
|
contains [Extmap.S] |
|
copy [Weakhtbl.S] | |
copy_paste [Controller_itp.Make] | |
create [Ptree_helpers.F] | |
create [Pretty] | `create spr apr tpr ppr forget` creates a new pretty-printing module from the printer `spr` for variables and functions, `apr` for type variables, `tpr` for type symbols and `ppr for proposition names`. |
create [Weakhtbl.S] | |
create_alias_decl [Pdecl] |
|
create_alias_itysymbol [Ity] |
|
create_attribute [Ident] | |
create_call_set [Decl] | |
create_constructor [Expr] | |
create_controller [Controller_itp] | creates a controller for the given session. |
create_cty [Ity] |
|
create_cty_defensive [Ity] | same as |
create_data_decl [Decl] | |
create_debugging_trans [Trans] | |
create_decl [Theory] | |
create_env [Env] | creates an environment from a "loadpath", a list of directories containing loadable Why3/WhyML/etc files |
create_exn_decl [Pdecl] | |
create_float_decl [Pdecl] |
|
create_float_itysymbol [Ity] |
|
create_fsymbol [Term] | ~constr is the number of constructors of the type in which the symbol is a constructor otherwise it must be the default 0. |
create_ident_printer [Ident] | start a new printer with a sanitizing function and a blacklist |
create_ind_decl [Decl] | |
create_let_decl [Pdecl] | |
create_logic_decl [Decl] | |
create_lsymbol [Term] | |
create_meta [Theory] | |
create_model_element [Model_parser] | Creates a counter-example model element. |
create_model_trace_attr [Ident] | |
create_module [Pmodule] | |
create_param_decl [Decl] | |
create_plain_record_decl [Pdecl] |
|
create_plain_record_itysymbol [Ity] |
|
create_plain_variant_decl [Pdecl] |
|
create_plain_variant_itysymbol [Ity] |
|
create_post [Ity] | |
create_prog_pattern [Expr] | |
create_projection [Expr] | |
create_prop_decl [Decl] | |
create_prsymbol [Decl] | |
create_psymbol [Term] | |
create_pure_decl [Pdecl] | |
create_pvsymbol [Ity] | |
create_range [Number] | |
create_range_decl [Pdecl] |
|
create_range_itysymbol [Ity] |
|
create_rec_itysymbol [Ity] |
|
create_rec_record_decl [Pdecl] |
|
create_rec_variant_decl [Pdecl] |
|
create_region [Ity] |
|
create_rsymbol [Expr] | If |
create_tag [Weakhtbl] | |
create_theory [Theory] | |
create_tvsymbol [Ty] | |
create_ty_decl [Decl] | |
create_type_decl [Pdecl] | |
create_tysymbol [Ty] | |
create_use [Theory] | |
create_vs_graph [Decl] | |
create_vsymbol [Term] | |
create_written_attr [Ident] | The vc_written attribute is built during VC generation: it is used to track the location of the creation of variables. |
create_xsymbol [Ity] | |
cty_add_post [Ity] |
|
cty_add_pre [Ity] |
|
cty_apply [Ity] |
|
cty_exec [Ity] |
|
cty_exec_post [Ity] |
|
cty_ghost [Ity] |
|
cty_ghostify [Ity] |
|
cty_pure [Ity] |
|
cty_read_post [Ity] |
|
cty_read_pre [Ity] |
|
cty_reads [Ity] |
|
cty_tuple [Ity] |
|
current_offset [Loc] | |
customize_clean [Model_parser] | Customize the class used to clean the values in the model. |
D | |
d_equal [Decl] | |
d_hash [Decl] | |
datadir [Whyconf] | |
debug [Call_provers] | debug flag for the calling procedure (option "--debug call_prover")
If set |
debug_attrs [Call_provers] | Print attributes in model |
debug_check_ce [Counterexample] | print information about the models returned by the solver and the result of checking them by interpreting the program concretly and abstractly using the values in the solver's model |
debug_force_binary_floats [Model_parser] | Print all floats using bitvectors in JSON output for models |
debug_parse_only [Typing] | |
debug_type_only [Typing] | |
decl [Trans] |
|
decl_fold [Decl.DeclTF] | |
decl_fold [Decl] | |
decl_goal_l [Trans] | FIXME: * make this comment more comprehensible * there should be no "disallowed cases": as soon as a goal is produced, no new decls should be added anymore in the resulting tasks |
decl_l [Trans] |
|
decl_map [Decl.DeclTF] | |
decl_map [Decl] | |
decl_map_fold [Decl.DeclTF] | |
decl_map_fold [Decl] | |
decr [Debug.Stats] | |
default_config [Whyconf] |
|
default_delay_ms [Controller_itp] | Default delay for the scheduler timeout |
default_editor [Whyconf] | editor name used when no specific editor known for a prover |
default_value_of_type [Pinterp] | |
desc_debug [Debug.Args] | Option for specifying a debug flag to set |
desc_debug_all [Debug.Args] | Option for setting all info flags |
desc_debug_list [Debug.Args] | Option for printing the list of debug flags |
desc_shortcut [Debug.Args] | Option for setting a specific flag |
diff [Extset.S] |
|
diff [Extmap.S] |
|
discard_file [Typing] | |
disjoint [Extset.S] |
|
disjoint [Extmap.S] |
|
div [Mlmpfr_wrapper] | |
diverges [Ity] | |
domain [Extmap.S] |
|
dot [Pp] | |
dprintf [Debug] | Print only if the flag is set |
drop_while [Lists] |
|
dummy_position [Loc] | |
dummy_tag [Weakhtbl] | |
duplicate_ident_printer [Ident] | This is used to avoid editing the current (mutable) printer when raising exception or printing information messages for the user. |
E | |
e_absurd [Expr] | |
e_and [Expr] | |
e_app [Expr] | |
e_assert [Expr] | |
e_assign [Expr] | |
e_attr_add [Expr] | |
e_attr_copy [Expr] | |
e_attr_push [Expr] | |
e_attr_set [Expr] | |
e_const [Expr] | |
e_exec [Expr] | |
e_exn [Expr] | |
e_false [Expr] | |
e_fold [Expr] |
|
e_for [Expr] | |
e_func_app [Expr] | |
e_func_app_l [Expr] | |
e_ghost [Expr] | |
e_ghostify [Expr] | |
e_if [Expr] | |
e_let [Expr] | |
e_locate_effect [Expr] |
|
e_match [Expr] | |
e_nat_const [Expr] | |
e_not [Expr] | |
e_or [Expr] | |
e_pur [Expr] | |
e_pure [Expr] | |
e_raise [Expr] | |
e_rs_subst [Expr] | |
e_true [Expr] | |
e_tuple [Expr] | |
e_var [Expr] | |
e_void [Expr] | |
e_while [Expr] | |
eapp [Ptree_helpers] | |
eapply [Ptree_helpers] | |
econst [Ptree_helpers] | |
editor_by_id [Whyconf] | return the configuration of the editor if found, otherwise return Not_found |
eff_assign [Ity] | |
eff_bind [Ity] | |
eff_bind_single [Ity] | |
eff_catch [Ity] | |
eff_diverge [Ity] | |
eff_empty [Ity] | Effect of a non-ghost total function without any observational effect of any kinds |
eff_equal [Ity] | |
eff_escape [Ity] | |
eff_fusion [Ity] | |
eff_ghostify [Ity] | |
eff_ghostify_weak [Ity] | |
eff_partial [Ity] | |
eff_pure [Ity] | |
eff_raise [Ity] | |
eff_read [Ity] | |
eff_read_post [Ity] | |
eff_read_pre [Ity] | |
eff_read_single [Ity] | |
eff_read_single_post [Ity] | |
eff_read_single_pre [Ity] | |
eff_reset [Ity] | |
eff_reset_overwritten [Ity] | |
eff_spoil [Ity] | |
eff_union_par [Ity] | |
eff_union_seq [Ity] | |
eff_write [Ity] | |
elements [Extset.S] | Return the list of all elements of the given set. |
empty [Coercion] | |
empty [Rc] | An empty Rc |
empty [Extset.S] | The empty set. |
empty [Extmap.S] | The empty map. |
empty_formatted [Pp] | |
empty_inst [Theory] | |
empty_limit [Call_provers] | |
empty_log [Pinterp.Log] | |
empty_log_uc [Pinterp.Log] | |
empty_mod_inst [Pmodule] | |
empty_model [Model_parser] | |
empty_ns [Theory] | |
empty_rc [Whyconf] | |
empty_section [Rc] | An empty section |
empty_session [Session_itp] | create an empty_session in the directory specified by the argument. |
end_module [Ptree_helpers.I] | |
end_module [Ptree_helpers.F] | |
ends_with [Strings] | test if a string ends with another |
env_tag [Env] | |
eq [BigInt] | comparisons |
equal [Pp] | |
equal [Loc] | |
equal [Wstdlib.OrderedHashedType] | |
equal [Extset.S] |
|
equal [Extmap.S] |
|
equal [Lists] | |
equal [Opt] | |
equal_p [Mlmpfr_wrapper] | |
error [Loc] | |
errorm [Loc] | |
euclidean_div [BigInt] | |
euclidean_div_mod [BigInt] | Division and modulo operators with the convention that modulo is always non-negative. |
euclidean_mod [BigInt] | |
eval_global_fundef [Pinterp] |
|
eval_rs [Pinterp] |
|
evar [Ptree_helpers] | |
exists [Extset.S] |
|
exists [Extmap.S] |
|
exit_with_usage [Whyconf.Args] | |
exp [Mlmpfr_wrapper] | |
expr [Ptree_helpers] | |
extract [Loc] | |
extract_field [Ident] | Take an attribute and extract its depth, name if it was a field attribute
( |
extract_written_loc [Ident] | Extract the location inside vc_written attribute. |
F | |
fd_of_rs [Expr] | raises |
ffalse [Util] |
|
field [Pinterp] | |
field_get [Pinterp] | |
field_set [Pinterp] | |
file_format [Session_itp] | |
file_id [Session_itp] | File |
file_iter_proof_attempt [Session_itp] | |
file_of_task [Driver] |
|
file_of_theory [Driver] |
|
file_path [Session_itp] | |
file_proved [Session_itp] | |
file_theories [Session_itp] | |
filter [Extset.S] |
|
filter [Extmap.S] |
|
filter_one_prover [Whyconf] | find the uniq prover that verify the filter. |
filter_prover [Whyconf] | test if the prover match the filter prover |
filter_prover_with_shortcut [Whyconf] | resolve prover shortcut in filter |
filter_provers [Whyconf] | Get all the provers that match this filter |
find [Coercion] | returns the coercion, or raises |
find [Weakhtbl.S] | |
find [Exthtbl.Private] | Same as |
find [Extmap.S] |
|
find_clone_tds [Task] | |
find_constructors [Decl] | |
find_def [Exthtbl.Private] | return the first binding or the given value if none found |
find_def [Exthtbl.S] | return the first binding or the given value if none found |
find_def [Extmap.S] |
|
find_exn [Exthtbl.Private] | return the first binding or raise the given exception if none found |
find_exn [Exthtbl.S] | return the first binding or raise the given exception if none found |
find_exn [Extmap.S] |
|
find_file_from_path [Session_itp] | raise |
find_inductive_cases [Decl] | |
find_its_defn [Pdecl] | |
find_logic_definition [Decl] | |
find_meta_tds [Task] | |
find_nth [Lists] |
|
find_opt [Exthtbl.Private] | return the first binding or None if none found |
find_opt [Exthtbl.S] | return the first binding or None if none found |
find_opt [Extmap.S] |
|
find_prop [Decl] | |
find_prop_decl [Decl] | |
find_symbol [Args_wrapper] | |
find_th [Session_itp] | |
find_variant [Decl] | |
first [Lists] |
|
first_arg [Whyconf.Args] | |
first_nth [Lists] | The combinaison of |
flag_desc [Debug] | get the description of the flag |
flatten_rev [Lists] | |
flip [Util] | |
float [Pp] | |
float_of_binary [Model_parser] | |
fma [Mlmpfr_wrapper] | |
focus_on_loading [Itp_server.Make] | |
fold [Trans] | Iterating transformations |
fold [Weakhtbl.S] | |
fold [Exthtbl.Private] | Same as |
fold [Extset.S] |
|
fold [Extmap.S] |
|
fold [Opt] |
|
fold2_inter [Extset.S] |
|
fold2_inter [Extmap.S] | fold the common keys of two map at the same time |
fold2_union [Extset.S] |
|
fold2_union [Extmap.S] | fold the keys which appear in one of the two maps |
fold_all_any [Session_itp] |
|
fold_all_session [Session_itp] |
|
fold_decl [Trans] | |
fold_l [Trans] | |
fold_left [Extset.S] | same as |
fold_left [Extmap.S] | same as |
fold_lefti [Lists] | similar to List.map, List.iter and List.fold_left, but with element index passed as extra argument (in 0..len-1) |
fold_map [Trans] | |
fold_map_l [Trans] | |
fold_product [Lists] |
|
fold_product_l [Lists] | generalisation of |
fold_right [Opt] | |
foldi [Util] | |
foldk [Weakhtbl.S] | |
for_all [Extset.S] |
|
for_all [Extmap.S] |
|
forget_all [Pretty.Printer] | |
forget_all [Ident] | forget all idents |
forget_cty [Ity] | |
forget_id [Ident] | forget an ident |
forget_pv [Ity] | |
forget_reg [Ity] | |
forget_rs [Expr] | |
forget_tvs [Pretty.Printer] | |
forget_var [Pretty.Printer] | |
forget_xs [Ity] | |
format [Getopt] |
|
formatted [Pp] | |
fprintf_any [Session_itp] | |
from_channel [Rc] |
|
from_file [Rc] |
|
fs_app [Term] | |
fs_bool_false [Term] | |
fs_bool_true [Term] | |
fs_func_app [Term] | |
fs_tuple [Term] | |
fs_void [Expr] | |
full_support [Number] | |
funlit [Ident] | |
G | |
ge [BigInt] | |
gen_report_position [Loc] | |
gen_syntax_arguments_prec [Printer] | |
get [Loc] | |
get [Opt] | |
get_any_parent [Session_itp] | |
get_bool [Rc] | Same as |
get_booll [Rc] | Same as |
get_boolo [Rc] | |
get_complete_command [Whyconf] | add the extra_options to the command |
get_conf_file [Whyconf] |
|
get_debug_formatter [Debug] | Get the formatter used when printing debug material |
get_decl_syms [Decl] | |
get_def [Opt] | |
get_default_printer_mapping [Printer] | |
get_dir [Session_itp] | |
get_editors [Whyconf] | returns the set of editors |
get_element_name [Ident] | |
get_element_syntax [Pretty] | |
get_encapsulating_file [Session_itp] | |
get_encapsulating_theory [Session_itp] | |
get_exn [Opt] | |
get_family [Whyconf.User] |
|
get_family [Rc] |
|
get_files [Session_itp] | |
get_format [Env] |
|
get_formatted_str [Mlmpfr_wrapper] | |
get_home_dir [Rc] |
|
get_hyp_name [Ident] | If attrs contains an attribute of the form |
get_int [Rc] |
|
get_intl [Rc] |
|
get_into [Rc] | |
get_loadpath [Env] | returns the loadpath of a given environment |
get_main [Whyconf] |
|
get_mlw_file [Ptree_helpers.I] | |
get_mlw_file [Ptree_helpers.F] | |
get_model_element [Model_parser] | |
get_model_element_by_id [Model_parser] | |
get_model_element_by_loc [Model_parser] | |
get_model_element_name [Ident] | If attributes contain an attribute of the form |
get_model_elements [Model_parser] | |
get_model_term_attrs [Model_parser] | |
get_model_term_loc [Model_parser] | |
get_model_trace_attr [Ident] | Return an attribute of the form |
get_model_trace_string [Ident] | If attrs contain an attribute of the form |
get_multiline [Loc] | Returns |
get_namespace [Theory] | |
get_new_results [Call_provers] | returns new results from why3server, in an unordered fashion. |
get_policies [Whyconf] | |
get_proof_attempt_ids [Session_itp] | |
get_proof_attempt_node [Session_itp] | |
get_proof_attempt_parent [Session_itp] | |
get_proof_attempts [Session_itp] | |
get_proof_expl [Session_itp] | |
get_proof_name [Session_itp] | |
get_proof_parent [Session_itp] | |
get_prover_config [Whyconf] |
|
get_prover_shortcuts [Whyconf] | return the prover shortcuts |
get_prover_upgrade_policy [Whyconf] |
|
get_provers [Whyconf] |
|
get_requests [Itp_server.Protocol] | |
get_rliteral_map [Printer] | |
get_section [Whyconf.User] |
|
get_section [Rc] |
|
get_simple_family [Whyconf.User] |
|
get_simple_family [Rc] |
|
get_strategies [Whyconf] | |
get_string [Rc] | Same as |
get_stringl [Rc] | Same as |
get_stringo [Rc] | |
get_sub_tasks [Session_itp] | |
get_syntax_map [Printer] | |
get_task [Session_itp] | |
get_task_name_table [Session_itp] | |
get_trans_parent [Session_itp] | |
get_transf_args [Session_itp] | |
get_transf_name [Session_itp] | |
get_transformations [Session_itp] | |
get_undetached_children_no_pa [Controller_itp] | |
goal [Trans] | |
goal_iter_proof_attempt [Session_itp] | |
goal_l [Trans] | |
graft_proof_attempt [Session_itp] |
|
graft_transf [Session_itp] |
|
greater_p [Mlmpfr_wrapper] | |
greaterequal_p [Mlmpfr_wrapper] | |
gt [BigInt] | |
H | |
handle_exn [Getopt] |
|
has_a_model_attr [Ident] |
|
has_prefix [Strings] |
|
has_suffix [Strings] |
|
hash [Loc] | |
hash [Wstdlib.OrderedHashedType] | |
hash [Exthtbl] | the same as Hashtbl.hash |
highord_module [Pmodule] | |
highord_theory [Theory] | |
hov [Pp] | |
hterm_generic [Term] | |
html_char [Pp] | |
html_string [Pp] | formats the string by escaping special HTML characters quote, double quote, <, > and & |
I | |
id_attr [Ident] | create a duplicate pre-ident with given attributes |
id_clone [Ident] | create a duplicate pre-ident |
id_compare [Ident] | |
id_derive [Ident] | create a derived pre-ident (inherit attributes and location) |
id_equal [Ident] | |
id_fresh [Ident] | create a fresh pre-ident |
id_hash [Ident] | |
id_register [Ident] | register a pre-ident (you should never use this function) |
id_unique [Ident] | use ident_printer to generate a unique name for ident an optional sanitizer is applied over the printer's sanitizer |
id_unique_attr [Ident] | Do the same as id_unique except that it tries first to use the "name:" attribute to generate the name instead of id.id_string |
id_user [Ident] | create a localized pre-ident |
ident [Ptree_helpers] |
|
identity [Trans] | |
identity_l [Trans] | |
idle [Controller_itp.Scheduler] |
|
import_namespace [Theory] | |
import_scope [Pmodule] | |
import_scope [Theory] | |
incr [Debug.Stats] | |
indent [Pp] | add the indentation at the first line |
inf_p [Mlmpfr_wrapper] | |
inhabited [Opt] | |
init [Lists] | |
init_config [Whyconf] |
|
init_real [Pinterp] | Give a precision on real computation. |
init_server [Itp_server.Make] | |
initialize [Whyconf.Args] | |
int [Pp] | |
int_literal [Number] | |
int_value [Pinterp] | |
inter [Extset.S] |
|
inter [Extmap.S] |
|
interleave_with_source [Model_parser] | Given a source code and a counter-example model interleaves the source code with information in about the counter-example. |
interrupt [Controller_itp.Make] | discards all scheduled proof attempts or transformations, including the ones already running |
interrupt_call [Call_provers] | non-blocking function that asks for prover interruption |
is_alias_type_def [Ty] | |
is_below [Session_itp] | |
is_detached [Session_itp] | |
is_e_false [Expr] | |
is_e_true [Expr] | |
is_e_void [Expr] | |
is_empty [Exthtbl.Private] | test if the hashtbl is empty |
is_empty [Exthtbl.S] | test if the hashtbl is empty |
is_empty [Extset.S] | Test whether a set is empty or not. |
is_empty [Extmap.S] | Test whether a map is empty or not. |
is_fatal [Session_itp] | |
is_float_type_def [Ty] | |
is_fs_tuple [Term] | |
is_fs_tuple_id [Term] | |
is_info_flag [Debug] | test if the flag is an info flag |
is_int [BigInt] | |
is_model_empty [Model_parser] | |
is_model_trace_attr [Ident] | |
is_num_elt [Extset.S] | check if the map has the given number of elements |
is_num_elt [Extmap.S] | check if the map has the given number of elements |
is_prover_known [Whyconf] | test if a prover is detected |
is_range_type_def [Ty] | |
is_root [Itp_communication] | |
is_rs_tuple [Expr] | |
is_sexp_simple_token [Util] | Check if a non-empty string contains only characters |
is_ts_tuple [Ty] | |
is_ts_tuple_id [Ty] | |
isb_empty [Ity] | |
iter [Weakhtbl.S] | |
iter [Exthtbl.Private] | Same as |
iter [Extset.S] |
|
iter [Extmap.S] |
|
iter [Opt] | |
iterf [Util] |
|
iteri [Lists] | |
iterk [Weakhtbl.S] | |
its_bool [Ity] | |
its_compare [Ity] | |
its_equal [Ity] | |
its_func [Ity] | |
its_hash [Ity] | |
its_int [Ity] | |
its_match_args [Ity] | |
its_match_regs [Ity] | |
its_pure [Ity] | a pure type symbol is immutable and has no mutable components |
its_real [Ity] | |
its_ref [Pmodule] | |
its_str [Ity] | |
its_tuple [Ity] | |
its_unit [Ity] | |
ity_affected [Ity] |
|
ity_app [Ity] |
|
ity_app_pure [Ity] |
|
ity_bool [Ity] | |
ity_closed [Ity] | a closed type contains no type variables |
ity_compare [Ity] | |
ity_equal [Ity] | |
ity_equal_check [Ity] | |
ity_exp_fold [Ity] | |
ity_fold [Ity] | |
ity_fragile [Ity] | a fragile type may contain a component with a broken invariant |
ity_freeregs [Ity] | |
ity_freevars [Ity] | |
ity_freeze [Ity] | |
ity_frz_regs [Ity] | |
ity_full_inst [Ity] | |
ity_func [Ity] | |
ity_hash [Ity] | |
ity_int [Ity] | |
ity_match [Ity] | |
ity_of_ty [Ity] | fresh regions are created when needed. |
ity_of_ty_pure [Ity] | pure snapshots are substituted when needed. |
ity_pred [Ity] | |
ity_purify [Ity] | replaces regions with pure snapshots |
ity_r_fold [Ity] | |
ity_r_occurs [Ity] | |
ity_r_reachable [Ity] | |
ity_r_stale [Ity] | |
ity_rch_fold [Ity] | |
ity_real [Ity] | |
ity_reg [Ity] | |
ity_s_fold [Ity] | |
ity_str [Ity] | |
ity_tuple [Ity] | |
ity_unit [Ity] | |
ity_v_fold [Ity] | |
ity_v_occurs [Ity] | |
ity_var [Ity] | |
J | |
join [Loc] | |
join [Strings] |
|
K | |
keys [Extmap.S] | Return the list of all keys of the given map. |
known_add_decl [Pdecl] | |
known_add_decl [Decl] | |
known_id [Pdecl] | |
known_id [Decl] | |
known_id [Ident] | Returns true if the printer already knows the id. |
kp_attr [Vc] | |
L | |
lbrace [Pp] | |
lchevron [Pp] | |
ld_func_app [Expr] | |
le [BigInt] | |
length [Weakhtbl.S] | |
length [Exthtbl.Private] | Same as |
less_p [Mlmpfr_wrapper] | |
lessequal_p [Mlmpfr_wrapper] | |
lessgreater_p [Mlmpfr_wrapper] | |
let_rec [Expr] | |
let_sym [Expr] | |
let_var [Expr] | |
libdir [Whyconf] | |
limit_max [Call_provers] | |
list_attributes [Ident] | |
list_flags [Debug] | list the known flags |
list_formats [Env] |
|
list_map_cont [Term] | |
list_metas [Theory] | |
list_model_parsers [Model_parser] | |
list_printers [Printer] | |
list_projs [Printer] | Return the union of projections and fields of a printer_mapping |
list_trans [Trans] | |
list_transforms [Trans] | |
list_transforms_l [Trans] | |
list_transforms_with_args [Trans] | |
list_transforms_with_args_l [Trans] | |
load_driver [Whyconf] |
|
load_driver_absolute [Driver] |
|
load_driver_raw [Whyconf] |
|
load_plugins [Whyconf] | |
load_session [Session_itp] |
|
loadpath [Whyconf] | |
local_decls [Task] | takes the result of |
locate_library [Env] |
|
log [Mlmpfr_wrapper] | |
log_any_call [Pinterp.Log] | |
log_call [Pinterp.Log] | |
log_const [Pinterp.Log] | |
log_exec_ended [Pinterp.Log] | |
log_exec_main [Pinterp.Log] | |
log_failed [Pinterp.Log] | |
log_iter_loop [Pinterp.Log] | |
log_pure_call [Pinterp.Log] | |
log_stucked [Pinterp.Log] | |
log_val [Pinterp.Log] | |
lookup_flag [Debug] | get the flag |
lookup_meta [Theory] | |
lookup_model_parser [Model_parser] | |
lookup_printer [Printer] | |
lookup_trans [Trans] | |
lookup_trans_desc [Trans] | |
lookup_transform [Trans] | |
lookup_transform_l [Trans] | |
lowercase [Strings] | |
lparen [Pp] | |
ls_app_inst [Term] | |
ls_arg_inst [Term] | |
ls_compare [Term] | |
ls_decr_of_rec_defn [Expr] | |
ls_defn_axiom [Decl] | |
ls_defn_decrease [Decl] |
|
ls_defn_of_axiom [Decl] | tries to reconstruct a definition from a defining axiom. |
ls_equal [Term] | |
ls_hash [Term] | |
ls_of_rs [Expr] | raises |
ls_ref_cons [Pmodule] | |
ls_ref_proj [Pmodule] | |
ls_ty_freevars [Term] | |
lsquare [Pp] | |
lt [BigInt] | |
M | |
make_from_int [Mlmpfr_wrapper] | |
make_from_str [Mlmpfr_wrapper] | |
make_ls_defn [Decl] | |
make_record [Decl] | |
make_record_pattern [Decl] | |
make_record_update [Decl] | |
make_zero [Mlmpfr_wrapper] | |
map [Exthtbl.Private] | a shortcut less efficient than possible |
map [Exthtbl.S] | a shortcut less efficient than possible |
map [Extmap.S] |
|
map [Opt] | |
map2 [Opt] | |
map_filter [Extmap.S] | Same as |
map_filter [Lists] | |
map_filter_model_elements [Model_parser] | |
map_fold [Opt] | |
map_fold_left [Lists] | |
map_fold_right [Lists] | |
map_join_left [Lists] | |
mapi [Extmap.S] | Same as |
mapi [Lists] | |
mapi [Util] | |
mapi_filter [Extmap.S] | Same as |
mapi_filter_fold [Extmap.S] | Same as |
mapi_fold [Extmap.S] | fold and map at the same time |
mark_as_obsolete [Controller_itp.Make] | |
mark_obsolete [Session_itp] |
|
mask_adjust [Ity] | |
mask_equal [Ity] | |
mask_ghost [Ity] | |
mask_of_pv [Ity] | |
mask_spill [Ity] | |
mask_union [Ity] | |
max [Mlmpfr_wrapper] | |
max [BigInt] | |
max_binding [Extmap.S] | Same as |
max_elt [Extset.S] | Return the largest element of the given set or raise
|
mem [Weakhtbl.S] | |
mem [Exthtbl.Private] | Same as |
mem [Extset.S] |
|
mem [Extmap.S] |
|
memlimit [Whyconf] | |
memo [Exthtbl.S] | convenience function, memoize a function |
memoize [Weakhtbl.S] | |
memoize_option [Weakhtbl.S] | |
memoize_rec [Weakhtbl.S] | |
merge [Extset.S] |
|
merge [Extmap.S] |
|
merge_files [Session_itp] |
|
merge_known [Pdecl] | |
merge_known [Decl] | |
meta_coercion [Theory] | |
meta_equal [Theory] | |
meta_float [Theory] | |
meta_hash [Theory] | |
meta_projection [Theory] | |
meta_range [Theory] | |
meta_realized_theory [Printer] | |
meta_record [Theory] | |
meta_remove_logic [Printer] | |
meta_remove_prop [Printer] | |
meta_remove_type [Printer] | |
meta_syntax_literal [Printer] | |
meta_syntax_logic [Printer] | |
meta_syntax_type [Printer] | |
min [Mlmpfr_wrapper] | |
min [BigInt] | min, max, abs |
min_binding [Extmap.S] | Return the smallest binding of the given map
(with respect to the |
min_elt [Extset.S] | Return the smallest element of the given set or raise
|
minus [BigInt] | |
mk_filter_prover [Whyconf] | |
mk_proxy_decl [Expr] |
|
mk_tds [Task] | |
mlw_language [Pmodule] | |
mlw_language_builtin [Pmodule] | |
mod0 [Debug.Stats] | |
mod1 [Debug.Stats] | |
mod2 [Debug.Stats] | |
model_for_positions_and_decls [Model_parser] | Given a model and a list of source-code positions returns model that contains only elements from the input model that are on these positions plus for every file in the model, elements that are in the positions of function declarations. |
model_of_exec_log [Counterexample] |
|
model_projected_attr [Ident] | |
model_vc_post_attr [Ident] | |
mterm_generic [Term] | |
mul [Mlmpfr_wrapper] | |
mul [BigInt] | |
mul_int [BigInt] | |
multiplier [Controller_itp.Scheduler] | Number of allowed task given to why3server is this number times the number of allowed proc on the machine. |
N | |
named [Trans] | give transformation a name without registering |
nan_p [Mlmpfr_wrapper] | |
neg [Mlmpfr_wrapper] | |
neg_int [Number] | |
neg_real [Number] | |
newline [Pp] | |
newline2 [Pp] | |
next_enum [Extmap.S] | get the next step of the enumeration |
next_ge_enum [Extmap.S] | get the next (or same) step of the enumeration which key is greater or equal to the given key |
next_pos [Mlw_printer] | Generate a unique location. |
notImplemented [Printer] | |
nothing [Pp] | |
notify [Itp_server.Protocol] | |
ns_find_its [Pmodule] | |
ns_find_ls [Theory] | |
ns_find_ns [Pmodule] | |
ns_find_ns [Theory] | |
ns_find_pr [Theory] | |
ns_find_prog_symbol [Pmodule] | |
ns_find_pv [Pmodule] | |
ns_find_rs [Pmodule] | |
ns_find_ts [Theory] | |
ns_find_xs [Pmodule] | |
nt_attr [Vc] | |
num_digits [BigInt] | number of digits |
O | |
of_int [BigInt] | |
of_list [Extset.S] | construct a set from a list of elements |
of_list [Extmap.S] | construct a map from a list of bindings. |
of_string [BigInt] | conversions |
on_cloned_theory [Trans] | |
on_cloned_theory [Task] | |
on_flag [Trans] |
|
on_flag_t [Trans] | |
on_meta [Trans] | |
on_meta [Task] | |
on_meta_excl [Trans] | |
on_meta_excl [Task] | |
on_syntax_map [Printer] | |
on_tagged_ls [Trans] | |
on_tagged_ls [Task] | |
on_tagged_pr [Trans] | |
on_tagged_pr [Task] | |
on_tagged_ts [Trans] | |
on_tagged_ts [Task] | |
on_tagged_ty [Trans] |
|
on_tagged_ty [Task] | |
on_used_theory [Trans] | |
on_used_theory [Task] | |
one [BigInt] | |
one_binder [Ptree_helpers] | |
op_cut [Ident] | |
op_equ [Ident] | |
op_get [Ident] | |
op_infix [Ident] | |
op_lcut [Ident] | |
op_neq [Ident] | |
op_prefix [Ident] | |
op_rcut [Ident] | |
op_set [Ident] | |
op_tight [Ident] | |
op_update [Ident] | |
open_file [Typing] | |
open_file_and_formatter [Pp] | |
open_formatter [Pp] | |
open_ls_defn [Decl] | |
open_ls_defn_cb [Decl] | |
open_module [Typing] | |
open_post [Ity] | |
open_post_with [Ity] | |
open_scope [Pmodule] | |
open_scope [Typing] | |
open_scope [Theory] | |
opt_config [Whyconf.Args] | |
option_list [Debug.Args] | Print the list of flags if requested (in this case return |
oty_compare [Ty] | |
oty_cons [Ty] | |
oty_equal [Ty] | |
oty_freevars [Ty] | |
oty_hash [Ty] | |
oty_inst [Ty] | |
oty_match [Ty] | |
oty_type [Ty] | |
overload_of_rs [Pmodule] | |
P | |
pa_proved [Session_itp] | |
pad_right [Strings] | chop or pad the given string on the right up to the given length |
par [Trans] | parallelize transformations: |
parse_all [Getopt] |
|
parse_filter_prover [Whyconf] | parse the string representing a filter_prover: "name,version,altern", "name,version" -> "name,version,^.*", "name,,altern" -> "name,^.*,altern", "name" -> "name,^.*,^.*" regexp must start with ^. |
parse_many [Getopt] |
|
parse_one [Getopt] |
|
parse_record [Decl] |
|
part [Lists] |
|
partial [Ity] | |
partition [Extset.S] |
|
partition [Extmap.S] |
|
pat [Ptree_helpers] | |
pat_all [Term] | |
pat_any [Term] | |
pat_app [Term] | |
pat_as [Term] | |
pat_fold [Term] | |
pat_map [Term] | |
pat_or [Term] | |
pat_var [Ptree_helpers] | |
pat_var [Term] | |
pat_wild [Term] | |
pd_bool [Pdecl] | |
pd_equ [Pdecl] | |
pd_func [Pdecl] | |
pd_func_app [Pdecl] | |
pd_int [Pdecl] | |
pd_real [Pdecl] | |
pd_str [Pdecl] | |
pd_tuple [Pdecl] | |
plugins [Whyconf] | |
pluginsdir [Whyconf] | |
pn_proved [Session_itp] | |
post_of_expr [Expr] | |
pow_int_pos [BigInt] | power of small integers. |
pow_int_pos_bigint [BigInt] | |
pp_decl [Mlw_printer] | Printer for declarations |
pp_expr [Mlw_printer] | Printer for expressions |
pp_mlw_file [Mlw_printer] | Printer for mlw files |
pp_pattern [Mlw_printer] | Printer for patterns |
pp_pty [Mlw_printer] | Printer for types |
pp_term [Mlw_printer] | Printer for terms |
pprinter [Pretty.Printer] | |
pr_equal [Decl] | |
pr_hash [Decl] | |
pred [BigInt] | |
prefix [Lists] | the first n elements of a list |
preid_name [Ident] | |
prepare_edition [Controller_itp.Make] |
|
prepare_task [Driver] | |
print [Debug.Stats] | |
print [Extset.S] | |
print0 [Pp] | |
print_attr [Pretty.Printer] | |
print_attrs [Pretty.Printer] | |
print_binop [Pretty.Printer] | |
print_ce_summary_kind [Counterexample] | |
print_ce_summary_title [Counterexample] | |
print_cexp [Expr] | |
print_check_model_result [Counterexample] | |
print_counterexample [Counterexample] | Print a counterexample. |
print_cs [Pretty.Printer] | |
print_cs_qualified [Pretty.Printer] | |
print_cty [Ity] | |
print_data_decl [Pretty.Printer] | |
print_decl [Pretty.Printer] | |
print_decoded [Ident] | |
print_expr [Expr] | |
print_filter_prover [Whyconf] | |
print_id_attrs [Pretty.Printer] | |
print_in_base [Number] |
|
print_in_file [Pp] | |
print_in_file_no_close [Pp] | |
print_ind_decl [Pretty.Printer] | |
print_int_constant [Number] | |
print_interface [Printer] | |
print_iter1 [Pp] | |
print_iter2 [Pp] |
|
print_iter22 [Pp] |
|
print_its [Ity] | |
print_ity [Ity] | |
print_ity_full [Ity] | |
print_json_loc [Pretty.Printer] | |
print_let_defn [Expr] | |
print_list [Pp] | |
print_list_delim [Pp] | |
print_list_next [Pp] | |
print_list_opt [Pp] | |
print_list_or_default [Pp] | |
print_list_par [Pp] | |
print_list_pre [Pp] | |
print_list_suf [Pp] | |
print_loc [Pretty.Printer] | |
print_loc' [Pretty.Printer] | |
print_log [Pinterp.Log] | |
print_logic_decl [Pretty.Printer] | |
print_ls [Pretty.Printer] | |
print_ls_qualified [Pretty.Printer] | |
print_meta [Trans] |
|
print_meta_arg [Pretty.Printer] | |
print_meta_arg_type [Pretty.Printer] | |
print_meta_desc [Theory] | |
print_model [Model_parser] | Prints the counter-example model |
print_model_human [Model_parser] | Same as print_model but is intended to be human readable. |
print_model_json [Model_parser] | Prints counter-example model to json format. |
print_model_value [Model_parser] | |
print_module [Pmodule] | |
print_msg [Itp_communication] | |
print_namespace [Pretty.Printer] | |
print_next_data_decl [Pretty.Printer] | |
print_next_ind_decl [Pretty.Printer] | |
print_next_logic_decl [Pretty.Printer] | |
print_notify [Itp_communication] | |
print_option [Pp] | |
print_option_or_default [Pp] | |
print_pair [Pp] | |
print_pair_delim [Pp] |
|
print_param_decl [Pretty.Printer] | |
print_pat [Pretty.Printer] | |
print_pdecl [Pdecl] | |
print_pkind [Pretty.Printer] | |
print_pr [Pretty.Printer] | |
print_pr_qualified [Pretty.Printer] | |
print_prelude [Printer] | |
print_proofAttemptID [Session_itp] | |
print_proofNodeID [Session_itp] | |
print_prop_decl [Pretty.Printer] | |
print_prover [Whyconf] | |
print_prover_answer [Call_provers] | Pretty-print a |
print_prover_parseable_format [Whyconf] | |
print_prover_result [Call_provers] | Pretty-print a prover_result. |
print_prover_upgrade_policy [Whyconf] | |
print_pv [Ity] | |
print_pvty [Ity] | |
print_qualid [Typing] | |
print_quant [Pretty.Printer] | |
print_real_constant [Number] | |
print_reg [Ity] | |
print_reg_name [Ity] | |
print_request [Itp_communication] | |
print_rs [Expr] | |
print_sequent [Pretty.Printer] | |
print_session [Controller_itp] | |
print_spec [Ity] | |
print_status [Controller_itp] | |
print_strategy_status [Controller_itp] | |
print_task [Driver] | |
print_task [Pretty.Printer] | |
print_task_prepared [Driver] | |
print_tdecl [Pretty.Printer] | |
print_term [Pretty.Printer] | |
print_th [Pretty.Printer] | |
print_th_prelude [Printer] | |
print_th_qualified [Pretty.Printer] | |
print_theory [Driver] | produce a realization of the given theory using the given driver |
print_theory [Pretty.Printer] | |
print_trans_status [Controller_itp] | |
print_ts [Pretty.Printer] | |
print_ts_qualified [Pretty.Printer] | |
print_tv [Pretty.Printer] | |
print_ty [Pretty.Printer] | |
print_ty_decl [Pretty.Printer] | |
print_ty_qualified [Pretty.Printer] | |
print_unit [Pmodule] | |
print_value [Pinterp] | |
print_vs [Pretty.Printer] | |
print_vsty [Pretty.Printer] | |
print_xs [Ity] | |
prio_binop [Pretty] | |
prioritize_first_good_model [Counterexample] | If there is any model that can be verified by counterexample checking, prioritize NCCE over SWCE over NCCE_SWCE, and prioritize simpler models from the incremental list produced by the prover. |
prioritize_last_non_empty_model [Counterexample] | Do not consider the result of checking the counterexample model, but just priotize the last, non-empty model in the incremental list of models. |
proj_value [Pinterp] | |
protect_on [Pretty] | |
prove_task [Driver] | |
prove_task_prepared [Driver] | |
prover_parseable_format [Whyconf] | |
provers_from_detected_provers [Whyconf] | |
proxy_attr [Ident] | |
ps_app [Term] | |
ps_equ [Term] | equality predicate |
purefun_value [Pinterp] | |
pv_affected [Ity] |
|
pv_compare [Ity] | |
pv_equal [Ity] | |
pv_hash [Ity] | |
pvs_affected [Ity] |
|
pvs_of_vss [Ity] | |
Q | |
qualid [Ptree_helpers] |
|
query_call [Call_provers] | non-blocking function that reports any new updates from the server related to a given prover call. |
query_syntax [Printer] | |
R | |
rac_config [Pinterp] | |
rac_prover [Pinterp] | |
rac_reduce_config [Pinterp] | |
rac_reduce_config_lit [Pinterp] |
|
range_value [Pinterp] | |
rbrace [Pp] | |
rc_of_config [Whyconf] | |
rchevron [Pp] | |
read_channel [Env] |
|
read_config [Whyconf] |
|
read_config_rc [Whyconf] |
|
read_file [Session_itp] | |
read_file [Env] | an open-close wrapper around |
read_library [Env] |
|
read_module [Pmodule] | |
read_theory [Env] |
|
real_literal [Number] |
|
real_value [Number] |
|
ref_attr [Pmodule] | |
ref_module [Pmodule] | |
reg_compare [Ity] | |
reg_equal [Ity] | |
reg_equal_check [Ity] | |
reg_exp_fold [Ity] | |
reg_fold [Ity] | |
reg_freeregs [Ity] | |
reg_freevars [Ity] | |
reg_freeze [Ity] | |
reg_full_inst [Ity] | |
reg_hash [Ity] | |
reg_match [Ity] | |
reg_r_fold [Ity] | |
reg_r_occurs [Ity] | |
reg_r_reachable [Ity] | |
reg_r_stale [Ity] | |
reg_rch_fold [Ity] | |
reg_s_fold [Ity] | |
reg_v_fold [Ity] | |
reg_v_occurs [Ity] | |
register [Debug.Stats] | |
register_call [Decl] | |
register_env_transform [Trans] | |
register_env_transform_l [Trans] | |
register_flag [Debug] | register a new flag. |
register_format [Env] |
|
register_info_flag [Debug] | register a new info flag. |
register_int [Debug.Stats] | |
register_language [Env] |
|
register_meta [Theory] | |
register_meta_excl [Theory] | With exclusive metas, each new meta cancels the previous one. |
register_model_parser [Model_parser] | |
register_observer [Controller_itp.Make] | records a hook that will be called with the number of waiting tasks, scheduled tasks, and running tasks, each time these numbers change |
register_printer [Printer] | |
register_remove_field [Model_parser] | |
register_transform [Trans] | |
register_transform_l [Trans] | |
register_transform_with_args [Trans] | |
register_transform_with_args_l [Trans] | |
relevant_for_counterexample [Ident] |
|
reload_files [Controller_itp] |
|
reloc [Loc] | |
remove [Weakhtbl.S] | |
remove [Extset.S] |
|
remove [Extmap.S] |
|
remove_left [Extset.S] |
|
remove_model_attrs [Ident] | Remove the counter-example attributes from an attribute set |
remove_prefix [Strings] |
|
remove_proof_attempt [Session_itp] |
|
remove_prop [Printer] | |
remove_subtree [Controller_itp] | remove a subtree of the session, taking care of not removing any proof attempt in progress. |
remove_subtree [Session_itp] |
|
remove_suffix [Strings] |
|
remove_transformation [Session_itp] |
|
remove_user_policy [Whyconf.User] | |
rename_file [Session_itp] |
|
replace [Extmap.S] |
|
replay [Controller_itp.Make] | This function reruns all the proofs of the session under the given any (None means the whole session), and produces a report comparing the results with the former ones. |
replay_print [Controller_itp.Make] | |
report_cntr [Pinterp] | |
report_cntr_body [Pinterp] | Report a contradiction context and term |
report_eval_result [Pinterp] | Report an evaluation result |
report_position [Loc] | |
reset_proofs [Controller_itp.Make] | Remove each proof attempt or transformation that are below proved goals. |
restore_its [Ity] | raises |
restore_module [Pmodule] | retrieves a module from its underlying theory
raises |
restore_module_id [Pmodule] | retrieves a module from a program symbol defined in it Raises Not_found if the ident was never declared in/as a module. |
restore_path [Pmodule] |
|
restore_path [Theory] |
|
restore_pv [Ity] | raises |
restore_rs [Expr] | raises |
restore_theory [Theory] | |
result_id [Ity] |
|
return [Trans] | |
rev_filter [Lists] | |
rev_map_fold_left [Lists] | |
rev_split [Strings] | |
rewrite [Trans] |
|
rewriteTF [Trans] | |
rint [Mlmpfr_wrapper] | |
root_node [Itp_communication] | |
rparen [Pp] | |
rs_compare [Expr] | |
rs_equal [Expr] | |
rs_false [Expr] | |
rs_func_app [Expr] | |
rs_ghost [Expr] | |
rs_hash [Expr] | |
rs_kind [Expr] | |
rs_ref [Pmodule] | |
rs_ref_cons [Pmodule] | |
rs_ref_proj [Pmodule] | |
rs_true [Expr] | |
rs_tuple [Expr] | |
rs_void [Expr] | |
rsquare [Pp] | |
run_strategy_on_goal [Controller_itp.Make] |
|
running_provers_max [Whyconf] | |
S | |
sanitizer [Ident] | generic sanitizer taking a separate encoder for the first letter |
sanitizer' [Ident] | generic sanitizer taking a separate encoder for the first and last letter |
save_config [Whyconf] |
|
save_session [Session_itp] |
|
schedule_edition [Controller_itp.Make] |
|
schedule_proof_attempt [Controller_itp.Make] |
|
schedule_transformation [Controller_itp.Make] |
|
select_model [Counterexample] |
|
select_model_last_non_empty [Counterexample] | Select the last, non-empty model in the incremental list of models as done before 2020. |
semi [Pp] | |
seq [Trans] | |
seq_l [Trans] | |
session_iter_proof_attempt [Session_itp] | |
set [Weakhtbl.S] | |
set_argument_parsing_functions [Args_wrapper] | |
set_bool [Rc] | Same as |
set_booll [Rc] | Same as |
set_boolo [Rc] | Same as |
set_column [Pp.Ansi] | |
set_compare [Extmap.S] |
|
set_debug_formatter [Debug] | Set the formatter used when printing debug material |
set_default_editor [Whyconf.User] | |
set_default_editor [Whyconf] | |
set_default_prec [Mlmpfr_wrapper] | |
set_diff [Extmap.S] |
|
set_disjoint [Extmap.S] |
|
set_editors [Whyconf] | replace the set of editors |
set_emax [Mlmpfr_wrapper] | |
set_emin [Mlmpfr_wrapper] | |
set_equal [Extmap.S] |
|
set_family [Whyconf.User] |
|
set_family [Rc] |
|
set_file [Loc] | |
set_flag [Debug] | Modify the state of a flag |
set_flags_selected [Debug.Args] | Set the flags selected by debug_all, debug or a shortcut. |
set_infer_invs [Vc] | |
set_int [Rc] |
|
set_inter [Extmap.S] |
|
set_intl [Rc] |
|
set_into [Rc] |
|
set_limits [Whyconf.User] | |
set_limits [Whyconf] | |
set_load_default_plugins [Whyconf] | Set if the plugins in the default path should be loaded |
set_loadpath [Whyconf] | |
set_main [Whyconf] |
|
set_model_files [Model_parser] | |
set_partial_config [Itp_server] | |
set_partial_config [Controller_itp] | edit a minimal part of the configuration that should be safe to edit during execution of the server (provers config, editors) |
set_plugins [Whyconf] | |
set_policies [Whyconf] | |
set_proof_script [Session_itp] | |
set_prover_shortcuts [Whyconf] | set the prover shortcuts |
set_prover_upgrade_policy [Whyconf.User] | |
set_prover_upgrade_policy [Whyconf] |
|
set_provers [Whyconf] |
|
set_section [Whyconf.User] |
|
set_section [Rc] |
|
set_session_max_tasks [Controller_itp] | sets the maximum number of proof tasks that can be running at the same time. |
set_session_memlimit [Controller_itp] | sets the default memlimit for proof attempts |
set_session_prover_upgrade_policy [Controller_itp] | |
set_session_timelimit [Controller_itp] | sets the default timelimit for proof attempts |
set_simple_family [Whyconf.User] |
|
set_simple_family [Rc] |
|
set_stdlib [Whyconf] | Set if the standard library should be added to loadpath |
set_string [Rc] | Same as |
set_stringl [Rc] | |
set_stringo [Rc] | |
set_submap [Extmap.S] |
|
set_union [Extmap.S] |
|
sign [BigInt] | |
signbit [Mlmpfr_wrapper] | |
simple_comma [Pp] | |
singleton [Trans] | |
singleton [Extset.S] |
|
singleton [Extmap.S] |
|
slash [Pp] | |
sn_decode [Ident] | |
sort_log_by_loc [Pinterp.Log] | |
sp_attr [Vc] | |
space [Pp] | |
split [Extset.S] |
|
split [Extmap.S] |
|
split [Strings] |
|
split [Lists] | split n l = (prefix n l, chop n l) |
split_theory [Task] |
|
sprint_decl [Printer] | |
sprint_tdecl [Printer] | |
sprinter [Pretty.Printer] | |
sprintf [Pp] | |
sprintf_wnl [Pp] | |
sqrt [Mlmpfr_wrapper] | |
stack_trace [Debug] | stack_trace flag |
star [Pp] | |
start_enum [Extmap.S] | start the enumeration of the given map |
start_ge_enum [Extmap.S] | start the enumeration of the given map at the first key which is greater or equal than the given one |
stats [Debug] | |
stepregexp [Call_provers] |
|
sterm_generic [Term] | |
stop_split [Term] | |
store [Trans] | |
string [Pp] | |
string_list_of_qualid [Typing] | |
string_of [Pp] | |
string_of_wnl [Pp] | same as |
string_unique [Ident] | Uniquify string |
string_value [Pinterp] | |
sub [Mlmpfr_wrapper] | |
sub [BigInt] | |
subdomain [Extmap.S] |
|
submap [Extmap.S] |
|
subnormalize [Mlmpfr_wrapper] | |
subset [Extset.S] |
|
succ [BigInt] | basic operations |
suffix_attr_name [Ident] | Add a suffix to all "name" attributes of |
syntax_arguments [Printer] | |
syntax_arguments_prec [Printer] |
|
syntax_arguments_typed [Printer] | |
syntax_arguments_typed_prec [Printer] |
|
syntax_arity [Printer] |
|
syntax_float_literal [Printer] | |
syntax_literal [Printer] | |
syntax_logic [Printer] | |
syntax_map [Driver] | |
syntax_range_literal [Printer] | |
syntax_type [Printer] | |
system_path [Session_itp] | the system-dependent absolute path associated to that file |
T | |
t_all [Term.TermTF] | |
t_all [Term] | |
t_and [Term] | |
t_and_asym [Term] | |
t_and_asym_l [Term] | |
t_and_asym_simp [Term] | |
t_and_asym_simp_l [Term] | |
t_and_l [Term] | |
t_and_simp [Term] | |
t_and_simp_l [Term] | |
t_any [Term.TermTF] | |
t_any [Term] | |
t_app [Term] | |
t_app_fold [Term] | |
t_app_infer [Term] | |
t_app_map [Term] | |
t_app_partial [Term] |
|
t_attr_add [Term] | |
t_attr_copy [Term] | |
t_attr_remove [Term] | |
t_attr_set [Term] | |
t_binary [Term] | |
t_binary_simp [Term] | |
t_bool_false [Term] | |
t_bool_true [Term] | |
t_case [Term] | |
t_case_close [Term] | |
t_case_close_simp [Term] | |
t_case_simp [Term] | |
t_clone_bound_id [Term] | |
t_close_bound [Term] | |
t_close_branch [Term] | |
t_close_quant [Term] | |
t_closed [Term] | |
t_closure [Term] |
|
t_compare [Term] | |
t_compare_generic [Term] | |
t_compare_strict [Term] | |
t_const [Term] | |
t_eps [Term] | |
t_eps_close [Term] | |
t_equ [Term] | |
t_equ_simp [Term] | |
t_equal [Term] | |
t_equal_generic [Term] | |
t_equal_strict [Term] | |
t_exists [Term] | |
t_exists_close [Term] | |
t_exists_close_merge [Term] |
|
t_exists_close_simp [Term] | |
t_exists_simp [Term] | |
t_false [Term] | |
t_fold [Term.TermTF] |
|
t_fold [Term] | |
t_forall [Term] | |
t_forall_close [Term] | |
t_forall_close_merge [Term] | |
t_forall_close_simp [Term] | |
t_forall_simp [Term] | |
t_freepvs [Ity] | raises |
t_freevars [Term] | |
t_func_app [Term] | |
t_func_app_beta [Term] |
|
t_func_app_beta_l [Term] | |
t_func_app_l [Term] | |
t_gen_map [Term] | |
t_hash [Term] | |
t_hash_generic [Term] | |
t_hash_strict [Term] | |
t_if [Term] | |
t_if_simp [Term] | |
t_iff [Term] | |
t_iff_simp [Term] | |
t_implies [Term] | |
t_implies_simp [Term] | |
t_int_const [Term] | |
t_is_lambda [Term] |
|
t_iter [Term] | |
t_lambda [Term] |
|
t_let [Term] | |
t_let_close [Term] | |
t_let_close_simp [Term] | |
t_let_simp [Term] | |
t_map [Term.TermTF] |
|
t_map [Term] | |
t_map_cont [Term.TermTF] | |
t_map_cont [Term] |
|
t_map_fold [Term.TermTF] | |
t_map_fold [Term] | |
t_map_sign [Term.TermTF] | |
t_map_sign [Term] |
|
t_map_simp [Term.TermTF] | |
t_map_simp [Term] |
|
t_nat_const [Term] |
|
t_neq [Term] | |
t_neq_simp [Term] | |
t_not [Term] | |
t_not_simp [Term] | |
t_occurs [Term] | |
t_open_bound [Term] | |
t_open_bound_cb [Term] | |
t_open_bound_with [Term] |
|
t_open_branch [Term] | |
t_open_branch_cb [Term] | |
t_open_lambda [Term] |
|
t_open_lambda_cb [Term] | the same as |
t_open_quant [Term] | |
t_open_quant_cb [Term] | |
t_or [Term] | |
t_or_asym [Term] | |
t_or_asym_l [Term] | |
t_or_asym_simp [Term] | |
t_or_asym_simp_l [Term] | |
t_or_l [Term] | |
t_or_simp [Term] | |
t_or_simp_l [Term] | |
t_peek_bound [Term] | |
t_peek_branch [Term] | |
t_peek_quant [Term] | |
t_pred_app [Term] | |
t_pred_app_beta [Term] |
|
t_pred_app_beta_l [Term] | |
t_pred_app_l [Term] | |
t_prop [Term] |
|
t_quant [Term] | |
t_quant_close [Term] | |
t_quant_close_simp [Term] | |
t_quant_simp [Term] | |
t_real_const [Term] | |
t_replace [Term] | |
t_s_all [Term] | |
t_s_any [Term] | |
t_s_fold [Term] | |
t_s_map [Term] | |
t_select [Term.TermTF] |
|
t_selecti [Term.TermTF] |
|
t_string_const [Term] | |
t_subst [Term] |
|
t_subst_single [Term] |
|
t_subst_types [Term] |
|
t_true [Term] | |
t_tuple [Term] | |
t_ty_check [Term] |
|
t_ty_fold [Term] | |
t_ty_freevars [Term] | |
t_ty_map [Term] | |
t_ty_subst [Term] |
|
t_type [Term] |
|
t_v_all [Term] | |
t_v_any [Term] | |
t_v_count [Term] | |
t_v_fold [Term] | |
t_v_map [Term] | |
t_v_occurs [Term] | |
t_var [Term] | |
t_vars [Term] | |
t_void [Expr] | |
tag [Wstdlib.TaggedType] | |
tag [Weakhtbl.Weakey] | |
tag_equal [Weakhtbl] | |
tag_hash [Weakhtbl] | |
tapp [Ptree_helpers] | |
task_clone [Task] | |
task_decls [Task] | |
task_equal [Task] | |
task_fold [Task] | |
task_goal [Task] | |
task_goal_fmla [Task] | |
task_hash [Task] | |
task_hd_equal [Task] | |
task_hd_hash [Task] | |
task_iter [Task] | |
task_known [Task] | |
task_meta [Task] | |
task_separate_goal [Task] |
|
task_tdecls [Task] | |
tconst [Ptree_helpers] | |
td_equal [Theory] | |
td_hash [Theory] | |
tdecl [Trans] | |
tdecl_l [Trans] | |
tds_compare [Task] | |
tds_empty [Task] | |
tds_equal [Task] | |
tds_hash [Task] | |
term [Ptree_helpers] | |
term_of_expr [Expr] | |
term_of_post [Expr] | |
terminal_has_color [Util] | Indicates if standard output supports ANSI terminal color codes (i.e. |
test_flag [Debug] | Return the state of the flag |
test_noflag [Debug] | |
tgoal [Trans] | |
tgoal_l [Trans] | |
th_proved [Session_itp] | |
theory_goals [Session_itp] | |
theory_iter_proof_attempt [Session_itp] | |
theory_name [Session_itp] | Theory |
theory_parent [Session_itp] | |
timelimit [Whyconf] | |
timeout [Controller_itp.Scheduler] |
|
timeregexp [Call_provers] | Converts a regular expression with special markers '%h','%m',
'%s','%i' (for milliseconds) into a value of type |
tn_proved [Session_itp] | |
to_channel [Rc] |
|
to_file [Rc] |
|
to_formatter [Rc] |
|
to_int [BigInt] | |
to_small_integer [Number] | |
to_string [BigInt] | |
toggle_flag [Debug] | |
total [Ity] | |
tprinter [Pretty.Printer] | |
tr_equal [Term] | |
tr_fold [Term.TermTF] | |
tr_fold [Term] | |
tr_map [Term.TermTF] | |
tr_map [Term] | |
tr_map_fold [Term.TermTF] | |
tr_map_fold [Term] | |
trace_goal [Trans] | |
transfer_loc [Loc] | |
translate [Extset.S] |
|
translate [Extmap.S] |
|
try1 [Loc] | |
try2 [Loc] | |
try3 [Loc] | |
try4 [Loc] | |
try5 [Loc] | |
try6 [Loc] | |
try7 [Loc] | |
ts_bool [Ty] | |
ts_compare [Ty] | |
ts_equal [Ty] | |
ts_func [Ty] | |
ts_hash [Ty] | |
ts_int [Ty] | |
ts_match_args [Ty] | |
ts_real [Ty] | |
ts_ref [Pmodule] | |
ts_str [Ty] | |
ts_tuple [Ty] | |
ts_unit [Ity] | the same as |
ttrue [Util] |
|
tuple_module [Pmodule] | |
tuple_theory [Theory] | |
tuple_theory_name [Theory] | |
tv_compare [Ty] | |
tv_equal [Ty] | |
tv_hash [Ty] | |
tv_of_string [Ty] | |
tvar [Ptree_helpers] | |
ty_all [Ty] | |
ty_any [Ty] | |
ty_app [Ty] | |
ty_bool [Ty] | |
ty_closed [Ty] |
|
ty_compare [Ty] | |
ty_equal [Ty] | |
ty_equal_check [Ty] | |
ty_fold [Ty] | |
ty_freevars [Ty] | |
ty_func [Ty] | |
ty_hash [Ty] | |
ty_inst [Ty] | |
ty_int [Ty] | |
ty_map [Ty] | traverse only one level of constructor, if you want full traversal you need to call those function inside your function |
ty_match [Ty] |
|
ty_match_args [Ty] | |
ty_of_ity [Ity] | |
ty_pred [Ty] | |
ty_real [Ty] | |
ty_s_all [Ty] | |
ty_s_any [Ty] | |
ty_s_fold [Ty] | |
ty_s_map [Ty] | visits every symbol of the type |
ty_str [Ty] | |
ty_tuple [Ty] | |
ty_unit [Ity] | |
ty_v_all [Ty] | |
ty_v_any [Ty] | |
ty_v_fold [Ty] | |
ty_v_map [Ty] | visits every variable of the type |
ty_var [Ty] | |
type_def_fold [Ty] | |
type_def_map [Ty] | |
type_expr_in_muc [Typing] | |
type_fmla_in_namespace [Typing] | |
type_mlw_file [Typing] | |
type_term_in_namespace [Typing] | |
U | |
uncapitalize [Strings] | |
undefined_value [Pinterp] | |
underscore [Pp] | |
union [Coercion] |
|
union [Extset.S] |
|
union [Extmap.S] |
|
unit_binder [Ptree_helpers] | |
unit_module [Pmodule] | |
unit_value [Pinterp] | |
unknown_to_known_provers [Whyconf] | return others, same name, same version |
unset_flag [Debug] | |
unsupported [Printer] | |
unsupportedDecl [Printer] | |
unsupportedPattern [Printer] | |
unsupportedTerm [Printer] | |
unsupportedType [Printer] | |
update_goal_node [Session_itp] | updates the proved status of the given goal node. |
update_proof_attempt [Session_itp] |
|
update_prover_editor [Whyconf.User] | |
update_section [Whyconf.User] | |
update_trans_node [Session_itp] | updates the proved status of the given transformation node. |
uppercase [Strings] | |
use [Ptree_helpers.I] | see |
use [Ptree_helpers.F] | see |
use [Ptree_helpers] |
|
use_export [Pmodule] | |
use_export [Task] | |
use_export [Theory] | |
used_symbols [Task] | takes the result of |
used_theories [Task] | returns a map from theory names to theories themselves |
user_position [Loc] | |
useraxiom_attr [Ident] | |
V | |
v_desc [Pinterp] | |
v_ty [Pinterp] | |
val_enum [Extmap.S] | get the current key value pair of the enumeration, return None if the enumeration reach the end |
values [Extmap.S] | Return the list of all values of the given map. |
vc [Vc] | |
vs_compare [Term] | |
vs_equal [Term] | |
vs_graph_drop [Decl] | |
vs_graph_let [Decl] | |
vs_graph_pat [Decl] | |
vs_hash [Term] | |
W | |
wait_on_call [Call_provers] | blocking function that waits until the prover finishes. |
warn_clone_not_abstract [Theory] | |
wb_attr [Vc] | |
why3_keywords [Pretty] | |
why3_regexp_of_string [Whyconf] | |
with_location [Loc] | |
with_marker [Mlw_printer] | Inform a printer to include the message (default: |
wnl [Pp] | |
wp_attr [Vc] | |
wrap [Args_wrapper] | |
wrap_and_register [Args_wrapper] | |
wrap_l [Args_wrapper] | |
X | |
xs_compare [Ity] | |
xs_equal [Ity] | |
xs_hash [Ity] | |
Z | |
zero [BigInt] | constants |
zero_p [Mlmpfr_wrapper] |