A  
abstr_num [Options]  
abstract_others [Forward]  
add [Heap.S]  
add [Use.Make]  
add [Uf.S]  
add [Intervals]  
add [Sig.RELATION]  add a representant to take into account 
add [Polynome.T]  
add [Cubetrie]  Add a mapping cube>v to trie 
add_and_resolve [Cubetrie]  
add_array [Cubetrie]  Add a mapping cube>v to trie 
add_array_force [Cubetrie]  Add a mapping cube>v to trie without checking for subsomption 
add_atom [Enumsolver_types]  
add_atom [Solver_types]  
add_constants [Types]  
add_force [Cubetrie]  Add a mapping cube>v to trie without checking for subsomption 
add_fresh [Explanation]  
add_fun_def [Ptree]  
add_label [Literal.S]  
add_node [Cubetrie]  Add a node in the trie 
alien_of [Fm.EXTENDED_Polynome]  
all_arrangements [Variable]  
all_arrangements_arity [Variable]  
all_constructors [Smt_sig.S.Type] 

all_instantiations [Variable]  same as 
all_permutations [Variable] 

all_vals [Cubetrie]  List of all values mapped by the trie 
all_var_terms [Forward]  
alpha [Types.ArrayAtom]  alpha renaming of process variables 
alphas [Variable]  
already_distinct [Uf.S]  
ancestor_of [Node] 

app_fun [Ptree]  
append_extra_procs [Variable]  
apply_subst [Types.ArrayAtom]  Efficient application of substitution 
are_distinct [Uf.S]  
are_equal [Uf.S]  
array [Node]  returns the conjunction in array form of the associated cube 
assign_constr [Smt_sig.S.Variant] 

assign_var [Smt_sig.S.Variant] 

assume [Enumsolver.Make]  
assume [Solver.Make]  
assume [Smt_sig.S.Solver] 

assume [Cc.S]  
assume [Sig.RELATION]  
assume_goal [Prover]  Clears the context and assumes a goal formula 
assume_goal_no_check [Prover]  Same as 
assume_goal_nodes [Prover]  
assume_node [Prover] 

