From 0784ff823bdf8cf52eb08ecae2987d9a79b7f45b Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Thu, 7 Jan 2016 09:31:56 +0000
Subject: [NFC] Refactor ValidatingSolver out of Solver.cpp into its own file
 ``ValidatingSolver.cpp``. Whilst I'm here also clang-format the modified
 code.

---
 lib/Solver/Solver.cpp | 134 --------------------------------------------------
 1 file changed, 134 deletions(-)

(limited to 'lib/Solver/Solver.cpp')

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));
-}
 
 /***/
 
-- 
cgit 1.4.1