More optimizations and usability enhancements

- Support different variable sizes, which lets us support other SMT formulas
- Move the counter seeding into the GPU for faster startup
- Some tweaks so that the jfs C++ code doesn't need as many modifications

Author: moyix

SMTLIB/BitVector.h

@@ -38,7 +38,7 @@ class BitVector<
   constexpr dataTy mask() const {
     return (N >= 64) ? UINT64_MAX : ((UINT64_C(1) << N) - 1);
   }
-  dataTy doMod(dataTy value) const {
+  __device__ dataTy doMod(dataTy value) const {
     if (N >= 64)
       return value;
     else

TODO.txt

@@ -2,7 +2,16 @@
     - Mostly done
     - Still need to figure out the nearest int routines
 * LOL what are unit tests
+* Make it easier to run different SMT formulas
+    - John has this in his branch, just need to integrate
+* Figure out how to count executions / second
+* Performance measurement & optimization
+
+DONE:
 * Find a harder SMT formula
+    - Done
 * Generalize to more variables
+    - Done!
 * Support multiple GPUs
     - Done!
+

cuda_aes.h

@@ -3,4 +3,4 @@
 
 __host__   void expand_key(uint8_t *key, uint8_t *rkey);
 __device__ void encrypt_k(uint8_t *data, const uint8_t *rkey, uint32_t numblock);
-
+__device__ void encrypt_one_table(uint8_t *block, const uint8_t *rkey, uint32_t offset);