From: bdemsky <bdemsky@uci.edu>
Date: Wed, 20 Sep 2017 00:16:04 +0000 (-0700)
Subject: Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/constraint_compiler
X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=15741847172c31b17658b9db8bdcfcf2e3297f57;hp=cac96bb8e95553aa23fe1f32744a8ed96f811103;p=satune.git

Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/constraint_compiler
---

diff --git a/src/ASTAnalyses/Encoding/encodinggraph.cc b/src/ASTAnalyses/Encoding/encodinggraph.cc
index 75a98b1..2aee670 100644
--- a/src/ASTAnalyses/Encoding/encodinggraph.cc
+++ b/src/ASTAnalyses/Encoding/encodinggraph.cc
@@ -63,15 +63,60 @@ void EncodingGraph::encode() {
 		case ELEMFUNCRETURN: {
 			ElementEncoding *encoding=e->getElementEncoding();
 			if (encoding->getElementEncodingType() == ELEM_UNASSIGNED) {
-				//Do assignment...
+				EncodingNode *n = getNode(e);
+				ASSERT(n != NULL);
+				ElementEncodingType encodetype=n->getEncoding();
+				encoding->setElementEncodingType(encodetype);
+				if (encodetype == UNARY || encodetype == ONEHOT) {
+					encoding->encodingArrayInitialization();
+				} else if (encodetype == BINARYINDEX) {
+					EncodingSubGraph * subgraph = graphMap.get(n);
+					uint encodingSize = subgraph->getEncodingSize(n);
+					uint paddedSize = encoding->getSizeEncodingArray(encodingSize);
+					encoding->allocInUseArrayElement(paddedSize);
+					encoding->allocEncodingArrayElement(paddedSize);
+					Set * s=e->getRange();
+					for(uint i=0;i<s->getSize();i++) {
+						uint64_t value=s->getElement(i);
+						uint encodingIndex=subgraph->getEncoding(n, value);
+						encoding->setInUseElement(encodingIndex);
+						encoding->encodingArray[encodingIndex] = value;
+					}
+				}
 			}
 			break;
 		}
 		default:
 			break;
 		}
+		encodeParent(e);
+	}
+}
+
+void EncodingGraph::encodeParent(Element *e) {
+	uint size=e->parents.getSize();
+	for(uint i=0;i<size;i++) {
+		ASTNode * n = e->parents.get(i);
+		if (n->type==PREDICATEOP) {
+			BooleanPredicate *b=(BooleanPredicate *)n;
+			FunctionEncoding *fenc=b->getFunctionEncoding();
+			if (fenc->getFunctionEncodingType() != FUNC_UNASSIGNED)
+				continue;
+			Predicate *p=b->getPredicate();
+			if (p->type==OPERATORPRED) {
+				PredicateOperator *po=(PredicateOperator *)p;
+				ASSERT(b->inputs.getSize()==2);
+				EncodingNode *left=createNode(b->inputs.get(0));
+				EncodingNode *right=createNode(b->inputs.get(1));
+				if (left == NULL || right == NULL)
+					return;
+				EncodingEdge *edge=getEdge(left, right, NULL);
+				if (edge != NULL && edge->getEncoding() == EDGE_MATCH) {
+					fenc->setFunctionEncodingType(CIRCUIT);
+				}
+			}
+		}
 	}
-	
 }
 
 void EncodingGraph::mergeNodes(EncodingNode *first, EncodingNode *second) {
@@ -134,7 +179,7 @@ void EncodingGraph::processFunction(ElementFunction *ef) {
 		if (left == NULL && right == NULL)
 			return;
 		EncodingNode *dst=createNode(ef);
-		EncodingEdge *edge=getEdge(left, right, dst);
+		EncodingEdge *edge=createEdge(left, right, dst);
 		edge->numArithOps++;
 	}
 }
