Deduplication Support

diff --git a/src/AST/asthash.cc b/src/AST/asthash.cc
index f2ed5ecc2fb00361594a2458fe345f1a1be17b5c..503ca0ee1393862ace97bc726545a6b4ae56e4a8 100644 (file)
--- a/src/AST/asthash.cc
+++ b/src/AST/asthash.cc
@@ -110,7 +110,7 @@ uint hashElement(Element *e) {
        }
        case ELEMCONST: {
                ElementConst * ec=(ElementConst *) e;
        }
        case ELEMCONST: {
                ElementConst * ec=(ElementConst *) e;

-               return ((uint)(uintptr_t) ec->set) ^ ((uint) ec->value);
+               return ((uint) ec->value);

        }
        default:
                ASSERT(0);
        }
        default:
                ASSERT(0);


@@ -134,8 +134,7 @@ bool compareElement(Element *e1, Element *e2) {
        case ELEMCONST: {
                ElementConst * ec1=(ElementConst *) e1;
                ElementConst * ec2=(ElementConst *) 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);
        }
        default:
                ASSERT(0);

diff --git a/src/AST/asthash.h b/src/AST/asthash.h
index fccd963b469ef30834a62368f0731034ff478111..184215290d4d8112ea6fc01627f4a95e70b14f16 100644 (file)
--- a/src/AST/asthash.h
+++ b/src/AST/asthash.h
@@ -1,6 +1,7 @@
 #ifndef ASTHASH_H
 #define ASTHASH_H
 #include "classlist.h"
 #ifndef ASTHASH_H
 #define ASTHASH_H
 #include "classlist.h"

+#include "hashtable.h"

 
 uint hashBoolean(Boolean * boolean);
 bool compareBoolean(Boolean *b1, Boolean *b2);
 
 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);
 
 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
 #endif

diff --git a/src/csolver.cc b/src/csolver.cc
index b6206315156c9e4f25779ad34b05184b4de97697..06ecf78dddbb3b668ec36650879d81e5004affb2 100644 (file)
--- 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);
 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);
        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);
 }
 
 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) {
 }
 
 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);
 
 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);
 }
 
 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) {
 }
 
 Boolean *CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second) {

diff --git a/src/csolver.h b/src/csolver.h
index a3d4c2b1aef970f6272bea87ae59075d09b7c875..63ee0fdf057e84b155467f0f66a27105c1ba0813 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -3,6 +3,7 @@
 #include "classlist.h"
 #include "ops.h"
 #include "structs.h"
 #include "classlist.h"
 #include "ops.h"
 #include "structs.h"

+#include "asthash.h"

 
 class CSolver {
 public:
 
 class CSolver {
 public:


@@ -127,8 +128,6 @@ public:
        MEMALLOC;
 
 private:
        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);
        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;
 
        /** 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;
        SATEncoder *satEncoder;
        bool unsat;
        Tuner *tuner;

-       uint booleanID;
-       uint elementID;

        
        long long elapsedTime;
 };
        
        long long elapsedTime;
 };