From 9a5247f652b1a8c78ac15d7e9142f77b9be064a6 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Thu, 21 Sep 2017 16:48:12 -0700
Subject: [PATCH] Bug patches

---
 src/ASTAnalyses/Encoding/encodinggraph.cc | 14 ++++++++++----
 src/ASTAnalyses/Encoding/encodinggraph.h  |  1 +
 src/ASTAnalyses/Encoding/subgraph.cc      |  5 ++---
 src/Test/ordertest.cc                     |  5 +++--
 4 files changed, 16 insertions(+), 9 deletions(-)

diff --git a/src/ASTAnalyses/Encoding/encodinggraph.cc b/src/ASTAnalyses/Encoding/encodinggraph.cc
index 6589976..ebe6d7a 100644
--- a/src/ASTAnalyses/Encoding/encodinggraph.cc
+++ b/src/ASTAnalyses/Encoding/encodinggraph.cc
@@ -124,6 +124,11 @@ void EncodingGraph::encodeParent(Element *e) {
 void EncodingGraph::mergeNodes(EncodingNode *first, EncodingNode *second) {
 	EncodingSubGraph *graph1=graphMap.get(first);
 	EncodingSubGraph *graph2=graphMap.get(second);
+	if (graph1 == NULL)
+		first->setEncoding(BINARYINDEX);
+	if (graph2 == NULL)
+		second->setEncoding(BINARYINDEX);
+
 	if (graph1 == NULL && graph2 == NULL) {
 		graph1 = new EncodingSubGraph();
 		subgraphs.add(graph1);
@@ -226,8 +231,8 @@ void EncodingGraph::decideEdges() {
 		EncodingNode *right = ee->right;
 		
 		if (ee->encoding != EDGE_UNASSIGNED ||
-				left->encoding != BINARYINDEX ||
-				right->encoding != BINARYINDEX)
+				!left->couldBeBinaryIndex() ||
+				!right->couldBeBinaryIndex())
 			continue;
 		
 		uint64_t eeValue = ee->getValue();
@@ -298,8 +303,8 @@ EncodingEdge * EncodingGraph::createEdge(EncodingNode *left, EncodingNode *right
 			v1=tmp;
 		}
 
-		if ((left != NULL && left->encoding==BINARYINDEX) &&
-				(right != NULL) && right->encoding==BINARYINDEX) {
+		if ((left != NULL && left->couldBeBinaryIndex()) &&
+				(right != NULL) && right->couldBeBinaryIndex()) {
 			EdgeEncodingType type=(EdgeEncodingType)solver->getTuner()->getVarTunable(v1, v2, EDGEENCODING, &EdgeEncodingDesc);
 			result->setEncoding(type);
 			if (type == EDGE_MATCH) {
@@ -340,6 +345,7 @@ EncodingNode * EncodingGraph::createNode(Element *e) {
 	if (n == NULL) {
 		n = new EncodingNode(s);
 		n->setEncoding((ElementEncodingType)solver->getTuner()->getVarTunable(n->getType(), NODEENCODING, &NodeEncodingDesc));
+		
 		encodingMap.put(s, n);
 	}
 	n->addElement(e);
diff --git a/src/ASTAnalyses/Encoding/encodinggraph.h b/src/ASTAnalyses/Encoding/encodinggraph.h
index ccd2a5c..301a74a 100644
--- a/src/ASTAnalyses/Encoding/encodinggraph.h
+++ b/src/ASTAnalyses/Encoding/encodinggraph.h
@@ -40,6 +40,7 @@ class EncodingNode {
 	VarType getType() const;
 	void setEncoding(ElementEncodingType e) {encoding=e;}
 	ElementEncodingType getEncoding() {return encoding;}
+	bool couldBeBinaryIndex() {return encoding == BINARYINDEX || encoding == ELEM_UNASSIGNED;}
 	CMEMALLOC;
  private:
 	Set *s;
diff --git a/src/ASTAnalyses/Encoding/subgraph.cc b/src/ASTAnalyses/Encoding/subgraph.cc
index 50cc2d0..afddea1 100644
--- a/src/ASTAnalyses/Encoding/subgraph.cc
+++ b/src/ASTAnalyses/Encoding/subgraph.cc
@@ -215,8 +215,6 @@ void EncodingSubGraph::computeComparisons() {
 		delete edgeit;
 	}
 	delete nodeit;
-	
-	
 }
 
 void EncodingSubGraph::orderEV(EncodingValue *earlier, EncodingValue *later) {
@@ -276,7 +274,8 @@ void EncodingSubGraph::generateComparison(EncodingNode *left, EncodingNode *righ
 				orderEV(last, rev);
 		}
 		if (lev != rev) {
-			if (rev == NULL || lVal < rVal) {
+			if (rev == NULL ||
+					(lev != NULL && lVal < rVal)) {
 				if (rev != NULL)
 					orderEV(lev, rev);
 				last = lev;
diff --git a/src/Test/ordertest.cc b/src/Test/ordertest.cc
index 9ffcab5..e2c46e0 100644
--- a/src/Test/ordertest.cc
+++ b/src/Test/ordertest.cc
@@ -13,8 +13,9 @@ int main(int numargs, char **argv) {
 	Order *order = solver->createOrder(SATC_TOTAL, s);
 	BooleanEdge b1 =  solver->orderConstraint(order, 5, 1);
 	BooleanEdge b2 =  solver->orderConstraint(order, 1, 4);
-	solver->addConstraint(b1);
-	solver->addConstraint(b2);
+
+	solver->addConstraint(solver->applyLogicalOperation(SATC_OR, b1, solver->applyLogicalOperation(SATC_NOT, b2)));
+	solver->addConstraint(solver->applyLogicalOperation(SATC_OR, b2, solver->applyLogicalOperation(SATC_NOT, b1)));
 	solver->serialize();
 	if (solver->solve() == 1){
 		printf("SAT\n");
-- 
2.34.1