Index of values


A
abstr_num [Options]
abstract_others [Forward]
add [Use.Make]
add [Uf.S]
add [Intervals]
add [Sig.RELATION]
add a representant to take into account
add [Polynome.T]
add [Heap.S]
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_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.Type]
all_constructors () returns a list of all the defined constructors.
all_instantiations [Variable]
same as Variable.all_permutations but does not assume elements of l1 to be distinct.
all_ones [Bitv]
all_permutations [Variable]
all_permutations l1 l2 returns all possible substitutions from l1 to l2 assuming that the variables of both lists are distinct.
all_vals [Cubetrie]
List of all values mapped by the trie
all_var_terms [Forward]
all_zeros [Bitv]
alpha [Types.ArrayAtom]
alpha renaming of process variables
alphas [Variable]
already_distinct [Uf.S]
ancestor_of [Node]
ancestor_of a b returns true if a is an ancestor of b
append [Bitv]
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.Variant]
assign_constr s cstr will add the constraint that the constructor cstr must be in the type of s
assign_var [Smt.Variant]
assign_var x y will add the constraint that the type of y is a subtype of x (use this function when x := y appear in your program
assume [Enumsolver.Make]
assume [Solver.Make]
assume [Cc.S]
assume [Sig.RELATION]
assume [Smt.Solver]
assume id f adds the formula f to the context of the solver with idetifier id.
assume_goal [Prover]
Clears the context and assumes a goal formula
assume_goal_nodes [Prover]
assume_node [Prover]
assume_node n a assumes the negation of a node n given in the form of a renaming a; raises Unsat if the context becomes unsatisfiable
atom [Enumsolver_types.Debug]
atom [Solver_types.Debug]
atoms_list [Enumsolver_types.Debug]

B
bitsolver [Options]
black [Util]
blit [Bitv]
blue [Util]
borne_inf [Intervals]
brab [Brab]
Backtracking procedure that uses approximated backward reachability (Bwd).
brab_up_to [Options]
build_subst [Variable]
constructs a variable substitution
bw_and [Bitv]
bw_and_in_place [Bitv]
bw_not [Bitv]
bw_not_in_place [Bitv]
bw_or [Bitv]
bw_or_in_place [Bitv]
bw_xor [Bitv]

C
candidate [Stats]
candidate n c registers a new candidate c emerging from node n
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 [Safety]
check s n raises Unsafe n if the node n is immediately reachable in the system s, i.e.
check [Smt.Solver]
check () runs Alt-Ergo light on its context.
check [Fixpoint.FixpointTrieNaive]
check [Fixpoint.FixpointTrie]
check s v returns the tags of nodes in v that were used if s implies the disjunction of the nodes in v.
check [Fixpoint.FixpointList]
check s v returns the tags of nodes in v that were used if s implies the disjunction of the nodes in v.
check_bottom_clause [Enumsolver_types]
check_guard [Prover]
check_guard vars s g checks if the guard g is feasible in state s; raises Unsat if it is not the case
check_limit [Stats]
Raises ReachedLimit if the limits given in Options have been exceeded
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 [Enumsolver_types]
clear [Enumsolver.Make]
clear [Solver_types]
clear [Solver.Make]
clear [Vec]
clear [Smt.Solver]
clear () clears the context of the solver.
clear [Bwd.PriorityNodeQueue]
close [Smt.Variant]
close () will compute the smallest type possible for each symbol.
combine [Hashcons]
combine2 [Hashcons]
combine3 [Hashcons]
combine_list [Hashcons]
combine_option [Hashcons]
combine_pair [Hashcons]
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 [Hstring]
compares x y returns 0 if x and y are equal, and is unspecified otherwise but provides a total ordering on hash-consed strings.
compare [Heap.OrderType]
compare [Types.Atom]
compares two atoms.
compare [Types.Term]
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 l1 l2 returns 0 if and only if l1 is equal to l2.
compare_nb_common [Types.ArrayAtom]
compare_nb_common a t1 t2: compares the "level of proximity" with a.
compare_nb_diff [Types.ArrayAtom]
compare_nb_diff a t1 t2: based on the previous measure, this compares the "level" of difference with a
compute [Fake_functory.Cores]
concat [Bitv]
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.Type]
constructors ty returns the list of constructors of ty when type is an enumerated data-type, otherwise returns [].
copy [Bitv]
copy [Vec]
cores [Options]
cpt_delete [Stats]
number of delted nodes
cpt_mk_var [Enumsolver_types]
cpt_mk_var [Solver_types]
create [Polynome.T]
create [Bitv]
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.Symbol]
declare s [arg_1; ... ; arg_n] out declares a new function symbol with type (arg_1, ... , arg_n) -> out
declare [Smt.Type]
declare n cstrs declares a new enumerated data-type with name n and constructors cstrs., declare n [] declares a new abstract type with name n.
declared [Smt.Symbol]
declared x is true if x is already declared.
decrease [Iheap]
delete [Stats]
delete nb registers nb deletions
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 Cube.dim)
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 if-then-else constructs and simplify a cube
elim_ite_simplify_atoms [Cube]
lifts if-then-else constructs and simplify a conjunction
embed [Sum.ALIEN]
embed [Sig.C]
embed [Sig.THEORY]
empty [Use.Make]
empty [Uf.S]
empty [Explanation]
empty [Cc.S]
empty [Sig.RELATION]
empty [Hstring]
the empty ("") hash-consed string.
empty [Heap.S]
empty [Cubetrie]
The empty trie.
empty_embedding [Sig.COMBINATOR]
enqueue_ident [Enumsolver_types]
entails [Smt.Solver]
entails ~id f returns true if the context of the solver entails the formula f.
enumerative [Options]
enumsolver [Options]
equal [Ty]
equal [Term]
equal [Symbols]
equal [Sig.X]
equal [Literal.S]
equal [Hstring]
equal x y returns true if x and y are the same hash-consed string (constant time).
equal [Hashcons.HashedType_consed]
equal [Hashcons.HashedType]
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 Instantiation.relevant but does not performs any checks
extra_procs [Variable]
extra_vars [Variable]
extract [Sum.ALIEN]
extract [Sig.C]
extract [Sig.COMBINATOR]

