Drastically improve performances by simplifying the book-keeping
of pending transitions during a topdown run.
Before:
- we were keeping for each node
(1) sat: the set of states satisfied at that node
(2) unsat: the set of states unsatisfied at that node
(3) todo: the hashconsed list of pending transitions (of the
form q, {a,b,c} -> f
where f has been simplified w.r.t to sat and unsat (that is
atoms containing states in either have been simplified to True
or False) and q is neither in sat nor unsat.
- during each run, for each node, we were scanning todo and rebuilding
it removing satisfied or unsatisfied transitions. This lead to excessive
hashconsing, and a lot of time spent in the hashconsing module (in turn
spending a lot of time in the GC)
After:
- we keep for each node:
(1) sat: the set of states satisfied at that node
(2) todo: the set of undetermined *states*
- we perform the book-keeping as before but do not materialize the
simplified transitions. Also unsat is made inplicit (a state is
unsat if it is neither in sat nor todo).