From: bdemsky <bdemsky@uci.edu>
Date: Tue, 29 Aug 2017 03:12:43 +0000 (-0700)
Subject: Add AST Hashing and Equals Functions
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=9c5f7893454def1fd8899ae8944f414ce442d24e;p=satune.git
Add AST Hashing and Equals Functions
---
diff --git a/src/AST/asthash.cc b/src/AST/asthash.cc
new file mode 100644
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
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 6f2f475..7949cdc 100644
--- 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 755969f..81ce9b4 100644
--- 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 e47d195..2efbf7d 100644
--- 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 9f772ad..8277b42 100644
--- 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 3131f3a..b620631 100644
--- 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 92900a1..a3d4c2b 100644
--- 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