aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorDaniel Schemmel <daniel@schemmel.net>2023-03-24 02:50:22 +0000
committerCristian Cadar <c.cadar@imperial.ac.uk>2023-04-21 13:07:31 +0100
commite9d77be6c688836d68a2be5f3f0a02e63f392bb8 (patch)
tree2e7d1d55b122df555ec51ef0a0f3ee1cd856e64c
parent4d59fe9aef258c35212e5b7b9f6eb2e17b88d293 (diff)
downloadklee-e9d77be6c688836d68a2be5f3f0a02e63f392bb8.tar.gz
use unique_ptr in Solver
-rw-r--r--include/klee/Solver/Solver.h12
-rw-r--r--lib/Solver/Solver.cpp5
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);