Estimate constraint difficulty using #SAT

[jryans]

We currently don't have any good way to estimate the difficultly of constraints. Being able to have a way of estimating difficultly would hopefully provide a way for us to understand the performance differences of JFS on different constraints.

A way we could do this take constraints, convert floating-point operations to bitvector operations, then bit blast to a sat problem, and then use a SAT model counting (#SAT) tool to count the number of satisfiable models. The number of satisfiable models divided by the number of all possible models gives the probability of guessing (uniform random) a satisfiable model.