Confluence check: improve debug output to show what it is doing, and how it reached it conclusions
Currently, debug output is very limited. It only prints a few lines at the end of the check, with the conclusion.
There is more debug output, but this needs to be enabled in the code. I propose to change some of that to normal debug output, to show what checks (mutual exclusiveness, update equivalence, etc) is being checked, etc.
We should then print normal BDD debug output, like we do with other BDD-based checks, and during data-based synthesis, rather than the internal representation of BDD.toString
. This may be tricky if the predicate has zero variables, as BddUtils.bddToStr
can't handle those, currently.
Addresses #892