From 1baf38f8e307dbf035530c976979be00f0a1d09e Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Mon, 28 Aug 2017 23:05:34 -0700
Subject: [PATCH] Deduplication Support

---
 src/AST/asthash.cc |  5 ++---
 src/AST/asthash.h  |  5 +++++
 src/csolver.cc     | 47 +++++++++++++++++++++++++++++++++++++---------
 src/csolver.h      |  9 +++++----
 4 files changed, 50 insertions(+), 16 deletions(-)

diff --git a/src/AST/asthash.cc b/src/AST/asthash.cc
index f2ed5ec..503ca0e 100644
--- a/src/AST/asthash.cc
+++ b/src/AST/asthash.cc
@@ -110,7 +110,7 @@ uint hashElement(Element *e) {
 	}
 	case ELEMCONST: {
 		ElementConst * ec=(ElementConst *) e;
-		return ((uint)(uintptr_t) ec->set) ^ ((uint) ec->value);
+		return ((uint) ec->value);
 	}
 	default:
 		ASSERT(0);
@@ -134,8 +134,7 @@ bool compareElement(Element *e1, Element *e2) {
 	case ELEMCONST: {
 		ElementConst * ec1=(ElementConst *) e1;
 		ElementConst * ec2=(ElementConst *) e2;
-		return (ec1->set == ec2->set) &&
-			(ec1->value == ec2->value);
+		return (ec1->value == ec2->value);
 	}
 	default:
 		ASSERT(0);
diff --git a/src/AST/asthash.h b/src/AST/asthash.h
index fccd963..1842152 100644
--- a/src/AST/asthash.h
+++ b/src/AST/asthash.h
@@ -1,6 +1,7 @@
 #ifndef ASTHASH_H
 #define ASTHASH_H
 #include "classlist.h"
+#include "hashtable.h"
 
 uint hashBoolean(Boolean * boolean);
 bool compareBoolean(Boolean *b1, Boolean *b2);
@@ -8,4 +9,8 @@ bool compareBoolean(Boolean *b1, Boolean *b2);
 uint hashElement(Element *element);
 bool compareElement(Element *e1, Element *e2);
 
+typedef HashTable<Boolean *, Boolean *, uintptr_t, 4, hashBoolean, compareBoolean> BooleanMatchMap;
+
+typedef HashTable<Element *, Element *, uintptr_t, 4, hashElement, compareElement> ElementMatchMap;
+
 #endif
diff --git a/src/csolver.cc b/src/csolver.cc
index b620631..06ecf78 100644
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -112,16 +112,31 @@ Element *CSolver::getElementVar(Set *set) {
 Element *CSolver::getElementConst(VarType type, uint64_t value) {
 	uint64_t array[] = {value};
 	Set *set = new Set(type, array, 1);
-	allSets.push(set);
 	Element *element = new ElementConst(value, type, set);
-	allElements.push(element);
-	return element;
+	Element *e = elemMap.get(element);
+	if (e == NULL) {
+		allSets.push(set);
+		allElements.push(element);
+		elemMap.put(element, element);
+		return element;
+	} else {
+		delete set;
+		delete element;
+		return e;
+	}
 }
 
 Element *CSolver::applyFunction(Function *function, Element **array, uint numArrays, Boolean *overflowstatus) {
 	Element *element = new ElementFunction(function,array,numArrays,overflowstatus);
-	allElements.push(element);
-	return element;
+	Element *e = elemMap.get(element);
+	if (e == NULL) {
+		allElements.push(element);
+		elemMap.put(element, element);
+		return element;
+	} else {
+		delete element;
+		return e;
+	}
 }
 
 Function *CSolver::createFunctionOperator(ArithOp op, Set **domain, uint numDomain, Set *range,OverFlowBehavior overflowbehavior) {
@@ -174,14 +189,28 @@ Boolean *CSolver::applyPredicate(Predicate *predicate, Element **inputs, uint nu
 
 Boolean *CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, uint numInputs, Boolean *undefinedStatus) {
 	BooleanPredicate *boolean = new BooleanPredicate(predicate, inputs, numInputs, undefinedStatus);
-	allBooleans.push(boolean);
-	return boolean;
+	Boolean * b = boolMap.get(boolean);
+	if (b == NULL) {
+		boolMap.put(boolean, boolean);
+		allBooleans.push(boolean);
+		return boolean;
+	} else {
+		delete boolean;
+		return b;
+	}
 }
 
 Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) {
 	Boolean *boolean = new BooleanLogic(this, op, array, asize);
-	allBooleans.push(boolean);
-	return boolean;
+	Boolean *b = boolMap.get(boolean);
+	if (b == NULL) {
+		boolMap.put(boolean, boolean);
+		allBooleans.push(boolean);
+		return boolean;		
+	} else {
+		delete boolean;
+		return b;
+	}
 }
 
 Boolean *CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second) {
diff --git a/src/csolver.h b/src/csolver.h
index a3d4c2b..63ee0fd 100644
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -3,6 +3,7 @@
 #include "classlist.h"
 #include "ops.h"
 #include "structs.h"
+#include "asthash.h"
 
 class CSolver {
 public:
@@ -127,8 +128,6 @@ public:
 	MEMALLOC;
 
 private:
-	void assignID(Boolean * b);
-	void assignID(Element * e);
 	void handleXORFalse(BooleanLogic *bexpr, Boolean *child);
 	void handleIMPLIESTrue(BooleanLogic *bexpr, Boolean *child);
 	void handleIMPLIESFalse(BooleanLogic *bexpr, Boolean *child);
@@ -159,11 +158,13 @@ private:
 	/** This is a vector of all function structs that we have allocated. */
 	Vector<Function *> allFunctions;
 
+	/** These two tables are used for deduplicating entries. */
+	BooleanMatchMap boolMap;
+	ElementMatchMap elemMap;
+	
 	SATEncoder *satEncoder;
 	bool unsat;
 	Tuner *tuner;
-	uint booleanID;
-	uint elementID;
 	
 	long long elapsedTime;
 };
-- 
2.34.1