using functors now.  need an mli file.
Sat is now parameterized on ints
new non-segfauling axioms