F
f_false [Smt.Formula]
The formula which represents false
f_true [Smt.Formula]
The formula which represents true
fast_remove [Vec]
faux [Term]
faux [Literal.S_Term]
file [Options]
fill [Bitv]
filter [Iheap]
find [Use.Make]
find [Uf.S]
find [Polynome.T]
find_r [Uf.S]
finite_size [Intervals]
first_good_candidate [Enumerative]
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]
fold_left [Bitv]
fold_right [Bitv]
foldi_left [Bitv]
foldi_right [Bitv]
forward_depth [Options]
forward_inv [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 [Bitv]
get [Vec]
get [Timer.S]
Returns the time in seconds accumulated in the timer.
get_calls [Smt.Solver]
get_calls () returns the cumulated number of calls to Smt.Solver.check.
get_time [Smt.Solver]
get_time () returns the cumulated time spent in the solver in seconds.
get_variants [Smt.Variant]
get_variants s returns a set of constructors, which is the refined type of s.
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.
gray_iter [Bitv]
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.Symbol]
has_abstract_type x is true if the type of x is abstract.
has_deleted_ancestor [Node]
returns true if one of the ancestor has been set to deleted
has_infinite_type [Smt.Symbol]
has_infinite_type x is true if the type of x is not finite.
has_type_proc [Smt.Symbol]
has_type_proc x is true if x has the type of a process identifier.
has_var [Types.Atom]
returns true if the atom contains the variable given in argument
has_vars [Types.Atom]
returns true if the atom contains one of the variable given in argument
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 [Hstring]
hash x returns the integer (hash) associated to x.
hash [Hashcons.HashedType_consed]
hash [Hashcons.HashedType]
hash [Types.ArrayAtom]
hash [Types.SAtom]
hash [Types.Atom]
hash [Types.Term]
hashcons [Hashcons.S_consed]
hashcons n f hash-cons the value n using function f i.e.
hashcons [Hashcons.S]
hashcons n f hash-cons the value n using function f i.e.
hex_color [Util]
hfalse [Types.Term]
htrue [Types.Term]

