Module Automata.SNFA

module SNFA: sig .. end
symbolic non-deterministic automata

type ('s, 'set, 'v, 'k, 'o) t = {
   m : ('set, 'k) Bdd.mem;
   t : 's -> ('v, ('set, 'k) Bdd.node) Common.span;
   o : 's -> 'o;
   o0 : 'o;
   o2 : 'o -> 'o -> 'o;
   state_info : 's Common.formatter;
reindex and memoise an NFA
val reindex : ('s Common.hval, 's Common.hset, 'v, 'k, 'o) t ->
(int, Common.int_set, 'v, 'k, 'o) t *
('s Common.hset -> Common.int_set)
number of states and Bdd internal nodes reachable from the given set of states
val size : (int, Common.int_set, 'a, 'b, 'c) t ->
Common.int_set -> int * int