Module Kat

module Kat: sig .. end

Kleene algebra with tests (KAT) expressions

type var = char

type gstring = (var, Bdd.key) Common.gstring

val print_gstring : gstring Common.formatter

type 's mem = ('s, Bdd.key) Bdd.mem

type 's node = ('s, Bdd.key) Bdd.node

type 'a span = (var, 'a) Common.span

type test =

`\|`	`Dsj of test * test`
`\|`	`Cnj of test * test`
`\|`	`Neg of test`
`\|`	`Top`
`\|`	`Bot`
`\|`	`Prd of Bdd.key`

Explicit Boolean formula

val test_to_formula : test -> Bdd.formula

Conversion to Boolean BDD

type ('o, 'e) expr_ =

`\|`	`Pls of 'e * 'e`
`\|`	`Dot of 'e * 'e`
`\|`	`Str of 'e`
`\|`	`Tst of 'o`
`\|`	`Var of var`

generic KAT constructors

type expr = (test, expr) expr_

explicit KAT expression

type abstr

symbolic KAT expressions (hash-consed, otherwise abstract)

type expr' = abstr Common.hval

type expr'_set = abstr Common.hset

sets of symbolic expressions

val hash : expr' -> int

hash of an expression

val head : expr' -> (Bdd.formula, expr') expr_

top constructor of a symbolic KAT expression

val subst : (var -> expr') -> expr' -> expr'

term substitution

val vars : expr' -> var Common.set

set of variables appearing in an expression

val pls : expr' -> expr' -> expr'

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

val dot : expr' -> expr' -> expr'

val tod : expr' -> expr' -> expr'

val str : expr' -> expr'

val tst : Bdd.formula -> expr'

val var : char -> expr'

val zer : expr'

val one : expr'

val expr' : expr -> expr'

from explicit expressions to (normalised) symbolic ones

val epsilon : expr' -> Bdd.formula

output of a symbolic expression

val ssf : expr' -> expr'

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)

val print_test : Format.formatter -> test -> unit

pretty-printing for tests and expressions

val print_expr : Format.formatter -> expr -> unit

val print_expr' : Format.formatter -> expr' -> unit

val random_expr : Bdd.key list -> var list -> int -> unit -> expr

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

val random_full_expr : Bdd.key list -> var list -> int -> unit -> expr

random_full_expr as ps n returns a saturated random expression: a random expression as explained above, summed with the universal expression (\sum ps)*