From: bdemsky Date: Tue, 29 Aug 2017 03:12:43 +0000 (-0700) Subject: Add AST Hashing and Equals Functions X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=9c5f7893454def1fd8899ae8944f414ce442d24e 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 * inputs1, Array *inputs2) { + if (inputs1->getSize() != inputs2->getSize()) + return false; + for(uint i=0;igetSize();i++) { + if (inputs1->get(i) != inputs2->get(i)) + return false; + } + return true; +} + +bool compareArray(Array * inputs1, Array *inputs2) { + if (inputs1->getSize() != inputs2->getSize()) + return false; + for(uint i=0;igetSize();i++) { + if (inputs1->get(i) != inputs2->get(i)) + return false; + } + return true; +} + +uint hashArray(Array * inputs) { + uint hash = inputs->getSize(); + for(uint i=0;igetSize();i++) { + uint newval = (uint)(uintptr_t) inputs->get(i); + hash ^= newval; + hash = (hash << 3) | (hash >> 29); + } + return hash; +} + +uint hashArray(Array * inputs) { + uint hash = inputs->getSize(); + for(uint i=0;igetSize();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 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 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