Altered DenseSet and IndependentElementSet to record ref<Expr> involved

This is important for future changes to IndependentSolver::
getInitialValues() so that an incoming constraint can be broken
down into its smallest possible parts.  Each of these individual
parts may then be solved for and then the solutions to each piece
combined to create a final answer.

Finally, several fields which had previously been private are now
public to facilitate the smaller solutions being combined into a
larger solution.

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