From: Hamed Gorjiara <hgorjiar@uci.edu>
Date: Thu, 6 Sep 2018 20:18:03 +0000 (-0700)
Subject: Bug fix in encoding subgraph DFS algorithm
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=eca9578226d7d44386fab228c4fa896e8100e5b5;p=satune.git

Bug fix in encoding subgraph DFS algorithm
---

diff --git a/src/ASTAnalyses/Encoding/subgraph.cc b/src/ASTAnalyses/Encoding/subgraph.cc
index 8693754..adc7ad7 100644
--- a/src/ASTAnalyses/Encoding/subgraph.cc
+++ b/src/ASTAnalyses/Encoding/subgraph.cc
@@ -61,6 +61,7 @@ void EncodingSubGraph::solveEquals() {
 		SetIteratorEncodingValue *conflictIt = ev->notequals.iterator();
 		while (conflictIt->hasNext()) {
 			EncodingValue *conflict = conflictIt->next();
+			ASSERT(conflict->value != ev->value);
 			if (conflict->assigned) {
 				encodingArray.setExpand(conflict->encoding, true);
 			}
@@ -239,6 +240,7 @@ void EncodingSubGraph::generateEquals(EncodingNode *left, EncodingNode *right) {
 			NodeValuePair nvp2(right, rVal);
 			EncodingValue *rev = map.get(&nvp2);
 			if (lev != rev) {
+				ASSERT(lVal != rVal);
 				if (lev->inComparison && rev->inComparison) {
 					//Need to assign during comparison stage...
 					//Thus promote to comparison
@@ -351,19 +353,24 @@ void EncodingSubGraph::traverseValue(EncodingNode *node, uint64_t value) {
 	while (tovisit.getSize() != 0) {
 		EncodingNode *n = tovisit.last();tovisit.pop();
 		//Add encoding node to structures
-		ecv->nodes.add(n);
 		NodeValuePair *nvp = new NodeValuePair(n, value);
+		if(map.contains(nvp))
+			continue;
+		ecv->nodes.add(n);
 		map.put(nvp, ecv);
-		SetIteratorEncodingEdge *edgeit = node->edges.iterator();
+		ASSERT(node != NULL);
+		SetIteratorEncodingEdge *edgeit = n->edges.iterator();
 		while (edgeit->hasNext()) {
 			EncodingEdge *ee = edgeit->next();
 			if (!discovered.contains(ee->left) && nodes.contains(ee->left) && ee->left->s->exists(value)) {
 				tovisit.push(ee->left);
 				discovered.add(ee->left);
+				ASSERT(discovered.contains(ee->left));
 			}
 			if (!discovered.contains(ee->right) && nodes.contains(ee->right) && ee->right->s->exists(value)) {
 				tovisit.push(ee->right);
 				discovered.add(ee->right);
+				ASSERT(discovered.contains(ee->right));
 			}
 		}
 		delete edgeit;