Index of values

check [Symkat]
utility for verifications: check two expressions for equivalence (`E), difference (`D), left-to-right inclusion (`L), or right-to-left inclusion (`G).
compare [Symkat]
full comparison: compare ~hyps x y returns `E if x and y are equivalent,, `L w if x is strictly contained in y (then w is a witness for strictness),, `G w if y is strictly contained in x (then w is a witness for strictness),, `D(w1,w2) if x and y are incomparable (then w1 is a witness against x<=y, and w2 is a witness against y<=x). Also return the actually compared terms, in symbolic form. Exploit hypotheses if asked to.
congruence [Symkat]
do we use up-to congruence
construction [Symkat]
which construction do we use

deriv [Brzozowski]
deriv [Antimirov]
partial derivatives
dfa [Brzozowski]
corresponding symbolic DFA
dot [Kat]

enfa [IlieYu]
corresponding automaton
epsilon [Kat]
output of a symbolic expression
equiv [Symkat]
equivalence check, using the above parameters; returns a counter-example if any.
expr [Parse]
parsing a string into a KAT expression
expr' [Kat]
from explicit expressions to (normalised) symbolic ones

hash [Kat]
hash of an expression
head [Kat]
top constructor of a symbolic KAT expression
hk [Symkat]
do we use Hopcroft and Karp's version?
hyps [Parse]
parsing a finite set of KAT equations (for hypothesis elimination)

nfa [Antimirov]
corresponding symbolic NFA

one [Kat]

pls [Kat]
smart constructors for symbolic KAT expressions: sums are sorted and associated to the left, consecutive tests are merged, duplicates and 0 are removed , products are associated to the left are simplified w.r.t. constants 0 and 1, and consecutive tests (on the left) are merged
print_expr [Kat]
print_expr' [Kat]
print_gstring [Kat]
print_test [Kat]
pretty-printing for tests and expressions

random_expr [Kat]
random_expr as ps n returns a random expression constructed from atomic tests in as and atomic Kleene elements in ps, with n connectives , with all negations at the leaves, without 0
random_full_expr [Kat]
random_full_expr as ps n returns a saturated random expression: a random expression as explained above, summed with the universal expression (\sum ps)*

split [Antimirov]
split a sum into a set of expressions
ssf [Symkat]
do we put expressions in strict star form first?
ssf [Kat]
putting an expression in strict star form: forall sub-expression of the shape e*, it is guaranted that e does not contain 1 (i.e., epsilon e!=top)
str [Kat]
subst [Kat]
term substitution

test_to_formula [Kat]
Conversion to Boolean BDD
tod [Kat]
trace [Symkat]
do we trace unifications in Format.str_formatter
tst [Kat]

var [Kat]
vars [Kat]
set of variables appearing in an expression

zer [Kat]