From be37ac9605d380b7f36717338c2c520f375798c8 Mon Sep 17 00:00:00 2001
From: Eric Rizzi <eric.rizzi@gmail.com>
Date: Mon, 16 Feb 2015 12:17:00 -0500
Subject: Added the function IndependentSolver::createdPointEvaluatesToTrue

This function should be used solely in assertion statements and is
intended as a sanity check to make sure that the solution constructed
by IndependentSolver::getInitialValues() produces and answer that in
fact satisfies the the query.
---
 lib/Solver/IndependentSolver.cpp | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

(limited to 'lib/Solver')

diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp
index 4d628a15..cfe1bb16 100644
--- a/lib/Solver/IndependentSolver.cpp
+++ b/lib/Solver/IndependentSolver.cpp
@@ -428,6 +428,27 @@ bool IndependentSolver::computeValue(const Query& query, ref<Expr> &result) {
   return solver->impl->computeValue(Query(tmp, query.expr), result);
 }
 
+
+// Helper function used only for assertions to make sure point created
+// during computeInitialValues is in fact correct.
+bool assertCreatedPointEvaluatesToTrue(const Query &query,
+                                       const std::vector<const Array*> &objects,
+                                       std::vector< std::vector<unsigned char> > &values){
+  Assignment assign = Assignment(objects, values);
+  for(ConstraintManager::constraint_iterator it = query.constraints.begin();
+      it != query.constraints.end(); ++it){
+    ref<Expr> ret = assign.evaluate(*it);
+    if(! isa<ConstantExpr>(ret) || ! cast<ConstantExpr>(ret)->isTrue()){
+      return false;
+    }
+  }
+  ref<Expr> neg = Expr::createIsZero(query.expr);
+  ref<Expr> q = assign.evaluate(neg);
+
+  assert(isa<ConstantExpr>(q) && "assignment evaluation did not result in constant");
+  return cast<ConstantExpr>(q)->isTrue();
+}
+
 bool IndependentSolver::computeInitialValues(const Query& query,
                                              const std::vector<const Array*> &objects,
                                              std::vector< std::vector<unsigned char> > &values,
@@ -490,6 +511,7 @@ bool IndependentSolver::computeInitialValues(const Query& query,
       values.push_back(retMap[arr]);
     }
   }
+  assert(assertCreatedPointEvaluatesToTrue(query, objects, values) && "should satisfy the equation");
   delete factors;
   return true;
 }
-- 
cgit 1.4.1