assume_node_no_check [Prover]  Same as 
atom [Enumsolver_types.Debug]  
atom [Solver_types.Debug]  
atoms_list [Enumsolver_types.Debug]  
B  
bitsolver [Options]  
black [Util]  
blue [Util]  
borne_inf [Intervals]  
brab [Brab]  Backtracking procedure that uses approximated backward reachability
( 
brab_up_to [Options]  
build_subst [Variable]  constructs a variable substitution 
C  
candidate [Stats] 

candidate [Dot]  
candidate_heuristic [Options]  
case_split [Sig.RELATION]  case_split env returns a list of equalities 
cc_active [Cc]  
certificate [Trace.S]  this takes a system in input and the list of visited nodes, of which the disjunction constitutes an inductive invariant for the system. 
check [Smt_sig.S.Solver] 

check [Safety] 

check [Fixpoint.FixpointTrieNaive]  
check [Fixpoint.FixpointTrie] 

check [Fixpoint.FixpointList] 

check_bottom_clause [Enumsolver_types]  
check_guard [Prover] 

check_limit [Stats]  Raises 
check_strategy [Smt_sig.S.Solver]  The stragey used for preforming checksat. 
choose [Polynome.T]  
choose [Types.MConst]  
chromatic [Util]  
cin [Options]  
class_of [Uf.S]  
class_of [Cc.S]  
clause [Enumsolver_types.Debug]  
clause [Solver_types.Debug]  
clear [Vec]  
clear [Enumsolver_types]  
clear [Enumsolver.Make]  
clear [Solver_types]  
clear [Solver.Make]  
clear [Smt_sig.S.Solver] 

clear [Bwd.PriorityNodeQueue]  
close [Smt_sig.S.Variant] 

combine [Hashcons]  
combine2 [Hashcons]  
combine3 [Hashcons]  
combine_list [Hashcons]  
combine_option [Hashcons]  
combine_pair [Hashcons]  
compare [Hstring] 

compare [Heap.OrderType]  
compare [Ty]  
compare [Term]  
compare [Symbols]  
compare [Sig.X]  
compare [Sig.COMBINATOR]  
compare [Polynome.S]  
compare [Literal.OrderedType]  
compare [Literal.S]  
compare [Sig.THEORY]  
compare [Polynome.T]  
compare [Variable]  
compare [Types.Atom]  compares two atoms. 
compare [Types.Term]  
compare [Types.Var]  
compare_by_breadth [Node]  compare two nodes with a heuristic to find the most general one. 
compare_by_depth [Node]  compare two nodes with a heuristic to find the most general one. 
compare_constants [Types]  
compare_list [Hstring] 

compare_list [Variable]  
compare_nb_common [Types.ArrayAtom] 

compare_nb_diff [Types.ArrayAtom] 

compute [Fake_functory.Cores]  
conflicting_from_trace [Forward]  check if an error trace is spurious due to the Crash Failure Model 
congr_add [Use.Make]  
congr_close_up [Use.Make]  
consistent [Cubetrie]  All values whose keys (cubes) are not inconsistent with the given cube. 
const_nul [Types]  
const_sign [Types]  
constructors [Smt_sig.S.Type] 

copy [Vec]  
cores [Options]  
cpp_cmd [Options]  
cpt_delete [Stats]  number of delted nodes 
cpt_mk_var [Enumsolver_types]  
cpt_mk_var [Solver_types]  
create [Polynome.T]  
create [Node]  given a cube creates a node with a given kind, and a history 
create [Cube]  create a cube given its existential variables and a conjunction 
create [Bwd.PriorityNodeQueue]  
create_normal [Cube]  create a cube in normal form by finding the quantified variables 
D  
date [Version]  
debug [Options]  
debug_smt [Options]  
declare [Smt_sig.S.Symbol] 

declare [Smt_sig.S.Type] 

declared [Smt_sig.S.Symbol] 

declared_types [Smt_sig.S.Type]  
decrease [Iheap]  
delete [Stats] 

delete [Options]  
delete [Cubetrie]  Delete all values which satisfy the predicate p 
delete_node_by [Dot]  
delete_subsumed [Cubetrie]  Delete from the trie nodes that are subsumed by the first arguments 
diff [Types.ArrayAtom]  array form of set difference 
dim [Node]  returns the dimension of the associated cube (see 
dim [Cube]  returns the number of exitential distinct variables, i.e. 
distinct [Uf.S]  
div [Intervals]  
div [Polynome.T]  
dmcmt [Options]  
do_brab [Options]  
doesnt_contain_0 [Intervals]  
dot [Options]  
dot_colors [Options]  
dot_level [Options]  
dot_prog [Options]  
dummy_atom [Enumsolver_types]  
dummy_atom [Solver_types]  
dummy_clause [Enumsolver_types]  
dummy_clause [Solver_types]  
dummy_var [Enumsolver_types]  
dummy_var [Solver_types]  
E  
easy_fixpoint [Fixpoint.FixpointTrie]  easy fixpoint test with subset tests 
elements [Heap.S]  
elim_ite_simplify [Cube]  lifts 
elim_ite_simplify_atoms [Cube]  lifts 
embed [Sum.ALIEN]  
embed [Sig.C]  
embed [Sig.THEORY]  
empty [Hstring]  the empty ( 
empty [Heap.S]  
empty [Use.Make]  
empty [Uf.S]  
empty [Explanation]  
empty [Cc.S]  
empty [Sig.RELATION]  
empty [Cubetrie]  The empty trie. 
empty_embedding [Sig.COMBINATOR]  
empty_env [Enumerative]  A dummy empty environment. 
empty_state [Enumerative]  A dummy empty state. 
encode_psystem [Ptree]  
encoding [Muparser_globals]  Filled by 
enqueue_ident [Enumsolver_types]  
entails [Smt_sig.S.Solver] 

enumerative [Options]  
enumsolver [Options]  
env [Muparser_globals]  
equal [Hstring] 

equal [Hashcons.HashedType_consed]  
equal [Hashcons.HashedType]  
equal [Ty]  
equal [Term]  
equal [Symbols]  
equal [Sig.X]  
equal [Literal.S]  
equal [Types.ArrayAtom]  
equal [Types.SAtom]  
equal [Types.Atom]  
equal [Types.Term]  
error_trace [Stats]  print an error trace given a faulty node 
error_trace [Dot]  
exclude [Intervals]  
exhaustive [Instantiation]  Same as 
extra_procs [Variable]  
extra_vars [Variable]  
extract [Sum.ALIEN]  
extract [Sig.C]  
extract [Sig.COMBINATOR]  
F  
f_false [Smt_sig.S.Formula]  The formula which represents 
f_true [Smt_sig.S.Formula]  The formula which represents 
fast_remove [Vec]  
faux [Term]  
faux [Literal.S_Term]  
file [Options]  
filter [Iheap]  
find [Use.Make]  
find [Uf.S]  
find [Polynome.T]  
find_r [Uf.S]  
finite_size [Intervals]  
first_good_candidate [Oracle.S]  Given a list of candidate invariants, returns the first one that seems to be indeed an invariant. 
fixpoint [Stats]  register the result of a successful fixpoint check 
fixpoint [Dot]  
fold [Cubetrie]  fold f to all values mapped to in the trie. 
fold_atoms [Explanation]  
forward_depth [Options]  
forward_inv [Options]  
forward_sym [Options]  
fresh_dname [Enumsolver_types]  
fresh_dname [Solver_types]  
fresh_exp [Explanation]  
fresh_lname [Enumsolver_types]  
fresh_lname [Solver_types]  
fresh_name [Enumsolver_types]  
fresh_name [Solver_types]  
freshs [Variable]  
from_array [Vec]  
from_list [Vec]  
fully_interpreted [Sig.X]  
fully_interpreted [Sig.THEORY]  
G  
gen_inv [Options]  
get [Vec]  
get [Timer.S]  Returns the time in seconds accumulated in the timer. 
get_calls [Smt_sig.S.Solver] 

get_time [Smt_sig.S.Solver] 

get_variants [Smt_sig.S.Variant] 

give_procs [Variable]  
good [Approx.S]  Returns a good approximation in the form of a candidate invariant if the oracle was able to find one. 
green [Util]  
grow_to [Vec]  
grow_to_by_double [Vec]  
grow_to_by_double [Iheap]  
grow_to_double_size [Vec]  
H  
hard_fixpoint [Fixpoint.FixpointTrie]  full semantic fixpoint test with SMT solver 
has_abstract_type [Smt_sig.S.Symbol] 

has_deleted_ancestor [Node]  returns 
has_infinite_type [Smt_sig.S.Symbol] 

has_type_proc [Smt_sig.S.Symbol] 

has_var [Types.Atom]  returns 
has_vars [Types.Atom]  returns 
hash [Hstring] 

hash [Hashcons.HashedType_consed]  
hash [Hashcons.HashedType]  
hash [Ty]  
hash [Term]  
hash [Symbols]  
hash [Sig.X]  
hash [Literal.OrderedType]  
hash [Literal.S]  
hash [Sig.THEORY]  solve r1 r2, solve the equality r1=r2 and return the substitution 
hash [Polynome.T]  
hash [Types.ArrayAtom]  
hash [Types.SAtom]  
hash [Types.Atom]  
hash [Types.Term]  
hashcons [Hashcons.S_consed] 

hashcons [Hashcons.S] 

hex_color [Util]  
hfalse [Types.Term]  
htrue [Types.Term]  
I  
in_heap [Iheap]  
inconsistent [Cube]  
inconsistent_2 [Cube]  is the conjunction of 
inconsistent_2arrays [Cube]  same as 
inconsistent_array [Cube]  same as 
inconsistent_set [Cube]  returns 
init [Vec]  
init [Iheap]  
init [Smt_sig.S.Variant] 

init [Oracle.S]  Initialize the oracle on a given system 
insert [Iheap]  
instantiate_transitions [Forward]  instantiate transitions with a list of possible parameters 
int [Term]  
int [Symbols]  
int_of_term [Enumerative]  Encoding of a term in the enumerative environment. 
intersect [Intervals]  
is_ac [Symbols]  
is_attached [Enumsolver_types]  
is_bottom [Enumsolver_types]  
is_empty [Vec]  
is_empty [Iheap]  
is_empty [Polynome.T]  
is_empty [Cubetrie]  Test emptyness of a trie 
is_empty [Bwd.PriorityNodeQueue]  
is_full [Vec]  
is_int [Term]  
is_int [Smt_sig.S.Term] 

is_mine_symb [Sig.THEORY]  return true if the symbol is owned by the theory 
is_monomial [Polynome.T]  
is_num [Types.MConst]  
is_point [Intervals]  
is_proc [Variable]  returns 
is_real [Term]  
is_real [Smt_sig.S.Term] 

is_strict_smaller [Intervals]  
is_subst_identity [Variable]  returns 
iter [Hashcons.S_consed] 

iter [Hashcons.S] 

iter [Cubetrie]  Apply f to all values mapped to in the trie. 
iter_atoms [Explanation]  
iter_subsumed [Cubetrie]  Apply f to all values whose keys (cubes) are subsumed by the given cube. 
J  
js_mode [Options]  
L  
label [Literal.S]  
last [Vec]  
lazyinv [Options]  
leaves [Sig.X]  
leaves [Sig.COMBINATOR]  
leaves [Sig.THEORY]  Give the leaves of a term of the theory 
length [Heap.S]  
length [Bwd.PriorityNodeQueue]  
libdir [Version]  
limit_forward_depth [Options]  
list_assoc [Hstring] 

list_assoc_inv [Hstring] 

list_equal [Hstring] 

list_mem [Hstring] 

list_mem_assoc [Hstring]  Same as 
list_mem_couple [Hstring] 

litterals [Node]  returns the conjunction of litterals of the associated cube 
localized [Options]  
M  
ma [Solver_types]  
made_vars_info [Enumsolver_types]  
made_vars_info [Solver_types]  
magenta [Util]  
make [Vec]  
make [Hstring] 

make [Term]  
make [Smt_sig.S.Formula] 

make [Sig.X]  
make [Sig.COMBINATOR]  
make [Literal.S]  
make [Sig.THEORY]  Give a representant of a term of the theory 
make_app [Smt_sig.S.Term] 

make_arith [Smt_sig.S.Term] 

make_clause [Enumsolver_types]  
make_clause [Solver_types]  
make_cnf [Smt_sig.S.Formula] 

make_formula [Prover]  
make_formula_set [Prover]  
make_int [Smt_sig.S.Term] 

make_lit [Smt_sig.S.Formula] 

make_literal [Prover]  
make_real [Smt_sig.S.Term] 

make_tau [Pre]  functional form of transition 
make_var [Solver_types]  
max_cands [Options]  
max_forward [Options]  
max_proc [Options]  
maxnodes [Options]  
maxrounds [Options]  
mem [Use.Make]  
mem [Uf.S]  
mem [Cubetrie]  Is cube subsumed by some cube in the trie? 
mem_array [Cubetrie]  Is cube subsumed by some cube in the trie? 
mem_array_poly [Cubetrie]  Is cube subsumed by some cube in the trie? 
merge [Explanation]  
mk_env [Enumerative] 

mk_pred [Literal.S_Term]  
mode [Options]  
modulo [Polynome.T]  
move_to [Vec]  
mu_cmd [Options]  
mu_opts [Options]  
mult [Polynome.S]  
mult [Intervals]  
mult [Polynome.T]  
mult_const [Polynome.T]  
mult_const [Types]  
murphi [Options]  
murphi_uopts [Options]  
N  
name [Symbols]  
name [Sig.THEORY]  Name of the theory 
nb_diff [Types.ArrayAtom]  returns the number of differences, i.e. 
nb_digits [Util]  Returns the number of digits of a positive integer 
neg [Literal.S]  
neg [Types.Atom]  returns the negation of the atom 
new_borne_inf [Intervals]  
new_borne_sup [Intervals]  
new_node [Stats]  register the treatment of a new node 
new_node [Dot]  
new_state [Muparser_globals]  Called by 
new_undef_state [Enumerative]  Returns a new uninitialized state from an enumertive environment 
next_id [Enumerative]  Returns the next free integer that is not used for encoding terms. 
no_scan_states [Enumerative]  Prevent the GC from scanning the list of states stored in the environemnt as it is going to be kept in memory all the time. 
nocolor [Options]  
noqe [Options]  
normal_form [Sig.COMBINATOR]  
normal_form [Polynome.T]  
normal_form [Cube]  puts a cube in normal form, so as to have the existential variables
contiguous ( 
normal_form_pos [Polynome.T]  
notyping [Options]  
num_range [Options]  
number [Variable]  
O  
of_satom [Types.ArrayAtom]  transforms a conjunction if the form of a set of atoms to an equivalent representation with an array 
only_forward [Options]  
open_dot [Dot]  
origin [Node]  returns the origin of the node, i.e. 
out_trace [Options]  
P  
pause [Timer.S]  Pause the time, i.e. 
peasy_fixpoint [Fixpoint.FixpointTrie]  easy fixpoint test including permutations 
permutations_missing [Variable]  
pgcd_numerators [Polynome.T]  
point [Intervals]  
poly_of [Fm.EXTENDED_Polynome]  
pop [Vec]  
pop [Heap.S]  
pop [Smt_sig.S.Solver]  Pop the last context from the stack and forget what was done since the last push. 
pop [Bwd.PriorityNodeQueue]  
pop_ident [Enumsolver_types]  
post_strategy [Options]  
power [Intervals]  
ppmc_denominators [Polynome.T]  
pre_image [Pre] 

print [Hstring]  Prints a hashconsed strings on a formatter. 
print [Use.Make]  
print [Ty]  
print [Term]  
print [Symbols]  
print [Smt_sig.S.Formula] 

print [Smt_sig.S.Variant] 

print [Sig.X]  
print [Sig.COMBINATOR]  
print [Polynome.S]  
print [Literal.OrderedType]  
print [Literal.S]  
print [Intervals]  
print [Explanation]  
print [Sig.THEORY]  
print [Polynome.T]  
print [Variable]  
print [Types.ArrayAtom]  prints the conjunction corresponding to the array of atoms 
print [Types.SAtom]  prints a conjunction 
print [Types.Atom]  prints an atom 
print [Types.Term]  prints a term 
print [Node]  prints the cube of a node 
print [Cube]  
print_double_line [Pretty]  prints separating double line 
print_history [Node]  prints the trace corresponding to the history of a node 
print_inline [Types.SAtom]  prints a conjunction on a signle line 
print_last [Enumerative]  
print_line [Pretty]  prints separating line 
print_list [Hstring]  Prints a list of hashconsed strings on a formatter. 
print_list [Pretty] 

print_report [Stats]  prints a complete report. 
print_state [Enumerative]  Printing a state. 
print_stats_certificate [Stats]  
print_subst [Variable]  
print_system [Murphi] 

print_system [Ptree]  
print_title [Pretty]  prints section title for stats 
print_vars [Variable]  
proc_vars_int [Variable]  
procs [Variable]  predefinied list of skolem variables 
profiling [Options]  
psystem_of_decls [Ptree]  
pure_smt_check [Fixpoint.FixpointList]  Same as 
push [Vec]  
push [Smt_sig.S.Solver]  Push the current context on a stack. 
push [Bwd.PriorityNodeQueue]  
push_list [Bwd.PriorityNodeQueue]  
push_none [Vec]  
Q  
query [Cc.S]  
query [Sig.RELATION]  
quiet [Options]  
R  
reachable_on_trace_from_init [Forward]  
reached [Prover] 

real [Term]  
real [Symbols]  
red [Util]  
refine [Options]  
refine_universal [Options]  
register_state [Enumerative]  Register the given state as an explored state in the environment. 
relevant [Instantiation] 

remaining [Stats]  outputs number of remaining nodes in the queues given a function to count them. 
remove [Vec]  
remove [Polynome.T]  
remove_bad_candidates [Approx]  Register bad candidates and try to infer as much inforamtion as possible from the error trace before the restart. 
remove_fresh [Explanation]  
remove_min [Iheap]  
remove_trailing_whitespaces_end [Util]  
replay_history [Forward]  Replays the history of a faulty node and returns (possibly) an error trace 
replay_trace_and_expand [Enumerative]  
report [Smt_sig.S]  
report [Typing]  
report_loc [Util]  Report location on formatter 
reset_gc_params [Util]  Reset the parameters of the GC to its default values. 
resolve_two [Cube]  
restart [Stats]  resisters a backtrack and restart 
restart [Dot]  
restore [Enumsolver.Make]  
restore [Solver.Make]  
resume_search_from [Enumerative]  
root [Intervals]  
run [Prover]  Runs the SMT solver on its current context 
S  
same_ident [Enumsolver_types]  
satom_globs [Cube]  
save [Enumsolver.Make]  
save [Solver.Make]  
scale [Intervals]  
search [Forward]  
search [Enumerative] 

search [Bwd.Strategy]  Backward reachability search on a system. 
search_stateless [Forward]  
set [Vec]  
set_arith [Smt_sig.S]  set_arith 
set_arith_active [Combine.CX]  
set_cc [Smt_sig.S]  set_cc 
set_js_mode [Options]  
set_liberal_gc [Util]  Changes garbage collector parameters limit its effect 
set_number_of_cores [Fake_functory.Cores]  
set_size [Vec]  
set_sum [Smt_sig.S]  set_sum 
set_sum_active [Combine.CX]  
shrink [Vec]  
simpl_by_uc [Options]  
simplify [Cube]  simplify a cube. 
simplify_atoms [Cube]  simplify a conjunction. 
simplify_atoms_base [Cube] 

singleton [Explanation]  
size [Vec]  
size [Iheap]  
size [Node]  returns the size of the associated cube (see 
size [Cube]  returns the number of atoms in the conjuction 
size_of_env [Enumerative]  Returns the (heuristically) computed size of tables needed for the exploration. 
size_proc [Options]  
smallest_to_resist_on_trace [Enumerative]  Given a list of candidate approximations (and their permutations),
checks if one is satisfiable on the finite model constructed by

smt_solver [Options]  
solve [Enumsolver.Make]  
solve [Solver.Make]  
solve [Sig.X]  
solve [Sig.COMBINATOR]  
solve [Sig.THEORY]  
sort [Vec]  
spurious [Forward]  check if the history of a node is spurious 
spurious_due_to_cfm [Forward]  check if an error trace is spurious due to the Crash Failure Model 
spurious_error_trace [Forward]  check if an error trace is spurious 
sqrt [Intervals]  
st [Muparser_globals]  
start [Timer.S]  Start (or restart) recording user time when this function is called. 
stateless [Options]  
stats [Hashcons.S_consed]  Return statistics on the table. 
stats [Hashcons.S]  Return statistics on the table. 
sub [Polynome.T]  
subset [Types.ArrayAtom] 

subset [Node]  returns true if the set of litterals of the cube associated with the first arguement is a subset of the second argument 
subst [Sig.X]  
subst [Sig.COMBINATOR]  
subst [Sig.THEORY]  
subst [Polynome.T]  
subst [Variable]  apply a variable substitution to a variable 
subst [Types.SAtom]  Apply the substitution given in argument to the conjunction 
subst [Types.Atom]  Apply the substitution given in argument to the atom. 
subst [Types.Term]  Apply the substitution given in argument to the term 
subst [Cube]  apply a substitution on a cube 
subtyping [Options]  
syscall [Util]  Captures the output of a unix command 
syscall_full [Util]  Captures the standard and error output of a unix command with its exit status 
system [Typing]  Types an untyped system and performs subtyping analysis is the flag

T  
t_false [Smt_sig.S.Term] 

t_true [Smt_sig.S.Term] 

tag [Hashcons.HashedType]  
term_embed [Sig.X]  
term_embed [Polynome.S]  
term_extract [Sig.X]  
term_extract [Sig.THEORY]  
to_float [Enumsolver_types]  
to_float [Solver_types]  
to_int [Enumsolver_types]  
to_int [Solver_types]  
to_list [Polynome.T]  
to_satom [Types.ArrayAtom]  returns the set of atoms corresponding to the conjuntion encoded in the array 
trace [Options]  
trivial_is_implied [Types.ArrayAtom]  
trivial_is_implied [Types.Atom]  return 
type_bool [Smt_sig.S.Type]  The type of booleans 
type_info [Sig.X]  
type_info [Sig.COMBINATOR]  
type_info [Sig.THEORY]  
type_info [Polynome.T]  
type_int [Smt_sig.S.Type]  The type of integers 
type_of [Smt_sig.S.Symbol] 

type_of [Types.Term]  returns the type of the term as it is known by the SMT solver 
type_only [Options]  
type_proc [Smt_sig.S.Type]  The type processes (identifiers) 
type_real [Smt_sig.S.Type]  The type of reals 
U  
uguard_dnf [Forward]  put a universal guard in disjunctive normal form 
undefined [Intervals]  
union [Uf.S]  
union [Explanation]  
union [Types.ArrayAtom]  in fact concatenation, equivalent to taking the conjunctions of two conjunctinos 
unsafe [Prover]  Checks if the node is directly reachable on init of the system 
unsolvable [Sig.X]  
unsolvable [Sig.THEORY]  return true when the argument is an unsolvable function of the theory 
up_add [Use.Make]  
up_close_up [Use.Make]  
useful_instances [Fixpoint.FixpointCertif]  Returns the cube instances that were useful in proving the fixpoint. 
V  
var [Symbols]  
variables [Types.SAtom]  returns the existential variables of the given conjunction 
variables [Types.Atom]  returns the existential variables of the given atom 
variables [Types.Term]  returns the existential variables of the given term 
variables [Node]  returns the variables of the associated cube 
variables_proc [Types.SAtom]  same as 
variables_proc [Types.Atom]  same as 
variables_proc [Types.Term]  same as 
verbose [Options]  
version [Version]  
view [Hstring] 

view [Term]  
view [Literal.S]  
vrai [Term]  
vrai [Literal.S_Term]  
vt_width [Pretty]  Width of the virtual terminal (80 if cannot be detected) 
W  
well_formed_subst [Variable]  returns 
white [Util] 