Improved the external constraint solver 'patsolve'

Added some documentation in the readme describing how to run the new constraint solver.

Improvements to the project include:

  - embedded python interpreter for running user Z3 scripts
  - more support for bit vectors and reals
  - moving all of our examples from the previous paper into the contrib/libats-/wdblair/prelude/{DATS,TEST}