From e3b88631ef58ad406ac069bd3a4ba16fb4aa07cc Mon Sep 17 00:00:00 2001 From: "Hoang M. Le" Date: Thu, 1 Jun 2017 12:09:02 +0200 Subject: hide backend solver declarations from public include --- include/klee/Solver.h | 58 -------------------------------------------- lib/Solver/CoreSolver.cpp | 3 +++ lib/Solver/MetaSMTSolver.cpp | 1 + lib/Solver/MetaSMTSolver.h | 32 ++++++++++++++++++++++++ lib/Solver/STPSolver.cpp | 1 + lib/Solver/STPSolver.h | 39 +++++++++++++++++++++++++++++ lib/Solver/Z3Solver.cpp | 1 + lib/Solver/Z3Solver.h | 34 ++++++++++++++++++++++++++ 8 files changed, 111 insertions(+), 58 deletions(-) create mode 100644 lib/Solver/MetaSMTSolver.h create mode 100644 lib/Solver/STPSolver.h create mode 100644 lib/Solver/Z3Solver.h diff --git a/include/klee/Solver.h b/include/klee/Solver.h index 7f12ddfb..e669c6f4 100644 --- a/include/klee/Solver.h +++ b/include/klee/Solver.h @@ -203,64 +203,6 @@ namespace klee { virtual void setCoreSolverTimeout(double timeout); }; -#ifdef ENABLE_STP - /// STPSolver - A complete solver based on STP. - class STPSolver : public Solver { - public: - /// STPSolver - Construct a new STPSolver. - /// - /// \param useForkedSTP - Whether STP should be run in a separate process - /// (required for using timeouts). - /// \param optimizeDivides - Whether constant division operations should - /// be optimized into add/shift/multiply operations. - STPSolver(bool useForkedSTP, bool optimizeDivides = true); - - /// getConstraintLog - Return the constraint log for the given state in CVC - /// format. - 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_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 - class MetaSMTSolver : public Solver { - public: - MetaSMTSolver(bool useForked, bool optimizeDivides); - virtual ~MetaSMTSolver(); - - virtual char *getConstraintLog(const Query&); - virtual void setCoreSolverTimeout(double timeout); - }; - - /// createMetaSMTSolver - Create a solver using the metaSMT backend set by - /// the option MetaSMTBackend. - Solver *createMetaSMTSolver(); - -#endif /* ENABLE_METASMT */ - /* *** */ /// createValidatingSolver - Create a solver which will validate all query diff --git a/lib/Solver/CoreSolver.cpp b/lib/Solver/CoreSolver.cpp index 72b82807..438f38f6 100644 --- a/lib/Solver/CoreSolver.cpp +++ b/lib/Solver/CoreSolver.cpp @@ -7,6 +7,9 @@ // //===----------------------------------------------------------------------===// +#include "STPSolver.h" +#include "Z3Solver.h" +#include "MetaSMTSolver.h" #include "klee/CommandLine.h" #include "klee/Internal/Support/ErrorHandling.h" #include "klee/Solver.h" diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp index 3b3eaf35..9b49f995 100644 --- a/lib/Solver/MetaSMTSolver.cpp +++ b/lib/Solver/MetaSMTSolver.cpp @@ -9,6 +9,7 @@ #include "klee/Config/config.h" #ifdef ENABLE_METASMT +#include "MetaSMTSolver.h" #include "MetaSMTBuilder.h" #include "klee/Constraints.h" #include "klee/Internal/Support/ErrorHandling.h" diff --git a/lib/Solver/MetaSMTSolver.h b/lib/Solver/MetaSMTSolver.h new file mode 100644 index 00000000..60d72383 --- /dev/null +++ b/lib/Solver/MetaSMTSolver.h @@ -0,0 +1,32 @@ +//===-- MetaSMTSolver.h +//---------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_METASMTSOLVER_H +#define KLEE_METASMTSOLVER_H + +#include "klee/Solver.h" + +namespace klee { + +template class MetaSMTSolver : public Solver { +public: + MetaSMTSolver(bool useForked, bool optimizeDivides); + virtual ~MetaSMTSolver(); + + virtual char *getConstraintLog(const Query &); + virtual void setCoreSolverTimeout(double timeout); +}; + +/// createMetaSMTSolver - Create a solver using the metaSMT backend set by +/// the option MetaSMTBackend. +Solver *createMetaSMTSolver(); +} + +#endif /* KLEE_METASMTSOLVER_H */ diff --git a/lib/Solver/STPSolver.cpp b/lib/Solver/STPSolver.cpp index 5893c28e..d1b8cbdc 100644 --- a/lib/Solver/STPSolver.cpp +++ b/lib/Solver/STPSolver.cpp @@ -8,6 +8,7 @@ //===----------------------------------------------------------------------===// #include "klee/Config/config.h" #ifdef ENABLE_STP +#include "STPSolver.h" #include "STPBuilder.h" #include "klee/Solver.h" #include "klee/SolverImpl.h" diff --git a/lib/Solver/STPSolver.h b/lib/Solver/STPSolver.h new file mode 100644 index 00000000..cb68ed91 --- /dev/null +++ b/lib/Solver/STPSolver.h @@ -0,0 +1,39 @@ +//===-- STPSolver.h +//---------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_STPSOLVER_H +#define KLEE_STPSOLVER_H + +#include "klee/Solver.h" + +namespace klee { +/// STPSolver - A complete solver based on STP. +class STPSolver : public Solver { +public: + /// STPSolver - Construct a new STPSolver. + /// + /// \param useForkedSTP - Whether STP should be run in a separate process + /// (required for using timeouts). + /// \param optimizeDivides - Whether constant division operations should + /// be optimized into add/shift/multiply operations. + STPSolver(bool useForkedSTP, bool optimizeDivides = true); + + /// getConstraintLog - Return the constraint log for the given state in CVC + /// format. + virtual char *getConstraintLog(const Query &); + + /// setCoreSolverTimeout - Set constraint solver timeout delay to the given + /// value; 0 + /// is off. + virtual void setCoreSolverTimeout(double timeout); +}; +} + +#endif /* KLEE_STPSOLVER_H */ diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp index c8af7e9e..985c143d 100644 --- a/lib/Solver/Z3Solver.cpp +++ b/lib/Solver/Z3Solver.cpp @@ -10,6 +10,7 @@ #include "klee/Internal/Support/ErrorHandling.h" #include "klee/Internal/Support/FileHandling.h" #ifdef ENABLE_Z3 +#include "Z3Solver.h" #include "Z3Builder.h" #include "klee/Constraints.h" #include "klee/Solver.h" diff --git a/lib/Solver/Z3Solver.h b/lib/Solver/Z3Solver.h new file mode 100644 index 00000000..8dc97e06 --- /dev/null +++ b/lib/Solver/Z3Solver.h @@ -0,0 +1,34 @@ +//===-- Z3Solver.h +//---------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_Z3SOLVER_H +#define KLEE_Z3SOLVER_H + +#include "klee/Solver.h" + +namespace klee { +/// 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 /* KLEE_Z3SOLVER_H */ -- cgit 1.4.1