Add AST Hashing and Equals Functions

diff --git a/src/AST/asthash.cc b/src/AST/asthash.cc
new file mode 100644 (file)
index 0000000..c57ce90
--- /dev/null
+++ b/src/AST/asthash.cc
@@ -0,0 +1,104 @@
+#include "asthash.h"
+#include "mymemory.h"
+#include "structs.h"
+#include "boolean.h"
+#include "element.h"
+
+bool compareArray(Array<Boolean *> * inputs1, Array<Boolean *> *inputs2) {
+       if (inputs1->getSize() != inputs2->getSize())
+               return false;
+       for(uint i=0;i<inputs1->getSize();i++) {
+               if (inputs1->get(i) != inputs2->get(i))
+                       return false;
+       }
+       return true;
+}
+
+bool compareArray(Array<Element *> * inputs1, Array<Element *> *inputs2) {
+       if (inputs1->getSize() != inputs2->getSize())
+               return false;
+       for(uint i=0;i<inputs1->getSize();i++) {
+               if (inputs1->get(i) != inputs2->get(i))
+                       return false;
+       }
+       return true;
+}
+
+uint hashArray(Array<Boolean *> * inputs) {
+       uint hash = inputs->getSize();
+       for(uint i=0;i<inputs->getSize();i++) {
+               uint newval = (uint)(uintptr_t) inputs->get(i);
+               hash ^= newval;
+               hash = (hash << 3) | (hash >> 29);
+       }
+       return hash;
+}
+
+uint hashArray(Array<Element *> * inputs) {
+       uint hash = inputs->getSize();
+       for(uint i=0;i<inputs->getSize();i++) {
+               uint newval = (uint)(uintptr_t) inputs->get(i);
+               hash ^= newval;
+               hash = (hash << 3) | (hash >> 29);
+       }
+       return hash;
+}
+
+uint hashBoolean(Boolean * b) {
+       switch(b->type) {
+       case ORDERCONST: {
+               BooleanOrder * o=(BooleanOrder *)b;
+               return ((uint)(uintptr_t) o->order) ^ ((uint) o->first) ^ (((uint)(o->second)) << 2);
+       }
+       case BOOLEANVAR: {
+               return (uint)(uintptr_t) b;
+       }
+       case LOGICOP: {
+               BooleanLogic * l=(BooleanLogic *)b;
+               return ((uint)l->op) ^ hashArray(&l->inputs);
+       }
+       case PREDICATEOP: {
+               BooleanPredicate * p=(BooleanPredicate *)b;
+               return ((uint)(uintptr_t) p->predicate) ^
+                       (((uint)(uintptr_t) p->undefStatus) << 1) ^
+                       hashArray(&p->inputs);
+       }
+       default:
+               ASSERT(0);
+       }
+}
+
+bool compareBoolean(Boolean *b1, Boolean *b2) {
+       if (b1->type != b2->type)
+               return false;
+       switch(b1->type) {
+       case ORDERCONST: {
+               BooleanOrder * o1=(BooleanOrder *)b1;
+               BooleanOrder * o2=(BooleanOrder *)b2;
+               return (o1->order == o2->order) && (o1->first == o2->first) && (o1->second == o2->second);
+       }
+       case BOOLEANVAR: {
+               return b1 == b2;
+       }
+       case LOGICOP: {
+               BooleanLogic * l1=(BooleanLogic *)b1;
+               BooleanLogic * l2=(BooleanLogic *)b2;
+               return (l1->op == l2->op) && compareArray(&l1->inputs, &l2->inputs);
+       }
+       case PREDICATEOP: {
+               BooleanPredicate * p1=(BooleanPredicate *)b1;
+               BooleanPredicate * p2=(BooleanPredicate *)b2;
+               return (p1->predicate == p2->predicate) &&
+                       p1->undefStatus == p2->undefStatus &&
+                       compareArray(&p1->inputs, &p2->inputs);
+       }
+       default:
+               ASSERT(0);
+       }
+}
+
+uint hashElement(Element *element) {
+}
+
+bool compareElement(Element *e1, Element *e2) {
+}

diff --git a/src/AST/asthash.h b/src/AST/asthash.h
new file mode 100644 (file)
index 0000000..fccd963
--- /dev/null
+++ b/src/AST/asthash.h
@@ -0,0 +1,11 @@
+#ifndef ASTHASH_H
+#define ASTHASH_H
+#include "classlist.h"
+
+uint hashBoolean(Boolean * boolean);
+bool compareBoolean(Boolean *b1, Boolean *b2);
+
+uint hashElement(Element *element);
+bool compareElement(Element *e1, Element *e2);
+
+#endif

