Deduplication Support
authorbdemsky <bdemsky@uci.edu>
Tue, 29 Aug 2017 06:05:34 +0000 (23:05 -0700)
committerbdemsky <bdemsky@uci.edu>
Tue, 29 Aug 2017 06:05:34 +0000 (23:05 -0700)
src/AST/asthash.cc
src/AST/asthash.h
src/csolver.cc
src/csolver.h

index f2ed5ec..503ca0e 100644 (file)
@@ -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);
index fccd963..1842152 100644 (file)
@@ -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
index b620631..06ecf78 100644 (file)
@@ -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) {
index a3d4c2b..63ee0fd 100644 (file)
@@ -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;
 };