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

1 files changed, 35 insertions, 0 deletions

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.