QF_NRA prototype

[paultristanwagner]

Implements a CAD (cylindrical algebraic decomposition) based protoype for solving quantifier-free non-linear real arithmetic.
The feature set is highly experimental and may still contain bugs.

Examples:

> smt QF_NRA (x^2 + y^2 = 1) & (x^2 + y^3 = 1/2)
SAT:
x=(x^6-2x^4+2x^2-3/4, 3/4, 15/16) ≈ 0.8249554777467228; y=(x^9+1/2x^6+3/4x^3+1/8, -7/4, 7/4) ≈ -0.5651977173836394;
Time: 456ms

> smt QF_NRA (x*y > 0) & (y*z > 0) & (x*z > 0) & (x + y + z = 0)
UNSAT
Time: 7ms