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

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

1 files changed, 142 insertions, 0 deletions

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));
+}
+}