I
in_heap [Iheap]
inconsistent [Cube]
inconsistent_2 [Cube]
is the conjunction of c1 and c2 inconsistent knowing that c1 and c2 are consitent on their own.
inconsistent_2arrays [Cube]
same as Cube.inconsistent_2 but for arrays
inconsistent_array [Cube]
same as Cube.inconsistent_set but for arrays
inconsistent_set [Cube]
returns true if the conjunction inconsistent
init [Smt.Variant]
init l where l is a list of pairs (s, ty) initializes the type (and associated constructors) of each s to its original type ty.
init [Bitv]
init [Vec]
init [Iheap]
init [Enumerative]
init [Oracle.S]
Initialize the oracle on a given system
input_bin [Bitv]
insert [Iheap]
instantiate_transitions [Forward]
instantiate transitions with a list of possible parameters
int [Term]
int [Symbols]
intersect [Intervals]
is_ac [Symbols]
is_attached [Enumsolver_types]
is_bottom [Enumsolver_types]
is_empty [Polynome.T]
is_empty [Vec]
is_empty [Iheap]
is_empty [Cubetrie]
Test emptyness of a trie
is_empty [Bwd.PriorityNodeQueue]
is_full [Vec]
is_int [Term]
is_int [Smt.Term]
is_int x is true if the term x has type int
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 true if the variable is a skolem process #i
is_real [Term]
is_real [Smt.Term]
is_real x is true if the term x has type real
is_strict_smaller [Intervals]
is_subst_identity [Variable]
returns true if the substitution is the identity function
iter [Bitv]
iter [Hashcons.S_consed]
iter f iterates f over all elements of the table .
iter [Hashcons.S]
iter f iterates f over all elements of the table .
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.
iteri [Bitv]
iteri_true [Bitv]

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 [Bitv]
length [Heap.S]
length [Bwd.PriorityNodeQueue]
libdir [Version]
limit_forward_depth [Options]
list_assoc [Hstring]
list_assoc x l returns the element associated with x in the list of pairs l.
list_equal [Hstring]
list_equal l1 l2 returns true if and only if l1 is equal to l2.
list_mem [Hstring]
list_mem x l is true if and only if x is equal to an element of l.
list_mem_assoc [Hstring]
Same as Hstring.list_assoc, but simply returns true if a binding exists, and false if no bindings exist for the given key.
list_mem_couple [Hstring]
list_mem_couple (x,y) l is true if and only if (x,y) is equal to an element of l.
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 [Term]
make [Smt.Formula]
make cmb [f_1; ...; f_n] creates the formula (f_1 <cmb> ... <cmb> f_n).
make [Sig.X]
make [Sig.COMBINATOR]
make [Literal.S]
make [Sig.THEORY]
Give a representant of a term of the theory
make [Vec]
make [Hstring]
make s builds ans returns a hash-consed string from s.
make_app [Smt.Term]
make_app f l creates the application of function symbol f to a list of terms l.
make_arith [Smt.Term]
make_arith op t1 t2 creates the term t1 <op> t2.
make_clause [Enumsolver_types]
make_clause [Solver_types]
make_cnf [Smt.Formula]
make_cnf f returns a conjunctive normal form of f under the form: a list (which is a conjunction) of lists (which are disjunctions) of literals.
make_formula [Prover]
make_formula_set [Prover]
make_int [Smt.Term]
make_int n creates an integer constant of value n.
make_lit [Smt.Formula]
make_lit cmp [t1; t2] creates the literal (t1 <cmp> t2).
make_literal [Prover]
make_real [Smt.Term]
make_real n creates an real constant of value n.
make_tau [Pre]
functional form of transition
make_var [Solver_types]
map [Bitv]
mapi [Bitv]
max_cands [Options]
max_forward [Options]
max_length [Bitv]
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_pred [Literal.S_Term]
mode [Options]
modulo [Polynome.T]
move_to [Vec]
mult [Polynome.S]
mult [Intervals]
mult [Polynome.T]
mult_const [Polynome.T]
mult_const [Types]

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]
nocolor [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 (#1, #2, #3, ...).
normal_form_pos [Polynome.T]
notyping [Options]
num_range [Options]
number [Variable]

O
of_int32_s [Bitv]
of_int32_us [Bitv]
of_int64_s [Bitv]
of_int64_us [Bitv]
of_int_s [Bitv]
of_int_us [Bitv]
of_list [Bitv]
of_list_with_length [Bitv]
of_nativeint_s [Bitv]
of_nativeint_us [Bitv]
of_satom [Types.ArrayAtom]
transforms a conjunction if the form of a set of atoms to an equivalent representation with an array
of_string [Bitv.M]
of_string [Bitv.L]
only_forward [Options]
open_dot [Dot]
origin [Node]
returns the origin of the node, i.e.
out_trace [Options]
output_bin [Bitv]

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 [Bwd.PriorityNodeQueue]
pop_ident [Enumsolver_types]
post_strategy [Options]
power [Intervals]
ppmc_denominators [Polynome.T]
pre_image [Pre]
pre-image tau n returns the pre-image of n by the transition relation tau as a disjunction of cubes in the form of two lists of new nodes.
print [Use.Make]
print [Ty]
print [Term]
print [Symbols]
print [Smt.Formula]
print fmt f prints the formula on the formatter fmt.
print [Smt.Variant]
print () will output the computed refined types on std_err.
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 [Bitv.M]
print [Bitv.L]
print [Hstring]
Prints a hash-consed strings on a formatter.
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_line [Pretty]
prints separating line
print_list [Hstring]
Prints a list of hash-consed strings on a formatter.
print_report [Stats]
prints a complete report.
print_subst [Variable]
print_title [Pretty]
prints section title for stats
print_vars [Variable]
proc_vars_int [Variable]
procs [Variable]
predefinied list of skolem variables #1, #2, #3, ...
profiling [Options]
pure_smt_check [Fixpoint.FixpointList]
Same as check but only uses the SMT solver.
push [Vec]
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]
reached vars s1 s2 raises Unsat if s2 has not been reached
real [Term]
real [Symbols]
red [Util]
refine [Options]
refine_universal [Options]
relevant [Instantiation]
relevant ~of_cube:a ~to_cube:b returns the list of relevant instantiations of the quantifiers of b for the test exists i1,... b => exists z1,... a.
remaining [Stats]
outputs number of remaining nodes in the queues given a function to count them.
remove [Polynome.T]
remove [Vec]
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_trace_and_expand [Enumerative]
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]
restore_state [Smt.Solver]
restore_state s restores a previously saved state s.
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]
save_state [Smt.Solver]
save_state () returns a copy of the current state of the solver.
scale [Intervals]
search [Forward]
search [Enumerative]
search procs init performs enumerative forward search.
search [Bwd.Strategy]
Backward reachability search on a system.
search_stateless [Forward]
set [Bitv]
set [Vec]
set_arith [Smt]
set_arith false deactivates the theory of arithmetic (true by default).
set_arith_active [Combine.CX]
set_cc [Smt]
set_cc false deactivates congruence closure algorithm (true by default).
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]
set_sum false deactivates the theory of enumerated data types (true by default).
set_sum_active [Combine.CX]
shiftl [Bitv]
shiftr [Bitv]
shrink [Vec]
simpl_by_uc [Options]
simplify [Cube]
simplify a cube.
simplify_atoms [Cube]
simplify a conjunction.
simplify_atoms_base [Cube]
simplify_atoms_base b c simplifies c in the context of b.
singleton [Explanation]
size [Vec]
size [Iheap]
size [Node]
returns the size of the associated cube (see Cube.size)
size [Cube]
returns the number of atoms in the conjuction
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 search.
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]
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]
sub [Bitv]
subset [Types.ArrayAtom]
subset a b returns true if the elements of a are a subsets of the elements contained in b.
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 and exit status of a unix command
system [Typing]
Types an untyped system and performs subtyping analysis is the flag Options.subtyping is true.

