Add basic implementation of Z3Builder and Z3Solver and Z3SolverImpl

which is based on the work of Andrew Santosa (see PR #295) but fixes
many bugs in that implementation. The implementation communicates
with Z3 via it's C API.

This implementation is based of the STPSolver and STPBuilder and so it
inherits a lot of its flaws (See TODOs and FIXMEs). I have also ripped
out some of the optimisations (constructMulByConstant,
constructSDivByConstant and constructUDivByConstant) that were used in
the STPBuilder because

* I don't trust them
* Z3 can probably do these for us in the future if we use the
 ``Z3_simplify()``

At a glance its performance seems worse than STP but future work can
look at improving this.

1 files changed, 1 insertions, 3 deletions

diff --git a/lib/Solver/CoreSolver.cpp b/lib/Solver/CoreSolver.cpp
index 26842d31..94bb3a5e 100644
--- a/lib/Solver/CoreSolver.cpp
+++ b/lib/Solver/CoreSolver.cpp
@@ -88,9 +88,7 @@ Solver *createCoreSolver(CoreSolverType cst) {
     return createDummySolver();
   case Z3_SOLVER:
 #ifdef ENABLE_Z3
-    // TODO
-    llvm::report_fatal_error("Z3 support not implemented");
-    return NULL;
+    return new Z3Solver();
 #else
     llvm::errs() << "Not compiled with Z3 support\n";
     return NULL;