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