C | |
| 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
|
D | |
| deriv [Brzozowski] |
derivatives
|
| deriv [Antimirov] |
partial derivatives
|
| dfa [Brzozowski] |
corresponding symbolic DFA
|
| dot [Kat] | |
E | |
| 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
|
H | |
| 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)
|
N | |
| nfa [Antimirov] |
corresponding symbolic NFA
|
O | |
| one [Kat] | |
P | |
| 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
|
R | |
| 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)*
|
S | |
| 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
|
T | |
| test_to_formula [Kat] |
Conversion to Boolean BDD
|
| tod [Kat] | |
| trace [Symkat] |
do we trace unifications in
Format.str_formatter
|
| tst [Kat] | |
V | |
| var [Kat] | |
| vars [Kat] |
set of variables appearing in an expression
|
Z | |
| zer [Kat] |