From 1f13e9dbf9db2095b6612a47717c2b86e4aaba72 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 26 Jan 2016 17:15:08 +0000 Subject: 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. --- include/klee/Solver.h | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) (limited to 'include') 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 -- cgit 1.4.1