about summary refs log tree commit diff homepage
path: root/lib/Solver/SMTLIBLoggingSolver.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Solver/SMTLIBLoggingSolver.cpp')
-rw-r--r--lib/Solver/SMTLIBLoggingSolver.cpp35
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));
 }