1 files changed, 29 insertions, 4 deletions

diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp
index dcaecb05..59a357b3 100644
--- a/lib/Solver/IndependentSolver.cpp
+++ b/lib/Solver/IndependentSolver.cpp
@@ -86,13 +86,23 @@ inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os,
 }
 
 class IndependentElementSet {
+public:
   typedef std::map<const Array*, ::DenseSet<unsigned> > elements_ty;
-  elements_ty elements;
-  std::set<const Array*> wholeObjects;
+  elements_ty elements;                 // Represents individual elements of array accesses (arr[1])
+  std::set<const Array*> wholeObjects;  // Represents symbolically accessed arrays (arr[x])
+  std::vector<ref<Expr> > exprs;        // All expressions that are associated with this factor
+                                        // Although order doesn't matter, we use a vector to match
+                                        // the ConstraintManager constructor that will eventually
+                                        // be invoked.
 
-public:
   IndependentElementSet() {}
   IndependentElementSet(ref<Expr> e) {
+    exprs.push_back(e);
+    // Track all reads in the program.  Determines whether reads are
+    // concrete or symbolic.  If they are symbolic, "collapses" array
+    // by adding it to wholeObjects.  Otherwise, creates a mapping of
+    // the form Map<array, set<index>> which tracks which parts of the
+    // array are being accessed.
     std::vector< ref<ReadExpr> > reads;
     findReads(e, /* visitUpdates= */ true, reads);
     for (unsigned i = 0; i != reads.size(); ++i) {
@@ -106,6 +116,8 @@ public:
 
       if (!wholeObjects.count(array)) {
         if (ConstantExpr *CE = dyn_cast<ConstantExpr>(re->index)) {
+          // if index constant, then add to set of constraints operating
+          // on that array (actually, don't add constraint, just set index)
           ::DenseSet<unsigned> &dis = elements[array];
           dis.add((unsigned) CE->getZExtValue(32));
         } else {
@@ -119,11 +131,13 @@ public:
   }
   IndependentElementSet(const IndependentElementSet &ies) : 
     elements(ies.elements),
-    wholeObjects(ies.wholeObjects) {}    
+    wholeObjects(ies.wholeObjects),
+    exprs(ies.exprs) {}
 
   IndependentElementSet &operator=(const IndependentElementSet &ies) {
     elements = ies.elements;
     wholeObjects = ies.wholeObjects;
+    exprs = ies.exprs;
     return *this;
   }
 
@@ -160,6 +174,7 @@ public:
 
   // more efficient when this is the smaller set
   bool intersects(const IndependentElementSet &b) {
+    // If there are any symbolic arrays in our query that b accesses
     for (std::set<const Array*>::iterator it = wholeObjects.begin(), 
            ie = wholeObjects.end(); it != ie; ++it) {
       const Array *array = *it;
@@ -170,9 +185,11 @@ public:
     for (elements_ty::iterator it = elements.begin(), ie = elements.end();
          it != ie; ++it) {
       const Array *array = it->first;
+      // if the array we access is symbolic in b
       if (b.wholeObjects.count(array))
         return true;
       elements_ty::const_iterator it2 = b.elements.find(array);
+      // if any of the elements we access are also accessed by b
       if (it2 != b.elements.end()) {
         if (it->second.intersects(it2->second))
           return true;
@@ -183,6 +200,11 @@ public:
 
   // returns true iff set is changed by addition
   bool add(const IndependentElementSet &b) {
+    for(unsigned i = 0; i < b.exprs.size(); i ++){
+      ref<Expr> expr = b.exprs[i];
+      exprs.push_back(expr);
+    }
+
     bool modified = false;
     for (std::set<const Array*>::const_iterator it = b.wholeObjects.begin(), 
            ie = b.wholeObjects.end(); it != ie; ++it) {
@@ -208,6 +230,7 @@ public:
           modified = true;
           elements.insert(*it);
         } else {
+          // Now need to see if there are any (z=?)'s
           if (it2->second.add(it->second))
             modified = true;
         }
@@ -244,6 +267,8 @@ IndependentElementSet getIndependentConstraints(const Query& query,
         if (eltsClosure.add(it->second))
           done = false;
         result.push_back(it->first);
+        // Means that we have added (z=y)added to (x=y)
+        // Now need to see if there are any (z=?)'s
       } else {
         newWorklist.push_back(*it);
       }