diff options
Diffstat (limited to 'lib/Solver/MetaSMTSolver.cpp')
-rw-r--r-- | lib/Solver/MetaSMTSolver.cpp | 34 |
1 files changed, 18 insertions, 16 deletions
diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp index 37c22f0e..c3c6dfaa 100644 --- a/lib/Solver/MetaSMTSolver.cpp +++ b/lib/Solver/MetaSMTSolver.cpp @@ -51,6 +51,8 @@ #undef type_t #endif +#include <memory> + #include <errno.h> #include <signal.h> #include <sys/ipc.h> @@ -85,7 +87,6 @@ private: public: MetaSMTSolverImpl(MetaSMTSolver<SolverContext> *solver, bool useForked, bool optimizeDivides); - virtual ~MetaSMTSolverImpl(); char *getConstraintLog(const Query &); void setCoreSolverTimeout(time::Span timeout) { _timeout = timeout; } @@ -134,9 +135,6 @@ MetaSMTSolverImpl<SolverContext>::MetaSMTSolverImpl( } template <typename SolverContext> -MetaSMTSolverImpl<SolverContext>::~MetaSMTSolverImpl() {} - -template <typename SolverContext> char *MetaSMTSolverImpl<SolverContext>::getConstraintLog(const Query &) { const char *msg = "Not supported"; char *buf = new char[strlen(msg) + 1]; @@ -404,8 +402,8 @@ MetaSMTSolverImpl<SolverContext>::getOperationStatusCode() { template <typename SolverContext> MetaSMTSolver<SolverContext>::MetaSMTSolver(bool useForked, bool optimizeDivides) - : Solver(new MetaSMTSolverImpl<SolverContext>(this, useForked, - optimizeDivides)) {} + : Solver(std::make_unique<MetaSMTSolverImpl<SolverContext>>( + this, useForked, optimizeDivides)) {} template <typename SolverContext> MetaSMTSolver<SolverContext>::~MetaSMTSolver() {} @@ -420,45 +418,50 @@ void MetaSMTSolver<SolverContext>::setCoreSolverTimeout(time::Span timeout) { impl->setCoreSolverTimeout(timeout); } -Solver *createMetaSMTSolver() { +std::unique_ptr<Solver> createMetaSMTSolver() { using namespace metaSMT; - Solver *coreSolver = NULL; + std::unique_ptr<Solver> coreSolver; std::string backend; switch (MetaSMTBackend) { #ifdef METASMT_HAVE_STP case METASMT_BACKEND_STP: backend = "STP"; - coreSolver = new MetaSMTSolver<DirectSolver_Context<solver::STP_Backend> >( + coreSolver = std::make_unique< + MetaSMTSolver<DirectSolver_Context<solver::STP_Backend>>>( UseForkedCoreSolver, CoreSolverOptimizeDivides); break; #endif #ifdef METASMT_HAVE_Z3 case METASMT_BACKEND_Z3: backend = "Z3"; - coreSolver = new MetaSMTSolver<DirectSolver_Context<solver::Z3_Backend> >( + coreSolver = std::make_unique< + MetaSMTSolver<DirectSolver_Context<solver::Z3_Backend>>>( UseForkedCoreSolver, CoreSolverOptimizeDivides); break; #endif #ifdef METASMT_HAVE_BTOR case METASMT_BACKEND_BOOLECTOR: backend = "Boolector"; - coreSolver = new MetaSMTSolver<DirectSolver_Context<solver::Boolector> >( + coreSolver = std::make_unique< + MetaSMTSolver<DirectSolver_Context<solver::Boolector>>>( UseForkedCoreSolver, CoreSolverOptimizeDivides); break; #endif #ifdef METASMT_HAVE_CVC4 case METASMT_BACKEND_CVC4: backend = "CVC4"; - coreSolver = new MetaSMTSolver<DirectSolver_Context<solver::CVC4> >( - UseForkedCoreSolver, CoreSolverOptimizeDivides); + coreSolver = + std::make_unique<MetaSMTSolver<DirectSolver_Context<solver::CVC4>>>( + UseForkedCoreSolver, CoreSolverOptimizeDivides); break; #endif #ifdef METASMT_HAVE_YICES2 case METASMT_BACKEND_YICES2: backend = "Yices2"; - coreSolver = new MetaSMTSolver<DirectSolver_Context<solver::Yices2> >( - UseForkedCoreSolver, CoreSolverOptimizeDivides); + coreSolver = + std::make_unique<MetaSMTSolver<DirectSolver_Context<solver::Yices2>>>( + UseForkedCoreSolver, CoreSolverOptimizeDivides); break; #endif default: @@ -468,6 +471,5 @@ Solver *createMetaSMTSolver() { klee_message("Starting MetaSMTSolver(%s)", backend.c_str()); return coreSolver; } - } #endif // ENABLE_METASMT |