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

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

1 files changed, 0 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";