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

``DummySolver.cpp``. Whilst I'm here also clang-format the modified code.

1 files changed, 0 insertions, 40 deletions

diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index e596d37d..07e8b8a0 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -276,46 +276,6 @@ std::pair< ref<Expr>, ref<Expr> > Solver::getRange(const Query& query) {
                         ConstantExpr::create(max, width));
 }
 
-
-/***/
-
-class DummySolverImpl : public SolverImpl {
-public: 
-  DummySolverImpl() {}
-  
-  bool computeValidity(const Query&, Solver::Validity &result) { 
-    ++stats::queries;
-    // FIXME: We should have stats::queriesFail;
-    return false; 
-  }
-  bool computeTruth(const Query&, bool &isValid) { 
-    ++stats::queries;
-    // FIXME: We should have stats::queriesFail;
-    return false; 
-  }
-  bool computeValue(const Query&, ref<Expr> &result) { 
-    ++stats::queries;
-    ++stats::queryCounterexamples;
-    return false; 
-  }
-  bool computeInitialValues(const Query&,
-                            const std::vector<const Array*> &objects,
-                            std::vector< std::vector<unsigned char> > &values,
-                            bool &hasSolution) { 
-    ++stats::queries;
-    ++stats::queryCounterexamples;
-    return false; 
-  }
-  SolverRunStatus getOperationStatusCode() {
-      return SOLVER_RUN_STATUS_FAILURE;
-  }
-  
-};
-
-Solver *klee::createDummySolver() {
-  return new Solver(new DummySolverImpl());
-}
-
 /***/
 
 class STPSolverImpl : public SolverImpl {