From 31bd7858d14dc5131a285a6a683ee89800374852 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Sun, 10 Sep 2017 16:15:33 -0700
Subject: [PATCH] More graph building

---
 src/AST/boolean.h                         | 10 +++----
 src/AST/predicate.cc                      |  2 +-
 src/AST/predicate.h                       |  4 ++-
 src/ASTAnalyses/Encoding/encodinggraph.cc | 36 +++++++++++++++++++++--
 src/ASTAnalyses/Encoding/encodinggraph.h  |  3 +-
 src/Backend/satfuncopencoder.cc           |  2 +-
 6 files changed, 45 insertions(+), 12 deletions(-)

diff --git a/src/AST/boolean.h b/src/AST/boolean.h
index 8be1d30..9d7e9ab 100644
--- a/src/AST/boolean.h
+++ b/src/AST/boolean.h
@@ -61,15 +61,15 @@ class BooleanPredicate : public Boolean {
 public:
 	BooleanPredicate(Predicate *_predicate, Element **_inputs, uint _numInputs, BooleanEdge _undefinedStatus);
 	Boolean *clone(CSolver *solver, CloneMap *map);
-
+	Predicate *getPredicate() {return predicate;}
+	FunctionEncoding *getFunctionEncoding() {return &encoding;}
+	void updateParents();
+	CMEMALLOC;
+	
 	Predicate *predicate;
 	FunctionEncoding encoding;
 	Array<Element *> inputs;
 	BooleanEdge undefStatus;
-	FunctionEncoding *getFunctionEncoding() {return &encoding;}
-	void updateParents();
-
-	CMEMALLOC;
 };
 
 class BooleanLogic : public Boolean {
diff --git a/src/AST/predicate.cc b/src/AST/predicate.cc
index d359811..f37d4cd 100644
--- a/src/AST/predicate.cc
+++ b/src/AST/predicate.cc
@@ -4,7 +4,7 @@
 #include "table.h"
 #include "csolver.h"
 
-PredicateOperator::PredicateOperator(CompOp _op, Set **domain, uint numDomain) : Predicate(OPERATORPRED), op(_op), domains(domain, numDomain) {
+PredicateOperator::PredicateOperator(CompOp _op, Set **domain, uint numDomain) : Predicate(OPERATORPRED), domains(domain, numDomain), op(_op) {
 }
 
 PredicateTable::PredicateTable(Table *_table, UndefinedBehavior _undefBehavior) : Predicate(TABLEPRED), table(_table), undefinedbehavior(_undefBehavior) {
diff --git a/src/AST/predicate.h b/src/AST/predicate.h
index 183a960..80515fa 100644
--- a/src/AST/predicate.h
+++ b/src/AST/predicate.h
@@ -21,9 +21,11 @@ public:
 	PredicateOperator(CompOp op, Set **domain, uint numDomain);
 	bool evalPredicateOperator(uint64_t *inputs);
 	Predicate *clone(CSolver *solver, CloneMap *map);
-	CompOp op;
+	CompOp getOp() {return op;}
 	Array<Set *> domains;
 	CMEMALLOC;
+ private:
+	CompOp op;
 };
 
 class PredicateTable : public Predicate {
diff --git a/src/ASTAnalyses/Encoding/encodinggraph.cc b/src/ASTAnalyses/Encoding/encodinggraph.cc
index a329e6b..8779975 100644
--- a/src/ASTAnalyses/Encoding/encodinggraph.cc
+++ b/src/ASTAnalyses/Encoding/encodinggraph.cc
@@ -2,6 +2,8 @@
 #include "iterator.h"
 #include "element.h"
 #include "function.h"
+#include "predicate.h"
+#include "set.h"
 
 EncodingGraph::EncodingGraph(CSolver * _solver) :
 	solver(_solver) {
@@ -58,6 +60,33 @@ void EncodingGraph::processFunction(ElementFunction *ef) {
 	}
 }
 
+void EncodingGraph::processPredicate(BooleanPredicate *b) {
+	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);
+		CompOp op=po->getOp();
+		switch(op) {
+		case SATC_EQUALS:
+			edge->numEquals++;
+			break;
+		case SATC_LT:
+		case SATC_LTE:
+		case SATC_GT:
+		case SATC_GTE:
+			edge->numComparisons++;
+			break;
+		default:
+			ASSERT(0);
+		}
+	}
+}
+
 EncodingEdge * EncodingGraph::getEdge(EncodingNode *left, EncodingNode *right, EncodingNode *dst) {
 	EncodingEdge e(left, right, dst);
 	EncodingEdge *result = edgeMap.get(&e);
@@ -68,14 +97,15 @@ EncodingEdge * EncodingGraph::getEdge(EncodingNode *left, EncodingNode *right, E
 	return result;
 }
 
-void EncodingGraph::processPredicate(BooleanPredicate *b) {
-}
-
 EncodingNode::EncodingNode(Set *_s) :
 	s(_s),
 	numElements(0) {
 }
 
+uint EncodingNode::getSize() {
+	return s->getSize();
+}
+
 EncodingNode * EncodingGraph::createNode(Element *e) {
 	if (e->type == ELEMCONST)
 		return NULL;
diff --git a/src/ASTAnalyses/Encoding/encodinggraph.h b/src/ASTAnalyses/Encoding/encodinggraph.h
index 12994da..7f7b8b4 100644
--- a/src/ASTAnalyses/Encoding/encodinggraph.h
+++ b/src/ASTAnalyses/Encoding/encodinggraph.h
@@ -30,6 +30,7 @@ class EncodingNode {
  public:
 	EncodingNode(Set *_s);
 	void addElement(Element *e);
+	uint getSize();
 	CMEMALLOC;
  private:
 	Set *s;
@@ -52,6 +53,6 @@ class EncodingEdge {
 	uint numComparisons;
 	friend uint hashEncodingEdge(EncodingEdge *edge);
 	friend bool equalsEncodingEdge(EncodingEdge *e1, EncodingEdge *e2);
-	fiend class EncodingGraph;
+	friend class EncodingGraph;
 };
 #endif
diff --git a/src/Backend/satfuncopencoder.cc b/src/Backend/satfuncopencoder.cc
index 7e6a67d..9fc3c41 100644
--- a/src/Backend/satfuncopencoder.cc
+++ b/src/Backend/satfuncopencoder.cc
@@ -204,7 +204,7 @@ Edge SATEncoder::encodeCircuitOperatorPredicateEncoder(BooleanPredicate *constra
 	ElementEncoding *ee1 = getElementEncoding(elem1);
 	ASSERT(ee0->numVars == ee1->numVars);
 	uint numVars = ee0->numVars;
-	switch (predicate->op) {
+	switch (predicate->getOp()) {
 	case SATC_EQUALS:
 		return generateEquivNVConstraint(cnf, numVars, ee0->variables, ee1->variables);
 	case SATC_LT:
-- 
2.34.1