TODO

* Better way to deal with Integers: easier construction and printing (bin2int)
* Better multiplication than just repeated addition, re-try ladner-fischer
* Rename generate_var, generate_cnf to evaluate*
* Implement very simple clause caching/suppressing duplicate clauses
* Support integer division/subtraction by re-arranging parse tree into addition/multiplication
  instead of solving for the result.
* Generate a bash script for sat generation/solving/extracting
* Implement IsPrime predicate using Pratt certificates, drop into jane st. number cross 4
* Implement Formula.WriteCubedCnf(fd, vars)
* Make NumTrue auto-convert to NumFalse and vise-versa when appropriate with fixed integers
* Add a Formula.WriteBlocker method to write a blocking solution extractor
* NumTrue/NumFalse are specialized for comparisons with int so that "NumTrue(*varz) >= Integer(1)"
  sums up all the variables in varz that are true and compares it to the binary representation of 1,
  but "NumTrue(*varz) >= 1" generates something simpler like an OR of varz. For larger int, we will
  generate a selection network, but it's not clear if that's more efficient that just computing the
  sum of the varz. Test and remove all the selection network code if it isn't dramatically more
  efficient.
* Support negative integers with twos-complement representation.