Index of values

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_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_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]
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

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_constr s cstr will add the constraint that the constructor cstr must be in the type of s

assign_var [Smt_sig.S.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 [Smt_sig.S.Solver]

assume id f adds the formula f to the context of the solver with identifier id.

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 but without the solver check

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

assume_node_no_check [Prover]

Same as assume_node but without the solver check

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 (Bwd).

brab_up_to [Options]
build_subst [Variable]

constructs a variable substitution

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 [Smt_sig.S.Solver]

check () runs the solver on its context.

check [Safety]

check s n raises Unsafe n if the node n is immediately reachable in the system s, i.e.

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

check_strategy [Smt_sig.S.Solver]

The stragey used for preforming check-sat.

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 () clears the context of the solver.

clear [Bwd.PriorityNodeQueue]
close [Smt_sig.S.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 [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 [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 l1 l2 returns 0 if and only if l1 is equal to l2.

compare_list [Variable]
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]
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]

constructors ty returns the list of constructors of ty when type is an enumerated data-type, otherwise returns [].

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 s [arg_1; ... ; arg_n] out declares a new function symbol with type (arg_1, ... , arg_n) -> out

declare [Smt_sig.S.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_sig.S.Symbol]

declared x is true if x is already declared.

declared_types [Smt_sig.S.Type]
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 [Hstring]

the empty ("") hash-consed string.

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 Murphi.mk_encoding_table

enqueue_ident [Enumsolver_types]
entails [Smt_sig.S.Solver]

entails f returns true if the context of the solver entails the formula f.

enumerative [Options]
enumsolver [Options]
env [Muparser_globals]
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 [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 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_sig.S.Formula]

The formula which represents false

f_true [Smt_sig.S.Formula]

The formula which represents true

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_calls () returns the cumulated number of calls to Smt_sig.S.Solver.check.

get_time [Smt_sig.S.Solver]

get_time () returns the cumulated time spent in the solver in seconds.

get_variants [Smt_sig.S.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.

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_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_sig.S.Symbol]

has_infinite_type x is true if the type of x is not finite.

has_type_proc [Smt_sig.S.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 [Hstring]

hash x returns the integer (hash) associated to x.

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 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 [Vec]
init [Iheap]
init [Smt_sig.S.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 [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_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_sig.S.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 [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.

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 x l returns the element associated with x in the list of pairs l.

list_assoc_inv [Hstring]

list_assoc_inv x l returns the first element which is associated to 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 [Vec]
make [Hstring]

make s builds ans returns a hash-consed string from s.

make [Term]
make [Smt_sig.S.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_app [Smt_sig.S.Term]

make_app f l creates the application of function symbol f to a list of terms l.

make_arith [Smt_sig.S.Term]

make_arith op t1 t2 creates the term t1 <op> t2.

make_clause [Enumsolver_types]
make_clause [Solver_types]
make_cnf [Smt_sig.S.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_sig.S.Term]

make_int n creates an integer constant of value n.

make_lit [Smt_sig.S.Formula]

make_lit cmp [t1; t2] creates the literal (t1 <cmp> t2).

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

make_real n creates an real constant of value n.

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_env nb sys creates an environment for the enumerative exploration of the transition system sys with a fixed number nb of processes.

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 Mulexer

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 (#1, #2, #3, ...).

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]

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 [Hstring]

Prints a hash-consed strings on a formatter.

print [Use.Make]
print [Ty]
print [Term]
print [Symbols]
print [Smt_sig.S.Formula]

print fmt f prints the formula on the formatter fmt.

print [Smt_sig.S.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 [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 hash-consed strings on a formatter.

print_list [Pretty]

print_list f sep fmt l prints list l whose elements are printed with f, each of them being separated by the separator sep.

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 p a fmt sys prints the system sys in Murphi's syntax with p processes and infinite types abstracted with the subrange [1;a].

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 #1, #2, #3, ...

profiling [Options]
psystem_of_decls [Ptree]
pure_smt_check [Fixpoint.FixpointList]

Same as check but only uses the SMT solver.

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]

reached vars s1 s2 raises Unsat if s2 has not been reached

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]

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 [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 procs init performs enumerative forward search.

search [Bwd.Strategy]

Backward reachability search on a system.

search_stateless [Forward]
set [Vec]
set_arith [Smt_sig.S]

set_arith false deactivates the theory of arithmetic (true by default).

set_arith_active [Combine.CX]
set_cc [Smt_sig.S]

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_sig.S]

set_sum false deactivates the theory of enumerated data types (true by default).

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]

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_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 search.

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 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 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 Options.subtyping is true.

T
t_false [Smt_sig.S.Term]

t_false is the boolean term false

t_true [Smt_sig.S.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_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 true if it can be immediately said that the atom in the first argument implies the second

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 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_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 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 [Hstring]

view hs returns the string corresponding to hs.

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 true if the substitution is well formed, i.e.

white [Util]