A  
add [Common.Set]  
add [Sets.T]  
B  
binary [Bdd] 
applying a binary function to two BDDs (the standard "apply" function)

bot [Bdd] 
the two constants

C  
cardinal [Common.Set]  
cardinal [Sets.T]  
ce [Trace]  
clear [Trace]  
cnj [Bdd]  
compare [Sets.T]  
constant [Bdd] 
constant BDD (leaf)

count_calls [Stats] 
count the calls to the given function, under the given name

counter [Stats] 
create a new counter with the given name

D  
diff [Common.Set]  
diff [Sets.T]  
dsj [Bdd]  
E  
empty [Congruence.Make]  
empty [Common.QUEUE]  
empty [Common.Span]  single p x z is map whose value is x on p and z everywhere else

empty [Common.Set]  
empty [Sets.T]  
entry [Trace]  
equal [Sets.T]  
equiv [Safa.Make]  
equiv_c [Safa.Make] 
same algorithms, further enhanced using up to congruence

exists [Common.Set]  
exists [Sets.T]  
F  
filter [Common.Set]  
filter [Sets.T]  
fold [Common.QUEUE]  
fold [Common.Set]  
fold [Sets.T]  
for_all [Common.Set]  
forall [Sets.T]  
full [Sets.T]  
G  
generic [Determinisation] 
simple, generic determinisation, using
Common.Set sets

generic_output_check [Automata.SDFA]  
get [Stats] 
getting the value of a counter

get [Common.Span]  
get [Common] 
wrapper around
Hashtbl.find

H  
hash [Bdd] 
hash of a BDD node

hash [Sets.T]  
head [Bdd] 
explicit description of a given node

hide [Bdd] 
hide a given key, by using the given function to resolve choices

I  
iff [Bdd]  
incr [Stats] 
increment a counter

init [Bdd] 
empty memory, with given hash and equality functions for leaves

inter [Common.Set]  
inter [Sets.T]  
intersect [Sets.T]  
is_empty [Common.Set]  
is_empty [Sets.T]  
iter [Common.Span]  iter2 f m n applies f to all nontrivial pairs obtained by zipping m and n

iter [Common.Set]  
iter [Sets.T]  
iter2 [Common.Span]  get m p returns the value of the map m on p

L  
leaf [Trace]  
leaf_t [Trace]  
line [Trace]  
M  
map [Common.Span] 
simple iterator

map [Common.Set]  
map [Sets.T]  
mem [Common.Set]  
mem [Sets.T]  
memo_rec [Common] 
memoisation utilities

memo_rec1 [Common]  
memo_rec2 [Common]  
merge [Common.Span] 
pointwise application of a function

N  
neg [Bdd] 
the various connectives

next_line [Common] 
Utilities for lexing/parsing

node [Bdd] 
lowlevel node creation function, variable ordering is not enforced

node [Trace]  
node_l [Trace]  
node_r [Trace]  
O  
of_list [Sets.T]  
ok [Trace]  
optimised [Determinisation] 
more efficient determinisation, using
IntSet instead

P  
paren [Common] 
utility for formatting parenthesised expressions

parse [Common]  
partial_apply [Bdd] 
partially apply a BDD, by using the given function to resolve nodes

pop [Common.QUEUE]  
print [Stats] 
print the status of all counters

print [Common.Set]  
print [Sets.T]  
print' [Sets.T]  
print_formula [Bdd] 
prettyprinting a symbolic formula (the first argument specifies
the current level, for parentheses)

print_gstring [Common] 
prettyprinting for guarded strings

push [Common.QUEUE]  
R  
random [Sets.T]  
rav [Bdd]  
reindex [Automata.SNFA] 
number of states and Bdd internal nodes reachable from the given set of states

rem [Common.Set]  
rem [Sets.T]  
remove [Epsilon] 
convert a symbolic NFA with epsilon transitions into a symbolic NFA

render [Trace]  
reset [Stats] 
reset all counters

reset_caches [Bdd] 
reset all memoisation caches

restore [Trace]  
S  
save [Trace]  
set_compare [Sets.T]  
shift [Sets.T]  
single [Common.Span]  merge f m n applies f pointwise to m and n ,
assume that m and z share the same default value z ,
and that f z z = z

singleton [Common.QUEUE]  
singleton [Common.Set]  
singleton [Sets.T]  
size [Automata.SNFA]  
size [Automata.SDFA] 
generic output check: outputs are computed and copmared physically

size [Sets.T]  
skip [Trace]  
subset [Common.Set]  
subseteq [Sets.T]  
T  
tag [Bdd] 
identifier of a BDD node (unique w.r.t.

time [Common] 
simple timing function

times [Bdd]  times m z f n multiplies the BDD n by the formula f ,
using z where f is false

to_list [Sets.T]  
top [Bdd]  
trace [Automata.SDFA] 
number of states and Bdd internal nodes reachable from the given list of states

U  
unary [Bdd] 
applying a unary function to a BDD

unexpected_char [Common]  
unify_dsf [Bdd] 
unionfind based unifier where a forest of pointers is stored.

unify_naive [Bdd] 
naive unifier where a set of pairs of nodes is stored.

union [Common.Set]  
union [Sets.T]  
V  
var [Bdd] 
literals: a single variable, or the negation of a variable

W  
walk [Bdd] 
walking recursively through a BDD, ensuring that a given node is visited at most once

witness [Bdd] 
witness assignation for a satisfiable formula

X  
xor [Bdd] 