[NFC] Refactor SolverImpl out of Solver.cpp into its own file

(SolverImpl.cpp). Whilst I'm here also clang-format the modified
code.

2 files changed, 52 insertions, 46 deletions

diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 6f4bbc5b..30424526 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -69,52 +69,6 @@ using namespace metaSMT::solver;
 
 #endif /* SUPPORT_METASMT */
 
-
-
-/***/
-
-SolverImpl::~SolverImpl() {
-}
-
-bool SolverImpl::computeValidity(const Query& query, Solver::Validity &result) {
-  bool isTrue, isFalse;
-  if (!computeTruth(query, isTrue))
-    return false;
-  if (isTrue) {
-    result = Solver::True;
-  } else {
-    if (!computeTruth(query.negateExpr(), isFalse))
-      return false;
-    result = isFalse ? Solver::False : Solver::Unknown;
-  }
-  return true;
-}
-
-const char* SolverImpl::getOperationStatusString(SolverRunStatus statusCode)
-{
-    switch (statusCode)
-    {
-        case SOLVER_RUN_STATUS_SUCCESS_SOLVABLE:
-            return "OPERATION SUCCESSFUL, QUERY IS SOLVABLE";
-        case SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE:
-            return "OPERATION SUCCESSFUL, QUERY IS UNSOLVABLE";
-        case SOLVER_RUN_STATUS_FAILURE:
-            return "OPERATION FAILED";
-        case SOLVER_RUN_STATUS_TIMEOUT:
-            return "SOLVER TIMEOUT";
-        case SOLVER_RUN_STATUS_FORK_FAILED:
-            return "FORK FAILED";
-        case SOLVER_RUN_STATUS_INTERRUPTED:
-            return "SOLVER PROCESS INTERRUPTED";
-        case SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE:
-            return "UNEXPECTED SOLVER PROCESS EXIT CODE";
-        case SOLVER_RUN_STATUS_WAITPID_FAILED:
-            return "WAITPID FAILED FOR SOLVER PROCESS";
-        default:
-            return "UNRECOGNIZED OPERATION STATUS";        
-    }    
-}
-
 const char *Solver::validity_to_str(Validity v) {
   switch (v) {
   default:    return "Unknown";
diff --git a/lib/Solver/SolverImpl.cpp b/lib/Solver/SolverImpl.cpp
new file mode 100644
index 00000000..e8f30c9e
--- /dev/null
+++ b/lib/Solver/SolverImpl.cpp
@@ -0,0 +1,52 @@
+//===-- SolverImpl.cpp ----------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "klee/Solver.h"
+#include "klee/SolverImpl.h"
+
+using namespace klee;
+
+SolverImpl::~SolverImpl() {}
+
+bool SolverImpl::computeValidity(const Query &query, Solver::Validity &result) {
+  bool isTrue, isFalse;
+  if (!computeTruth(query, isTrue))
+    return false;
+  if (isTrue) {
+    result = Solver::True;
+  } else {
+    if (!computeTruth(query.negateExpr(), isFalse))
+      return false;
+    result = isFalse ? Solver::False : Solver::Unknown;
+  }
+  return true;
+}
+
+const char *SolverImpl::getOperationStatusString(SolverRunStatus statusCode) {
+  switch (statusCode) {
+  case SOLVER_RUN_STATUS_SUCCESS_SOLVABLE:
+    return "OPERATION SUCCESSFUL, QUERY IS SOLVABLE";
+  case SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE:
+    return "OPERATION SUCCESSFUL, QUERY IS UNSOLVABLE";
+  case SOLVER_RUN_STATUS_FAILURE:
+    return "OPERATION FAILED";
+  case SOLVER_RUN_STATUS_TIMEOUT:
+    return "SOLVER TIMEOUT";
+  case SOLVER_RUN_STATUS_FORK_FAILED:
+    return "FORK FAILED";
+  case SOLVER_RUN_STATUS_INTERRUPTED:
+    return "SOLVER PROCESS INTERRUPTED";
+  case SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE:
+    return "UNEXPECTED SOLVER PROCESS EXIT CODE";
+  case SOLVER_RUN_STATUS_WAITPID_FAILED:
+    return "WAITPID FAILED FOR SOLVER PROCESS";
+  default:
+    return "UNRECOGNIZED OPERATION STATUS";
+  }
+}