Add klee::createDummySolver, the dummy solver always fails.

 - Useful as an alternative backend to STP for testing.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73048 91177308-0d34-0410-b5e6-96231b3b80d8

2 files changed, 38 insertions, 0 deletions

diff --git a/include/klee/Solver.h b/include/klee/Solver.h
index b8324a9f..f1e18f12 100644
--- a/include/klee/Solver.h
+++ b/include/klee/Solver.h
@@ -213,6 +213,9 @@ namespace klee {
   /// after writing them to the given path in .pc format.
   Solver *createPCLoggingSolver(Solver *s, std::string path);
 
+  /// createDummySolver - Create a dummy solver implementation which always
+  /// fails.
+  Solver *createDummySolver();
 }
 
 #endif
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 936f252d..98dcad0b 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -375,6 +375,41 @@ Solver *klee::createValidatingSolver(Solver *s, Solver *oracle) {
 
 /***/
 
+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; 
+  }
+};
+
+Solver *klee::createDummySolver() {
+  return new Solver(new DummySolverImpl());
+}
+
+/***/
+
 class STPSolverImpl : public SolverImpl {
 private:
   /// The solver we are part of, for access to public information.