Index of values

add [Common.Set]
add [Sets.T]

binary [Bdd]
applying a binary function to two BDDs (the standard "apply" function)
bot [Bdd]
the two constants

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

diff [Common.Set]
diff [Sets.T]
dsj [Bdd]

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]

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]

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

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

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 non-trivial 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

leaf [Trace]
leaf_t [Trace]
line [Trace]

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

neg [Bdd]
the various connectives
next_line [Common]
Utilities for lexing/parsing
node [Bdd]
low-level node creation function, variable ordering is not enforced
node [Trace]
node_l [Trace]
node_r [Trace]

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

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]
pretty-printing a symbolic formula (the first argument specifies the current level, for parentheses)
print_gstring [Common]
pretty-printing for guarded strings
push [Common.QUEUE]

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]

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]

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

unary [Bdd]
applying a unary function to a BDD
unexpected_char [Common]
unify_dsf [Bdd]
union-find 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]

var [Bdd]
literals: a single variable, or the negation of a variable

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

xor [Bdd]