@@ -148,7 +193,7 @@ void EncodingGraph::processPredicate(BooleanPredicate *b) {
 		EncodingNode *right=createNode(b->inputs.get(1));
 		if (left == NULL || right == NULL)
 			return;
-		EncodingEdge *edge=getEdge(left, right, NULL);
+		EncodingEdge *edge=createEdge(left, right, NULL);
 		CompOp op=po->getOp();
 		switch(op) {
 		case SATC_EQUALS:
@@ -233,6 +278,12 @@ void EncodingGraph::decideEdges() {
 static TunableDesc EdgeEncodingDesc(EDGE_UNASSIGNED, EDGE_MATCH, EDGE_UNASSIGNED);
 
 EncodingEdge * EncodingGraph::getEdge(EncodingNode *left, EncodingNode *right, EncodingNode *dst) {
+	EncodingEdge e(left, right, dst);
+	EncodingEdge *result = edgeMap.get(&e);
+	return result;
+}
+
+EncodingEdge * EncodingGraph::createEdge(EncodingNode *left, EncodingNode *right, EncodingNode *dst) {
 	EncodingEdge e(left, right, dst);
 	EncodingEdge *result = edgeMap.get(&e);
 	if (result == NULL) {
@@ -293,6 +344,14 @@ EncodingNode * EncodingGraph::createNode(Element *e) {
 	return n;
 }
 
+EncodingNode * EncodingGraph::getNode(Element *e) {
+	if (e->type == ELEMCONST)
+		return NULL;
+	Set *s = e->getRange();
+	EncodingNode *n = encodingMap.get(s);
+	return n;
+}
+
 void EncodingNode::addElement(Element *e) {
 	elements.add(e);
 }
diff --git a/src/ASTAnalyses/Encoding/encodinggraph.h b/src/ASTAnalyses/Encoding/encodinggraph.h
index 5fe6d2a..ccd2a5c 100644
--- a/src/ASTAnalyses/Encoding/encodinggraph.h
+++ b/src/ASTAnalyses/Encoding/encodinggraph.h
@@ -20,13 +20,16 @@ class EncodingGraph {
 	HashtableNodeToSubGraph graphMap;
 	HashsetEncodingSubGraph subgraphs;
 	
+	void encodeParent(Element *e);
 	void decideEdges();
 	void mergeNodes(EncodingNode *first, EncodingNode *second);
 	void processElement(Element *e);
 	void processFunction(ElementFunction *f);
 	void processPredicate(BooleanPredicate *b);
 	EncodingNode * createNode(Element *e);
+	EncodingNode * getNode(Element *e);
 	EncodingEdge * getEdge(EncodingNode *left, EncodingNode *right, EncodingNode *dst);
+	EncodingEdge * createEdge(EncodingNode *left, EncodingNode *right, EncodingNode *dst);
 };
 
 class EncodingNode {
@@ -36,7 +39,7 @@ class EncodingNode {
 	uint getSize() const;
 	VarType getType() const;
 	void setEncoding(ElementEncodingType e) {encoding=e;}
-	
+	ElementEncodingType getEncoding() {return encoding;}
 	CMEMALLOC;
  private:
 	Set *s;
@@ -56,6 +59,8 @@ class EncodingEdge {
 	EncodingEdge(EncodingNode *_l, EncodingNode *_r, EncodingNode *_d);
 	void setEncoding(EdgeEncodingType e) {encoding=e;}
 	uint64_t getValue() const;
+	EdgeEncodingType getEncoding() {return encoding;}
+
 	CMEMALLOC;
 	
  private:
diff --git a/src/ASTAnalyses/Encoding/subgraph.cc b/src/ASTAnalyses/Encoding/subgraph.cc
index f75d7c8..50cc2d0 100644
--- a/src/ASTAnalyses/Encoding/subgraph.cc
+++ b/src/ASTAnalyses/Encoding/subgraph.cc
@@ -30,6 +30,12 @@ int sortEncodingValue(const void *p1, const void *p2) {
 		return 1;
 }
 
+uint EncodingSubGraph::getEncoding(EncodingNode *n, uint64_t val) {
+	NodeValuePair nvp(n, val);
+	EncodingValue *ev = map.get(&nvp);
+	return ev->encoding;
+}
+
 void EncodingSubGraph::solveEquals() {
 	Vector<EncodingValue *> toEncode;
 	Vector<bool> encodingArray;
diff --git a/src/ASTAnalyses/Encoding/subgraph.h b/src/ASTAnalyses/Encoding/subgraph.h
index 7738445..1f90e91 100644
--- a/src/ASTAnalyses/Encoding/subgraph.h
+++ b/src/ASTAnalyses/Encoding/subgraph.h
@@ -40,6 +40,8 @@ class EncodingSubGraph {
 	void addNode(EncodingNode *n);
 	SetIteratorEncodingNode * nodeIterator();
 	void encode();
+	uint getEncoding(EncodingNode *n, uint64_t val);
+	uint getEncodingSize(EncodingNode *n) { return maxEncodingVal;}
 	
 	CMEMALLOC;
  private: