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.

1 files changed, 22 insertions, 0 deletions

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