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

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

2 files changed, 142 insertions, 134 deletions

diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 30424526..e596d37d 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -276,140 +276,6 @@ std::pair< ref<Expr>, ref<Expr> > Solver::getRange(const Query& query) {
                         ConstantExpr::create(max, width));
 }
 
-/***/
-
-class ValidatingSolver : public SolverImpl {
-private:
-  Solver *solver, *oracle;
-
-public: 
-  ValidatingSolver(Solver *_solver, Solver *_oracle) 
-    : solver(_solver), oracle(_oracle) {}
-  ~ValidatingSolver() { delete solver; }
-  
-  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();
-  char *getConstraintLog(const Query&);
-  void setCoreSolverTimeout(double timeout);
-};
-
-bool ValidatingSolver::computeTruth(const Query& query,
-                                    bool &isValid) {
-  bool answer;
-  
-  if (!solver->impl->computeTruth(query, isValid))
-    return false;
-  if (!oracle->impl->computeTruth(query, answer))
-    return false;
-  
-  if (isValid != answer)
-    assert(0 && "invalid solver result (computeTruth)");
-  
-  return true;
-}
-
-bool ValidatingSolver::computeValidity(const Query& query,
-                                       Solver::Validity &result) {
-  Solver::Validity answer;
-  
-  if (!solver->impl->computeValidity(query, result))
-    return false;
-  if (!oracle->impl->computeValidity(query, answer))
-    return false;
-  
-  if (result != answer)
-    assert(0 && "invalid solver result (computeValidity)");
-  
-  return true;
-}
-
-bool ValidatingSolver::computeValue(const Query& query,
-                                    ref<Expr> &result) {  
-  bool answer;
-
-  if (!solver->impl->computeValue(query, result))
-    return false;
-  // We don't want to compare, but just make sure this is a legal
-  // solution.
-  if (!oracle->impl->computeTruth(query.withExpr(NeExpr::create(query.expr, 
-                                                                result)),
-                                  answer))
-    return false;
-
-  if (answer)
-    assert(0 && "invalid solver result (computeValue)");
-
-  return true;
-}
-
-bool 
-ValidatingSolver::computeInitialValues(const Query& query,
-                                       const std::vector<const Array*>
-                                         &objects,
-                                       std::vector< std::vector<unsigned char> >
-                                         &values,
-                                       bool &hasSolution) {
-  bool answer;
-
-  if (!solver->impl->computeInitialValues(query, objects, values, 
-                                          hasSolution))
-    return false;
-
-  if (hasSolution) {
-    // Assert the bindings as constraints, and verify that the
-    // conjunction of the actual constraints is satisfiable.
-    std::vector< ref<Expr> > bindings;
-    for (unsigned i = 0; i != values.size(); ++i) {
-      const Array *array = objects[i];
-      assert(array);
-      for (unsigned j=0; j<array->size; j++) {
-        unsigned char value = values[i][j];
-        bindings.push_back(EqExpr::create(ReadExpr::create(UpdateList(array, 0),
-                                                           ConstantExpr::alloc(j, array->getDomain())),
-                                          ConstantExpr::alloc(value, array->getRange())));
-      }
-    }
-    ConstraintManager tmp(bindings);
-    ref<Expr> constraints = Expr::createIsZero(query.expr);
-    for (ConstraintManager::const_iterator it = query.constraints.begin(), 
-           ie = query.constraints.end(); it != ie; ++it)
-      constraints = AndExpr::create(constraints, *it);
-    
-    if (!oracle->impl->computeTruth(Query(tmp, constraints), answer))
-      return false;
-    if (!answer)
-      assert(0 && "invalid solver result (computeInitialValues)");
-  } else {
-    if (!oracle->impl->computeTruth(query, answer))
-      return false;
-    if (!answer)
-      assert(0 && "invalid solver result (computeInitialValues)");    
-  }
-
-  return true;
-}
-
-SolverImpl::SolverRunStatus ValidatingSolver::getOperationStatusCode() {
-    return solver->impl->getOperationStatusCode();
-}
-
-char *ValidatingSolver::getConstraintLog(const Query& query) {
-  return solver->impl->getConstraintLog(query);
-}
-
-void ValidatingSolver::setCoreSolverTimeout(double timeout) {
-  solver->impl->setCoreSolverTimeout(timeout);
-}
-
-Solver *klee::createValidatingSolver(Solver *s, Solver *oracle) {
-  return new Solver(new ValidatingSolver(s, oracle));
-}
 
 /***/
 