diff --git a/src/AST/boolean.cc b/src/AST/boolean.cc
index 6f2f4753bf2009bee5b31c6564710704750bdd7d..7949cdc16dc6cb3335ecd0f3de2e7ed4589c4c2d 100644 (file)
--- a/src/AST/boolean.cc
+++ b/src/AST/boolean.cc
@@ -9,7 +9,8 @@ Boolean::Boolean(ASTNodeType _type) :
        ASTNode(_type),
        polarity(P_UNDEFINED),
        boolVal(BV_UNDEFINED),
-       parents() {
+       parents(),
+       idNumber(0) {
 }
 
 BooleanVar::BooleanVar(VarType t) :

diff --git a/src/AST/boolean.h b/src/AST/boolean.h
index 755969f21608e8fcd57dcc74a2dc8aa0f432fc6b..81ce9b41495be0612d2bd378e8a922c733c9d292 100644 (file)
--- a/src/AST/boolean.h
+++ b/src/AST/boolean.h
@@ -16,6 +16,7 @@ public:
        Polarity polarity;
        BooleanValue boolVal;
        Vector<Boolean *> parents;
+
        MEMALLOC;
 };
 

diff --git a/src/AST/element.cc b/src/AST/element.cc
index e47d195eff65058896da811c77e90ef79c713c1f..2efbf7d9a8cd9685d3550e90e37271abe197386b 100644 (file)
--- a/src/AST/element.cc
+++ b/src/AST/element.cc
@@ -8,7 +8,8 @@
 
 Element::Element(ASTNodeType _type) :
        ASTNode(_type),
-       encoding(this) {
+       encoding(this),
+       idNumber(0) {
 }
 
 ElementSet::ElementSet(Set *s) :

diff --git a/src/AST/element.h b/src/AST/element.h
index 9f772adf4d99cfed7e7b697e7200490b3905aec2..8277b42b018159b57d896e3234c15217144ba0fb 100644 (file)
--- a/src/AST/element.h
+++ b/src/AST/element.h
@@ -15,6 +15,7 @@ public:
        Vector<ASTNode *> parents;
        ElementEncoding encoding;
        virtual Element *clone(CSolver *solver, CloneMap *map) {ASSERT(0); return NULL;};
+       
        MEMALLOC;
 };
 

diff --git a/src/csolver.cc b/src/csolver.cc
index 3131f3a1d1677e743a0760dccda9b3e65e2e5289..b6206315156c9e4f25779ad34b05184b4de97697 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -118,10 +118,10 @@ Element *CSolver::getElementConst(VarType type, uint64_t value) {
        return element;
 }
 
-Boolean *CSolver::getBooleanVar(VarType type) {
-       Boolean *boolean = new BooleanVar(type);
-       allBooleans.push(boolean);
-       return boolean;
+Element *CSolver::applyFunction(Function *function, Element **array, uint numArrays, Boolean *overflowstatus) {
+       Element *element = new ElementFunction(function,array,numArrays,overflowstatus);
+       allElements.push(element);
+       return element;
 }
 
 Function *CSolver::createFunctionOperator(ArithOp op, Set **domain, uint numDomain, Set *range,OverFlowBehavior overflowbehavior) {
@@ -162,10 +162,10 @@ Function *CSolver::completeTable(Table *table, UndefinedBehavior behavior) {
        return function;
 }
 
-Element *CSolver::applyFunction(Function *function, Element **array, uint numArrays, Boolean *overflowstatus) {
-       Element *element = new ElementFunction(function,array,numArrays,overflowstatus);
-       allElements.push(element);
-       return element;
+Boolean *CSolver::getBooleanVar(VarType type) {
+       Boolean *boolean = new BooleanVar(type);
+       allBooleans.push(boolean);
+       return boolean;
 }
 
 Boolean *CSolver::applyPredicate(Predicate *predicate, Element **inputs, uint numInputs) {
@@ -184,6 +184,12 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize)
        return boolean;
 }
 
+Boolean *CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second) {
+       Boolean *constraint = new BooleanOrder(order, first, second);
+       allBooleans.push(constraint);
+       return constraint;
+}
+
 void CSolver::addConstraint(Boolean *constraint) {
        constraints.add(constraint);
 }
@@ -194,12 +200,6 @@ Order *CSolver::createOrder(OrderType type, Set *set) {
        return order;
 }
 
-Boolean *CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second) {
-       Boolean *constraint = new BooleanOrder(order, first, second);
-       allBooleans.push(constraint);
-       return constraint;
-}
-
 int CSolver::startEncoding() {
        bool deleteTuner = false;
        if (tuner == NULL) {

diff --git a/src/csolver.h b/src/csolver.h
index 92900a19468eb386ce861b8c427e91638279c9d1..a3d4c2b1aef970f6272bea87ae59075d09b7c875 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -127,6 +127,8 @@ 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);
@@ -160,7 +162,9 @@ private:
        SATEncoder *satEncoder;
        bool unsat;
        Tuner *tuner;
-
+       uint booleanID;
+       uint elementID;
+       
        long long elapsedTime;
 };
 #endif