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 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
|
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] |
low-level 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] |
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] | |
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] |
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] | |
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] |