From: bdemsky <bdemsky@uci.edu>
Date: Sat, 9 Sep 2017 07:08:02 +0000 (-0700)
Subject: More code towards graph
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=d9b1da6e3af3c3272e4782ca3983ff7771c03b36;p=satune.git

More code towards graph
---

diff --git a/src/ASTAnalyses/Encoding/encodinggraph.cc b/src/ASTAnalyses/Encoding/encodinggraph.cc
index 9c0a29e..070f639 100644
--- a/src/ASTAnalyses/Encoding/encodinggraph.cc
+++ b/src/ASTAnalyses/Encoding/encodinggraph.cc
@@ -47,15 +47,38 @@ void EncodingGraph::processFunction(ElementFunction *ef) {
 	Function *f=ef->getFunction();
 	if (f->type==OPERATORFUNC) {
 		FunctionOperator *fo=(FunctionOperator*)f;
-		ArithOp op=fo->op;
+		ASSERT(ef->inputs.getSize() == 2);
+		EncodingNode *left=createNode(ef->inputs.get(0));
+		EncodingNode *right=createNode(ef->inputs.get(1));
+		if (left == NULL && right == NULL)
+			return;
+		EncodingNode *dst=createNode(ef);
+		EncodingEdge *edge=getEdge(left, right, dst);
 	}
 }
 
+EncodingEdge * EncodingGraph::getEdge(EncodingNode *left, EncodingNode *right, EncodingNode *dst) {
+	EncodingEdge e(left, right, dst);
+	EncodingEdge *result = edgeMap.get(&e);
+	if (result == NULL) {
+		result=new EncodingEdge(left, right, dst);
+		edgeMap.put(result, result);
+	}
+	return result;
+}
+
 void EncodingGraph::processPredicate(BooleanPredicate *b) {
 
 }
 
+EncodingNode::EncodingNode(Set *_s) :
+	s(_s),
+	numElements(0) {
+}
+
 EncodingNode * EncodingGraph::createNode(Element *e) {
+	if (e->type == ELEMCONST)
+		return NULL;
 	Set *s = e->getRange();
 	EncodingNode *n = encodingMap.get(s);
 	if (n == NULL) {
@@ -63,6 +86,8 @@ EncodingNode * EncodingGraph::createNode(Element *e) {
 		encodingMap.put(s, n);
 	}
 	n->addElement(e);
+	if (discovered.add(e))
+		n->numElements++;
 	return n;
 }
 
@@ -73,14 +98,20 @@ void EncodingNode::addElement(Element *e) {
 EncodingEdge::EncodingEdge(EncodingNode *_l, EncodingNode *_r) :
 	left(_l),
 	right(_r),
-	dst(NULL)
+	dst(NULL),
+	numArithOps(0),
+	numEquals(0),
+	numComparisons(0)
 {
 }
 
 EncodingEdge::EncodingEdge(EncodingNode *_left, EncodingNode *_right, EncodingNode *_dst) :
 	left(_left),
 	right(_right),
-	dst(_dst)
+	dst(_dst),
+	numArithOps(0),
+	numEquals(0),
+	numComparisons(0)
 {
 }
 
diff --git a/src/ASTAnalyses/Encoding/encodinggraph.h b/src/ASTAnalyses/Encoding/encodinggraph.h
index adb467c..a7ccace 100644
--- a/src/ASTAnalyses/Encoding/encodinggraph.h
+++ b/src/ASTAnalyses/Encoding/encodinggraph.h
@@ -18,11 +18,12 @@ class EncodingGraph {
 	CSolver * solver;
 	HashtableEncoding encodingMap;
 	HashtableEdge edgeMap;
+	HashsetElement discovered;
 	void processElement(Element *e);
 	void processFunction(ElementFunction *f);
 	void processPredicate(BooleanPredicate *b);
 	EncodingNode * createNode(Element *e);
-
+	EncodingEdge * getEdge(EncodingNode *left, EncodingNode *right, EncodingNode *dst);
 };
 
 class EncodingNode {
@@ -33,6 +34,8 @@ class EncodingNode {
  private:
 	Set *s;
 	HashsetElement elements;
+	uint numElements;
+	friend class EncodingGraph;
 };
 
 class EncodingEdge {
@@ -44,10 +47,10 @@ class EncodingEdge {
 	EncodingNode *left;
 	EncodingNode *right;
 	EncodingNode *dst;
+	uint numArithOps;
+	uint numEquals;
+	uint numComparisons;
 	friend uint hashEncodingEdge(EncodingEdge *edge);
 	friend bool equalsEncodingEdge(EncodingEdge *e1, EncodingEdge *e2);
-
 };
-
-
 #endif