diff options
author | Daniel Schemmel <daniel@schemmel.net> | 2023-03-24 02:50:22 +0000 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2023-04-21 13:07:31 +0100 |
commit | e9d77be6c688836d68a2be5f3f0a02e63f392bb8 (patch) | |
tree | 2e7d1d55b122df555ec51ef0a0f3ee1cd856e64c | |
parent | 4d59fe9aef258c35212e5b7b9f6eb2e17b88d293 (diff) | |
download | klee-e9d77be6c688836d68a2be5f3f0a02e63f392bb8.tar.gz |
use unique_ptr in Solver
-rw-r--r-- | include/klee/Solver/Solver.h | 12 | ||||
-rw-r--r-- | lib/Solver/Solver.cpp | 5 |
2 files changed, 5 insertions, 12 deletions
diff --git a/include/klee/Solver/Solver.h b/include/klee/Solver/Solver.h index a2256028..2689d19c 100644 --- a/include/klee/Solver/Solver.h +++ b/include/klee/Solver/Solver.h @@ -14,6 +14,7 @@ #include "klee/System/Time.h" #include "klee/Solver/SolverCmdLine.h" +#include <memory> #include <vector> namespace klee { @@ -58,10 +59,6 @@ namespace klee { }; class Solver { - // DO NOT IMPLEMENT. - Solver(const Solver&); - void operator=(const Solver&); - public: enum Validity { True = 1, @@ -69,15 +66,12 @@ namespace klee { Unknown = 0 }; - public: /// validity_to_str - Return the name of given Validity enum value. static const char *validity_to_str(Validity v); - public: - SolverImpl *impl; + std::unique_ptr<SolverImpl> impl; - public: - Solver(SolverImpl *_impl) : impl(_impl) {} + Solver(SolverImpl *impl); virtual ~Solver(); /// evaluate - Determine for a particular state if the query diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp index 5fe973fe..e123a667 100644 --- a/lib/Solver/Solver.cpp +++ b/lib/Solver/Solver.cpp @@ -22,9 +22,8 @@ const char *Solver::validity_to_str(Validity v) { } } -Solver::~Solver() { - delete impl; -} +Solver::Solver(SolverImpl *impl) : impl(impl) {} +Solver::~Solver() = default; char *Solver::getConstraintLog(const Query& query) { return impl->getConstraintLog(query); |