Commit of improved IndependentSolver::getIniitalValues().

Previous implementation simply passed the entire constraint forward
without any factoring of the constraint at all.  This is a problem
since it is highly likely that there are cached solutions to pieces
of the constraint.  The new implementation breaks the entire
constraint down into its requisite factors and passes each piece
forward, one by one, down the solver chain.  After an answer is
returned, it is integrated into a larger solution.  Since, by
definition, no factor can affect another, we can safely create a
solution to the larger constraint from the answers of its smaller
pieces.

The reconstruction of the solution is done by analyzing which parts of
an array a factor touches.  If the factor is the only one to reference
a particular array, then all of the values calculated in the solution
for that array are included in the final answer.  If the factor
references a particular element of the array (for example, arr[1]),
then only the value in index 1 of array arr will be included in the
solution.

2 files changed, 77 insertions, 6 deletions

diff --git a/include/klee/util/Assignment.h b/include/klee/util/Assignment.h
index 63df4b65..6fee5cb1 100644
--- a/include/klee/util/Assignment.h
+++ b/include/klee/util/Assignment.h
@@ -29,13 +29,13 @@ namespace klee {
   public:
     Assignment(bool _allowFreeValues=false) 
       : allowFreeValues(_allowFreeValues) {}
-    Assignment(std::vector<const Array*> &objects, 
+    Assignment(const std::vector<const Array*> &objects,
                std::vector< std::vector<unsigned char> > &values,
                bool _allowFreeValues=false) 
       : allowFreeValues(_allowFreeValues){
       std::vector< std::vector<unsigned char> >::iterator valIt = 
         values.begin();
-      for (std::vector<const Array*>::iterator it = objects.begin(),
+      for (std::vector<const Array*>::const_iterator it = objects.begin(),
              ie = objects.end(); it != ie; ++it) {
         const Array *os = *it;
         std::vector<unsigned char> &arr = *valIt;
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp
index c02a3bd6..4d628a15 100644
--- a/lib/Solver/IndependentSolver.cpp
+++ b/lib/Solver/IndependentSolver.cpp
@@ -64,6 +64,14 @@ public:
     return false;
   }
 
+  std::set<unsigned>::iterator begin(){
+    return s.begin();
+  }
+
+  std::set<unsigned>::iterator end(){
+    return s.end();
+  }
+
   void print(llvm::raw_ostream &os) const {
     bool first = true;
     os << "{";
@@ -387,10 +395,7 @@ public:
   bool computeInitialValues(const Query& query,
                             const std::vector<const Array*> &objects,
                             std::vector< std::vector<unsigned char> > &values,
-                            bool &hasSolution) {
-    return solver->impl->computeInitialValues(query, objects, values,
-                                              hasSolution);
-  }
+                            bool &hasSolution);
   SolverRunStatus getOperationStatusCode();
   char *getConstraintLog(const Query&);
   void setCoreSolverTimeout(double timeout);
@@ -423,6 +428,72 @@ bool IndependentSolver::computeValue(const Query& query, ref<Expr> &result) {
   return solver->impl->computeValue(Query(tmp, query.expr), result);
 }
 
+bool IndependentSolver::computeInitialValues(const Query& query,
+                                             const std::vector<const Array*> &objects,
+                                             std::vector< std::vector<unsigned char> > &values,
+                                             bool &hasSolution){
+  std::list<IndependentElementSet> * factors = new std::list<IndependentElementSet>;
+  getAllIndependentConstraintsSets(query, factors);
+  //Used to rearrange all of the answers into the correct order
+  std::map<const Array*, std::vector<unsigned char> > retMap;
+  for (std::list<IndependentElementSet>::iterator it = factors->begin();
+       it != factors->end(); ++it) {
+    std::vector<const Array*> arraysInFactor;
+    calculateArrayReferences(*it, arraysInFactor);
+    // Going to use this as the "fresh" expression for the Query() invocation below
+    assert(it->exprs.size() >= 1 && "No null/empty factors");
+    if (arraysInFactor.size() == 0){
+      continue;
+    }
+    ConstraintManager tmp(it->exprs);
+    std::vector<std::vector<unsigned char> > tempValues;
+    if (!solver->impl->computeInitialValues(Query(tmp, ConstantExpr::alloc(0, Expr::Bool)),
+                                            arraysInFactor, tempValues, hasSolution)){
+      values.clear();
+      return false;
+    } else if (!hasSolution){
+      values.clear();
+      return true;
+    } else {
+      assert(tempValues.size() == arraysInFactor.size() &&
+             "Should be equal number arrays and answers");
+      for (unsigned i = 0; i < tempValues.size(); i++){
+        if (retMap.count(arraysInFactor[i])){
+          // We already have an array with some partially correct answers,
+          // so we need to place the answers to the new query into the right
+          // spot while avoiding the undetermined values also in the array
+          std::vector<unsigned char> * tempPtr = &retMap[arraysInFactor[i]];
+          assert(tempPtr->size() == tempValues[i].size() &&
+                 "we're talking about the same array here");
+          ::DenseSet<unsigned> * ds = &(it->elements[arraysInFactor[i]]);
+          for (std::set<unsigned>::iterator it2 = ds->begin(); it2 != ds->end(); it2++){
+            unsigned index = * it2;
+            (* tempPtr)[index] = tempValues[i][index];
+          }
+        } else {
+          // Dump all the new values into the array
+          retMap[arraysInFactor[i]] = tempValues[i];
+        }
+      }
+    }
+  }
+  for (std::vector<const Array *>::const_iterator it = objects.begin();
+       it != objects.end(); it++){
+    const Array * arr = * it;
+    if (!retMap.count(arr)){
+      // this means we have an array that is somehow related to the
+      // constraint, but whose values aren't actually required to
+      // satisfy the query.
+      std::vector<unsigned char> ret(arr->size);
+      values.push_back(ret);
+    } else {
+      values.push_back(retMap[arr]);
+    }
+  }
+  delete factors;
+  return true;
+}
+
 SolverImpl::SolverRunStatus IndependentSolver::getOperationStatusCode() {
   return solver->impl->getOperationStatusCode();      
 }