1 files changed, 63 insertions, 0 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()); }
+}