Add solver that deduces facts using unit propagation

This unit propagation algorithms is not very efficient but it
allows us to experiment with abstraction techniques and get a
sense for the overhead of traversing the expression tree.

The BDD code was removed because the overhead of these data
structures is just to great for practical purposes.