Support for solving constraints on reals

I have recently added support for generating constraints on reals in ATS.

The generated constraints can be exported for solving via Z3:

https://github.com/githwxi/ATS-Postiats-contrib/blob/master/projects/MEDIUM/ATS-extsolve-z3/

Here is an example verifying the two solutions to a quadratic equation:

https://github.com/githwxi/ATS-Postiats-contrib/blob/master/projects/MEDIUM/ATS-extsolve-z3/TEST/quadratic.dats

There are a few lines in the following script showing how patsolve_z3 can
be built:

Cheers!

–Hongwei