diff --git a/lib/Solver/ValidatingSolver.cpp b/lib/Solver/ValidatingSolver.cpp
new file mode 100644
index 00000000..ef79b563
--- /dev/null
+++ b/lib/Solver/ValidatingSolver.cpp
@@ -0,0 +1,142 @@
+//===-- ValidatingSolver.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/Constraints.h"
+#include "klee/Solver.h"
+#include "klee/SolverImpl.h"
+#include <vector>
+
+namespace klee {
+
+class ValidatingSolver : public SolverImpl {
+private:
+  Solver *solver, *oracle;
+
+public:
+  ValidatingSolver(Solver *_solver, Solver *_oracle)
+      : solver(_solver), oracle(_oracle) {}
+  ~ValidatingSolver() { delete solver; }
+
+  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();
+  char *getConstraintLog(const Query &);
+  void setCoreSolverTimeout(double timeout);
+};
+
+bool ValidatingSolver::computeTruth(const Query &query, bool &isValid) {
+  bool answer;
+
+  if (!solver->impl->computeTruth(query, isValid))
+    return false;
+  if (!oracle->impl->computeTruth(query, answer))
+    return false;
+
+  if (isValid != answer)
+    assert(0 && "invalid solver result (computeTruth)");
+
+  return true;
+}
+
+bool ValidatingSolver::computeValidity(const Query &query,
+                                       Solver::Validity &result) {
+  Solver::Validity answer;
+
+  if (!solver->impl->computeValidity(query, result))
+    return false;
+  if (!oracle->impl->computeValidity(query, answer))
+    return false;
+
+  if (result != answer)
+    assert(0 && "invalid solver result (computeValidity)");
+
+  return true;
+}
+
+bool ValidatingSolver::computeValue(const Query &query, ref<Expr> &result) {
+  bool answer;
+
+  if (!solver->impl->computeValue(query, result))
+    return false;
+  // We don't want to compare, but just make sure this is a legal
+  // solution.
+  if (!oracle->impl->computeTruth(
+          query.withExpr(NeExpr::create(query.expr, result)), answer))
+    return false;
+
+  if (answer)
+    assert(0 && "invalid solver result (computeValue)");
+
+  return true;
+}
+
+bool ValidatingSolver::computeInitialValues(
+    const Query &query, const std::vector<const Array *> &objects,
+    std::vector<std::vector<unsigned char> > &values, bool &hasSolution) {
+  bool answer;
+
+  if (!solver->impl->computeInitialValues(query, objects, values, hasSolution))
+    return false;
+
+  if (hasSolution) {
+    // Assert the bindings as constraints, and verify that the
+    // conjunction of the actual constraints is satisfiable.
+    std::vector<ref<Expr> > bindings;
+    for (unsigned i = 0; i != values.size(); ++i) {
+      const Array *array = objects[i];
+      assert(array);
+      for (unsigned j = 0; j < array->size; j++) {
+        unsigned char value = values[i][j];
+        bindings.push_back(EqExpr::create(
+            ReadExpr::create(UpdateList(array, 0),
+                             ConstantExpr::alloc(j, array->getDomain())),
+            ConstantExpr::alloc(value, array->getRange())));
+      }
+    }
+    ConstraintManager tmp(bindings);
+    ref<Expr> constraints = Expr::createIsZero(query.expr);
+    for (ConstraintManager::const_iterator it = query.constraints.begin(),
+                                           ie = query.constraints.end();
+         it != ie; ++it)
+      constraints = AndExpr::create(constraints, *it);
+
+    if (!oracle->impl->computeTruth(Query(tmp, constraints), answer))
+      return false;
+    if (!answer)
+      assert(0 && "invalid solver result (computeInitialValues)");
+  } else {
+    if (!oracle->impl->computeTruth(query, answer))
+      return false;
+    if (!answer)
+      assert(0 && "invalid solver result (computeInitialValues)");
+  }
+
+  return true;
+}
+
+SolverImpl::SolverRunStatus ValidatingSolver::getOperationStatusCode() {
+  return solver->impl->getOperationStatusCode();
+}
+
+char *ValidatingSolver::getConstraintLog(const Query &query) {
+  return solver->impl->getConstraintLog(query);
+}
+
+void ValidatingSolver::setCoreSolverTimeout(double timeout) {
+  solver->impl->setCoreSolverTimeout(timeout);
+}
+
+Solver *createValidatingSolver(Solver *s, Solver *oracle) {
+  return new Solver(new ValidatingSolver(s, oracle));
+}
+}