T
t_false [Smt.Term]
t_false is the boolean term false
t_true [Smt.Term]
t_true is the boolean term true
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_int32_s [Bitv]
to_int32_us [Bitv]
to_int64_s [Bitv]
to_int64_us [Bitv]
to_int_s [Bitv]
to_int_us [Bitv]
to_list [Polynome.T]
to_list [Bitv]
to_nativeint_s [Bitv]
to_nativeint_us [Bitv]
to_satom [Types.ArrayAtom]
returns the set of atoms corresponding to the conjuntion encoded in the array
to_string [Bitv.M]
to_string [Bitv.L]
trace [Options]
trivial_is_implied [Types.ArrayAtom]
trivial_is_implied [Types.Atom]
return true if it can be immediately said that the atom in the first argument implies the second
type_bool [Smt.Type]
The type of booleans
type_info [Sig.X]
type_info [Sig.COMBINATOR]
type_info [Sig.THEORY]
type_info [Polynome.T]
type_int [Smt.Type]
The type of integers
type_of [Smt.Symbol]
type_of x returns the type of x.
type_of [Types.Term]
returns the type of the term as it is known by the SMT solver
type_only [Options]
type_proc [Smt.Type]
The type processes (identifiers)
type_real [Smt.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
unsafe_get [Bitv]
unsafe_set [Bitv]
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 but only return skolemized variables of the form #i
variables_proc [Types.Atom]
same as variables but only return skolemized variables of the form #i
variables_proc [Types.Term]
same as variables but only return skolemized variables of the form #i
verbose [Options]
version [Version]
view [Term]
view [Literal.S]
view [Hstring]
view hs returns the string corresponding to hs.
vrai [Term]
vrai [Literal.S_Term]
vt_width [Pretty]
Width of the virtual terminal (80 if cannot be detected)

W
white [Util]