2 files changed, 63 insertions, 40 deletions
diff --git a/lib/Solver/DummySolver.cpp b/lib/Solver/DummySolver.cpp
new file mode 100644
index 00000000..39328653
--- /dev/null
+++ b/lib/Solver/DummySolver.cpp
@@ -0,0 +1,63 @@
+//===-- DummySolver.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"
+#include "klee/SolverStats.h"
+
+namespace klee {
+
+class DummySolverImpl : public SolverImpl {
+public:
+  DummySolverImpl();
+
+  bool computeValidity(const Query &, Solver::Validity &result);
+  bool computeTruth(const Query &, bool &isValid);
+  bool computeValue(const Query &, ref<Expr> &result);
+  bool computeInitialValues(const Query &,
+                            const std::vector<const Array *> &objects,
+                            std::vector<std::vector<unsigned char> > &values,
+                            bool &hasSolution);
+  SolverRunStatus getOperationStatusCode();
+};
+
+DummySolverImpl::DummySolverImpl() {}
+
+bool DummySolverImpl::computeValidity(const Query &, Solver::Validity &result) {
+  ++stats::queries;
+  // FIXME: We should have stats::queriesFail;
+  return false;
+}
+
+bool DummySolverImpl::computeTruth(const Query &, bool &isValid) {
+  ++stats::queries;
+  // FIXME: We should have stats::queriesFail;
+  return false;
+}
+
+bool DummySolverImpl::computeValue(const Query &, ref<Expr> &result) {
+  ++stats::queries;
+  ++stats::queryCounterexamples;
+  return false;
+}
+
+bool DummySolverImpl::computeInitialValues(
+    const Query &, const std::vector<const Array *> &objects,
+    std::vector<std::vector<unsigned char> > &values, bool &hasSolution) {
+  ++stats::queries;
+  ++stats::queryCounterexamples;
+  return false;
+}
+
+SolverImpl::SolverRunStatus DummySolverImpl::getOperationStatusCode() {
+  return SOLVER_RUN_STATUS_FAILURE;
+}
+
+Solver *createDummySolver() { return new Solver(new DummySolverImpl()); }
+}
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 {