From: bdemsky <bdemsky@uci.edu>
Date: Tue, 19 Sep 2017 17:38:04 +0000 (-0700)
Subject: More code
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=5f41b2b031712790013f031bedcf815c668b5768;p=satune.git

More code
---

diff --git a/src/ASTAnalyses/Encoding/subgraph.cc b/src/ASTAnalyses/Encoding/subgraph.cc
index 69fb367..3690ea7 100644
--- a/src/ASTAnalyses/Encoding/subgraph.cc
+++ b/src/ASTAnalyses/Encoding/subgraph.cc
@@ -1,6 +1,7 @@
 #include "subgraph.h"
 #include "encodinggraph.h"
 #include "set.h"
+#include "qsort.h"
 
 EncodingSubGraph::EncodingSubGraph() :
 	encodingSize(0),
@@ -15,6 +16,82 @@ bool equalsNodeValuePair(NodeValuePair *nvp1, NodeValuePair *nvp2) {
 	return nvp1->value == nvp2->value && nvp1->node == nvp2->node;
 }
 
+int sortEncodingValue(const void *p1, const void *p2) {
+	const EncodingValue * e1 = * (const EncodingValue **) p1;
+	const EncodingValue * e2 = * (const EncodingValue **) p2;
+	uint se1=e1->notequals.getSize();
+	uint se2=e2->notequals.getSize();
+	if (se1 > se2)
+		return -1;
+	else if (se2 == se1)
+		return 0;
+	else
+		return 1;
+}
+
+void EncodingSubGraph::solveEquals() {
+	Vector<EncodingValue *> toEncode;
+	Vector<bool> encodingArray;
+	SetIteratorEncodingValue *valIt=values.iterator();
+	while(valIt->hasNext()) {
+		EncodingValue *ev=valIt->next();
+		if (!ev->inComparison)
+			toEncode.push(ev);
+		else
+			ev->assigned = true;
+	}
+	delete valIt;
+	bsdqsort(toEncode.expose(), toEncode.getSize(), sizeof(EncodingValue *), sortEncodingValue);
+	uint toEncodeSize=toEncode.getSize();
+	for(uint i=0; i<toEncodeSize; i++) {
+		EncodingValue * ev=toEncode.get(i);
+		encodingArray.clear();
+		SetIteratorEncodingValue *conflictIt=ev->notequals.iterator();
+		while(conflictIt->hasNext()) {
+			EncodingValue * conflict=conflictIt->next();
+			if (conflict->assigned) {
+				encodingArray.setExpand(conflict->encoding, true);
+			}
+		}
+		delete conflictIt;
+		uint encoding=0;
+		for(;encoding<encodingArray.getSize();encoding++) {
+			//See if this is unassigned
+			if (!encodingArray.get(encoding))
+				break;
+		}
+		ev->encoding = encoding;
+		ev->assigned = true;
+	}
+}
+
+void EncodingSubGraph::solveComparisons() {
+	HashsetEncodingValue discovered;
+	Vector<EncodingValue *> tovisit;
+	SetIteratorEncodingValue *valIt=values.iterator();
+	while(valIt->hasNext()) {
+		EncodingValue *ev=valIt->next();
+		if (discovered.add(ev)) {
+			tovisit.push(ev);
+			while(tovisit.getSize()!=0) {
+				EncodingValue * val=tovisit.last(); tovisit.pop();
+				SetIteratorEncodingValue *nextIt=val->larger.iterator();
+				uint minVal = val->encoding + 1;
+				while(nextIt->hasNext()) {
+					EncodingValue *nextVal=nextIt->next();
+					if (nextVal->encoding < minVal) {
+						nextVal->encoding = minVal;
+						discovered.add(nextVal);
+						tovisit.push(nextVal);
+					}
+				}
+				delete nextIt;
+			}
+		}
+	}
+	delete valIt;
+}
+
 uint EncodingSubGraph::estimateNewSize(EncodingSubGraph *sg) {
 	uint newSize=0;
 	SetIteratorEncodingNode * nit = sg->nodes.iterator();
@@ -67,10 +144,45 @@ SetIteratorEncodingNode * EncodingSubGraph::nodeIterator() {
 
 void EncodingSubGraph::encode() {
 	computeEncodingValue();
-	computeInequalities();
+	computeComparisons();
+	computeEqualities();
+	solveComparisons();
+	solveEquals();
+}
+
+void EncodingSubGraph::computeEqualities() {
+	SetIteratorEncodingNode *nodeit=nodes.iterator();
+	while(nodeit->hasNext()) {
+		EncodingNode *node=nodeit->next();
+		generateEquals(node, node);
+		
+		SetIteratorEncodingEdge *edgeit=node->edges.iterator();
+		while(edgeit->hasNext()) {
+			EncodingEdge *edge=edgeit->next();
+			//skip over comparisons as we have already handled them
+			if (edge->numComparisons != 0)
+				continue;
+			if (edge->numEquals == 0)
+				continue;
+			if (edge->left == NULL || !nodes.contains(edge->left))
+				continue;
+			if (edge->right == NULL || !nodes.contains(edge->right))
+				continue;
+			//examine only once
+			if (edge->left != node)
+				continue;
+			//We have a comparison edge between two nodes in the subgraph
+			//For now we don't support multiple encoding values with the same encoding....
+			//So we enforce != constraints for every Set...
+			if (edge->left != edge->right)
+				generateEquals(edge->left, edge->right);
+		}
+		delete edgeit;
+	}
+	delete nodeit;
 }
 
-void EncodingSubGraph::computeInequalities() {
+void EncodingSubGraph::computeComparisons() {
 	SetIteratorEncodingNode *nodeit=nodes.iterator();
 	while(nodeit->hasNext()) {
 		EncodingNode *node=nodeit->next();
@@ -92,6 +204,42 @@ void EncodingSubGraph::computeInequalities() {
 		delete edgeit;
 	}
 	delete nodeit;
+	
+	
+}
+
+void EncodingSubGraph::orderEV(EncodingValue *earlier, EncodingValue *later) {
+	earlier->larger.add(later);
+}
+
+void EncodingSubGraph::generateEquals(EncodingNode *left, EncodingNode *right) {
+	Set *lset=left->s;
+	Set *rset=right->s;
+	uint lSize=lset->getSize(), rSize=rset->getSize();
+	for(uint lindex=0; lindex < lSize; lindex++) {
+		for(uint rindex=0; rindex < rSize; rindex++) {
+			uint64_t lVal=lset->getElement(lindex);
+			NodeValuePair nvp1(left, lVal);
+			EncodingValue *lev = map.get(&nvp1);
+			uint64_t rVal=rset->getElement(rindex);
+			NodeValuePair nvp2(right, rVal);
+			EncodingValue *rev = map.get(&nvp2);
+			if (lev != rev) {
+				if (lev->inComparison && rev->inComparison) {
+					//Need to assign during comparison stage...
+					//Thus promote to comparison
+					if (lVal < rVal) {
+						orderEV(lev, rev);
+					} else {
+						orderEV(rev, lev);
+					}
+				} else {
+					lev->notequals.add(rev);
+					rev->notequals.add(lev);
+				}
+			}
+		}
+	}
 }
 
 void EncodingSubGraph::generateComparison(EncodingNode *left, EncodingNode *right) {
@@ -112,14 +260,14 @@ void EncodingSubGraph::generateComparison(EncodingNode *left, EncodingNode *righ
 	while(lindex < lSize || rindex < rSize) {
 		if (last != NULL) {
 			if (lev != NULL)
-				last->larger.push(lev);
+				orderEV(last, lev);
 			if (rev != NULL && lev != rev)
-				last->larger.push(rev);
+				orderEV(last, rev);
 		}
 		if (lev != rev) {
 			if (rev == NULL || lVal < rVal) {
 				if (rev != NULL)
-					lev->larger.push(rev);
+					orderEV(lev, rev);
 				last = lev;
 				if (++lindex < lSize) {
 					lVal=lset->getElement(lindex);
@@ -130,7 +278,7 @@ void EncodingSubGraph::generateComparison(EncodingNode *left, EncodingNode *righ
 					lev = NULL;
 			} else {
 				if (lev != NULL)
-					rev->larger.push(lev);
+					orderEV(rev, lev);
 				last = rev;
 				if (++rindex < rSize) {
 					rVal=rset->getElement(rindex);
@@ -180,6 +328,7 @@ void EncodingSubGraph::computeEncodingValue() {
 
 void EncodingSubGraph::traverseValue(EncodingNode *node, uint64_t value) {
 	EncodingValue *ecv=new EncodingValue(value);
+	values.add(ecv);
 	HashsetEncodingNode discovered;
 	Vector<EncodingNode *> tovisit;
 	tovisit.push(node);
diff --git a/src/ASTAnalyses/Encoding/subgraph.h b/src/ASTAnalyses/Encoding/subgraph.h
index bc7fdbf..4f19eb1 100644
--- a/src/ASTAnalyses/Encoding/subgraph.h
+++ b/src/ASTAnalyses/Encoding/subgraph.h
@@ -11,20 +11,28 @@ class NodeValuePair {
 	uint64_t value;
 };
 
+class EncodingValue;
+
+typedef Hashset<EncodingValue *, uintptr_t, PTRSHIFT> HashsetEncodingValue;
+typedef SetIterator<EncodingValue *, uintptr_t, PTRSHIFT> SetIteratorEncodingValue;
+
 class EncodingValue {
  public:
- EncodingValue(uint64_t _val) : value(_val), inComparison(false) {}
+ EncodingValue(uint64_t _val) : value(_val), encoding(0), inComparison(false), assigned(false) {}
 	void merge(EncodingValue *value);
 	uint64_t value;
+	uint encoding;
 	bool inComparison;
+	bool assigned;
 	HashsetEncodingNode nodes;
-	Vector<EncodingValue *> larger;
+	HashsetEncodingValue larger;
+	HashsetEncodingValue notequals;
 };
 
 uint hashNodeValuePair(NodeValuePair *nvp);
 bool equalsNodeValuePair(NodeValuePair *nvp1, NodeValuePair *nvp2);
 
-typedef Hashtable<NodeValuePair *, EncodingValue *, uintptr_t, 4, hashNodeValuePair, equalsNodeValuePair> NVPMap;
+typedef Hashtable<NodeValuePair *, EncodingValue *, uintptr_t, 0, hashNodeValuePair, equalsNodeValuePair> NVPMap;
 
 class EncodingSubGraph {
  public:
@@ -39,9 +47,15 @@ class EncodingSubGraph {
 	uint estimateNewSize(EncodingSubGraph *sg);
 	void traverseValue(EncodingNode *node, uint64_t value);
 	void computeEncodingValue();
-	void computeInequalities();
+	void computeComparisons();
+	void computeEqualities();
+	void solveComparisons();
+	void solveEquals();
 	void generateComparison(EncodingNode *left, EncodingNode *right);
+	void generateEquals(EncodingNode *left, EncodingNode *right);
+	void orderEV(EncodingValue *smaller, EncodingValue *larger);
 
+	HashsetEncodingValue values;
 	HashsetEncodingNode nodes;
 	NVPMap map;
 	uint encodingSize;