Support for solving constraints on reals

[gmhwxi]

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:

https://github.com/ats-lang/ats-lang.github.io/blob/master/SCRIPT/C9-ATS2-install-cs520-z3.sh

Cheers!

--Hongwei