diff options
| author | Daniel Schemmel <daniel@schemmel.net> | 2023-03-24 15:05:43 +0000 |
|---|---|---|
| committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2023-04-21 13:07:31 +0100 |
| commit | ac0fa15ab0679fe1b5067b07647b0701ae3bc347 (patch) | |
| tree | f2294eb5f0795ee9ce0f92d527242b7b7a507e79 /lib/Solver/SMTLIBLoggingSolver.cpp | |
| parent | e9d77be6c688836d68a2be5f3f0a02e63f392bb8 (diff) | |
| download | klee-ac0fa15ab0679fe1b5067b07647b0701ae3bc347.tar.gz | |
use unique_ptr all throughout the solver chain
Diffstat (limited to 'lib/Solver/SMTLIBLoggingSolver.cpp')
| -rw-r--r-- | lib/Solver/SMTLIBLoggingSolver.cpp | 35 |
1 files changed, 18 insertions, 17 deletions
diff --git a/lib/Solver/SMTLIBLoggingSolver.cpp b/lib/Solver/SMTLIBLoggingSolver.cpp index bfea5c1b..c0713b45 100644 --- a/lib/Solver/SMTLIBLoggingSolver.cpp +++ b/lib/Solver/SMTLIBLoggingSolver.cpp @@ -11,6 +11,9 @@ #include "klee/Expr/ExprSMTLIBPrinter.h" +#include <memory> +#include <utility> + using namespace klee; /// This QueryLoggingSolver will log queries to a file in the SMTLIBv2 format @@ -18,7 +21,6 @@ using namespace klee; class SMTLIBLoggingSolver : public QueryLoggingSolver { private: - ExprSMTLIBPrinter printer; virtual void printQuery(const Query& query, @@ -41,22 +43,21 @@ class SMTLIBLoggingSolver : public QueryLoggingSolver printer.generateOutput(); } - - public: - SMTLIBLoggingSolver(Solver *_solver, - std::string path, - time::Span queryTimeToLog, - bool logTimedOut) - : QueryLoggingSolver(_solver, path, ";", queryTimeToLog, logTimedOut) - { - //Setup the printer - printer.setOutput(logBuffer); - } -}; +public: + SMTLIBLoggingSolver(std::unique_ptr<Solver> solver, std::string path, + time::Span queryTimeToLog, bool logTimedOut) + : QueryLoggingSolver(std::move(solver), std::move(path), ";", + queryTimeToLog, logTimedOut) { + // Setup the printer + printer.setOutput(logBuffer); + } +}; -Solver* klee::createSMTLIBLoggingSolver(Solver *_solver, std::string path, - time::Span minQueryTimeToLog, bool logTimedOut) -{ - return new Solver(new SMTLIBLoggingSolver(_solver, path, minQueryTimeToLog, logTimedOut)); +std::unique_ptr<Solver> +klee::createSMTLIBLoggingSolver(std::unique_ptr<Solver> solver, + std::string path, time::Span minQueryTimeToLog, + bool logTimedOut) { + return std::make_unique<Solver>(std::make_unique<SMTLIBLoggingSolver>( + std::move(solver), std::move(path), minQueryTimeToLog, logTimedOut)); } |
