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, 18 insertions, 1 deletions

diff --git a/include/klee/Solver.h b/include/klee/Solver.h
index fed6191a..c82ab135 100644
--- a/include/klee/Solver.h
+++ b/include/klee/Solver.h
@@ -225,7 +225,24 @@ namespace klee {
   };
 #endif // ENABLE_STP
 
-  
+#ifdef ENABLE_Z3
+  /// Z3Solver - A solver complete solver based on Z3
+  class Z3Solver : public Solver {
+  public:
+    /// Z3Solver - Construct a new Z3Solver.
+    Z3Solver();
+
+    /// Get the query in SMT-LIBv2 format.
+    /// \return A C-style string. The caller is responsible for freeing this.
+    virtual char *getConstraintLog(const Query &);
+
+    /// setCoreSolverTimeout - Set constraint solver timeout delay to the given
+    /// value; 0
+    /// is off.
+    virtual void setCoreSolverTimeout(double timeout);
+  };
+#endif // ENABLE_Z3
+
 #ifdef ENABLE_METASMT
   
   template<typename SolverContext>