From: bdemsky Date: Fri, 25 Aug 2017 07:38:04 +0000 (-0700) Subject: Switch hashtable/hashset X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=7997cc8a8bbee380ba714aa52362374f2aa68ef1;p=satune.git Switch hashtable/hashset --- diff --git a/src/AST/order.cc b/src/AST/order.cc index 5443075..5d9fc4e 100644 --- a/src/AST/order.cc +++ b/src/AST/order.cc @@ -9,11 +9,11 @@ Order::Order(OrderType _type, Set *_set) : type(_type), set(_set), orderPairTabl } void Order::initializeOrderHashTable() { - orderPairTable = allocHashTableOrderPair(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR); + orderPairTable = new HashTableOrderPair(); } void Order::initializeOrderElementsHashTable() { - elementTable = allocHashSetOrderElement(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR); + elementTable = new HashSetOrderElement(); } void Order::addOrderConstraint(BooleanOrder *constraint) { @@ -27,11 +27,11 @@ void Order::setOrderEncodingType(OrderEncodingType type) { Order::~Order() { deleteOrderEncoding(&order); if (orderPairTable != NULL) { - resetAndDeleteHashTableOrderPair(orderPairTable); - deleteHashTableOrderPair(orderPairTable); + orderPairTable->resetanddelete(); + delete orderPairTable; } - if(elementTable != NULL){ - deleteHashSetOrderElement(elementTable); + if (elementTable != NULL) { + delete elementTable; } if (graph != NULL) { deleteOrderGraph(graph); diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc index b96a3b5..f659b4e 100644 --- a/src/AST/rewriter.cc +++ b/src/AST/rewriter.cc @@ -3,8 +3,8 @@ #include "csolver.h" void replaceBooleanWithTrue(CSolver * This, Boolean *bexpr) { - if (containsHashSetBoolean(This->constraints, bexpr)) { - removeHashSetBoolean(This->constraints, bexpr); + if (This->constraints.contains(bexpr)) { + This->constraints.remove(bexpr); } uint size = bexpr->parents.getSize(); @@ -32,9 +32,9 @@ void replaceBooleanWithTrue(CSolver * This, Boolean *bexpr) { } void replaceBooleanWithBoolean(CSolver * This, Boolean *oldb, Boolean *newb) { - if (containsHashSetBoolean(This->constraints, oldb)) { - removeHashSetBoolean(This->constraints, oldb); - addHashSetBoolean(This->constraints, newb); + if (This->constraints.contains(oldb)) { + This->constraints.remove(oldb); + This->constraints.add(newb); } uint size = oldb->parents.getSize(); @@ -134,9 +134,9 @@ void handleORFalse(CSolver * This, BooleanLogic *bexpr, Boolean *child) { } void replaceBooleanWithFalse(CSolver * This, Boolean *bexpr) { - if (containsHashSetBoolean(This->constraints, bexpr)) { + if (This->constraints.contains(bexpr)) { This->unsat=true; - removeHashSetBoolean(This->constraints, bexpr); + This->constraints.remove(bexpr); } uint size = bexpr->parents.getSize(); diff --git a/src/AST/table.cc b/src/AST/table.cc index b7d550c..016b3cc 100644 --- a/src/AST/table.cc +++ b/src/AST/table.cc @@ -8,7 +8,7 @@ Table::Table(Set **_domains, uint numDomain, Set *_range) : domains(_domains, numDomain), range(_range) { - entries = allocHashSetTableEntry(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR); + entries = new HashSetTableEntry(); } void Table::addNewTableEntry(uint64_t *inputs, uint inputSize, uint64_t result) { @@ -17,23 +17,23 @@ void Table::addNewTableEntry(uint64_t *inputs, uint inputSize, uint64_t result) ASSERT(result == true || result == false); #endif TableEntry *tb = allocTableEntry(inputs, inputSize, result); - bool status = addHashSetTableEntry(entries, tb); + bool status = entries->add(tb); ASSERT(status); } TableEntry * Table::getTableEntry(uint64_t *inputs, uint inputSize) { TableEntry *temp = allocTableEntry(inputs, inputSize, -1); - TableEntry *result = getHashSetTableEntry(entries, temp); + TableEntry *result = entries->get(temp); deleteTableEntry(temp); return result; } Table::~Table() { - HSIteratorTableEntry *iterator = iteratorTableEntry(entries); - while (hasNextTableEntry(iterator)) { - deleteTableEntry(nextTableEntry(iterator)); + HSIteratorTableEntry *iterator = entries->iterator(); + while (iterator->hasNext()) { + deleteTableEntry(iterator->next()); } - deleteIterTableEntry(iterator); - deleteHashSetTableEntry(entries); + delete iterator; + delete entries; } diff --git a/src/ASTAnalyses/orderencoder.cc b/src/ASTAnalyses/orderencoder.cc index 56cfdae..35ea575 100644 --- a/src/ASTAnalyses/orderencoder.cc +++ b/src/ASTAnalyses/orderencoder.cc @@ -10,9 +10,9 @@ #include "tunable.h" void DFS(OrderGraph *graph, Vector *finishNodes) { - HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes); - while (hasNextOrderNode(iterator)) { - OrderNode *node = nextOrderNode(iterator); + HSIteratorOrderNode *iterator = graph->nodes->iterator(); + while (iterator->hasNext()) { + OrderNode *node = iterator->next(); if (node->status == NOTVISITED) { node->status = VISITED; DFSNodeVisit(node, finishNodes, false, false, 0); @@ -20,7 +20,7 @@ void DFS(OrderGraph *graph, Vector *finishNodes) { finishNodes->push(node); } } - deleteIterOrderNode(iterator); + delete iterator; } void DFSReverse(OrderGraph *graph, Vector *finishNodes) { @@ -39,9 +39,9 @@ void DFSReverse(OrderGraph *graph, Vector *finishNodes) { } void DFSNodeVisit(OrderNode *node, Vector *finishNodes, bool isReverse, bool mustvisit, uint sccNum) { - HSIteratorOrderEdge *iterator = isReverse ? iteratorOrderEdge(node->inEdges) : iteratorOrderEdge(node->outEdges); - while (hasNextOrderEdge(iterator)) { - OrderEdge *edge = nextOrderEdge(iterator); + HSIteratorOrderEdge *iterator = isReverse ? node->inEdges->iterator() : node->outEdges->iterator(); + while (iterator->hasNext()) { + OrderEdge *edge = iterator->next(); if (mustvisit) { if (!edge->mustPos) continue; @@ -61,15 +61,15 @@ void DFSNodeVisit(OrderNode *node, Vector *finishNodes, bool isReve child->sccNum = sccNum; } } - deleteIterOrderEdge(iterator); + delete iterator; } void resetNodeInfoStatusSCC(OrderGraph *graph) { - HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes); - while (hasNextOrderNode(iterator)) { - nextOrderNode(iterator)->status = NOTVISITED; + HSIteratorOrderNode *iterator = graph->nodes->iterator(); + while (iterator->hasNext()) { + iterator->next()->status = NOTVISITED; } - deleteIterOrderNode(iterator); + delete iterator; } void computeStronglyConnectedComponentGraph(OrderGraph *graph) { @@ -81,57 +81,57 @@ void computeStronglyConnectedComponentGraph(OrderGraph *graph) { } bool isMustBeTrueNode(OrderNode* node){ - HSIteratorOrderEdge* iterator = iteratorOrderEdge(node->inEdges); - while(hasNextOrderEdge(iterator)){ - OrderEdge* edge = nextOrderEdge(iterator); + HSIteratorOrderEdge* iterator = node->inEdges->iterator(); + while(iterator->hasNext()){ + OrderEdge* edge = iterator->next(); if(!edge->mustPos) return false; } - deleteIterOrderEdge(iterator); - iterator = iteratorOrderEdge(node->outEdges); - while(hasNextOrderEdge(iterator)){ - OrderEdge* edge = nextOrderEdge(iterator); + delete iterator; + iterator = node->outEdges->iterator(); + while(iterator->hasNext()){ + OrderEdge* edge = iterator->next(); if(!edge->mustPos) return false; } - deleteIterOrderEdge(iterator); + delete iterator; return true; } void bypassMustBeTrueNode(CSolver *This, OrderGraph* graph, OrderNode* node){ - HSIteratorOrderEdge* iterin = iteratorOrderEdge(node->inEdges); - while(hasNextOrderEdge(iterin)){ - OrderEdge* inEdge = nextOrderEdge(iterin); + HSIteratorOrderEdge* iterin = node->inEdges->iterator(); + while(iterin->hasNext()){ + OrderEdge* inEdge = iterin->next(); OrderNode* srcNode = inEdge->source; - removeHashSetOrderEdge(srcNode->outEdges, inEdge); - HSIteratorOrderEdge* iterout = iteratorOrderEdge(node->outEdges); - while(hasNextOrderEdge(iterout)){ - OrderEdge* outEdge = nextOrderEdge(iterout); + srcNode->outEdges->remove(inEdge); + HSIteratorOrderEdge* iterout = node->outEdges->iterator(); + while(iterout->hasNext()){ + OrderEdge* outEdge = iterout->next(); OrderNode* sinkNode = outEdge->sink; - removeHashSetOrderEdge(sinkNode->inEdges, outEdge); + sinkNode->inEdges->remove(outEdge); //Adding new edge to new sink and src nodes ... OrderEdge *newEdge =getOrderEdgeFromOrderGraph(graph, srcNode, sinkNode); newEdge->mustPos = true; newEdge->polPos = true; if (newEdge->mustNeg) This->unsat = true; - addHashSetOrderEdge(srcNode->outEdges, newEdge); - addHashSetOrderEdge(sinkNode->inEdges, newEdge); + srcNode->outEdges->add(newEdge); + sinkNode->inEdges->add(newEdge); } - deleteIterOrderEdge(iterout); + delete iterout; } - deleteIterOrderEdge(iterin); + delete iterin; } void removeMustBeTrueNodes(CSolver *This, OrderGraph *graph) { - HSIteratorOrderNode* iterator = iteratorOrderNode(graph->nodes); - while(hasNextOrderNode(iterator)){ - OrderNode* node = nextOrderNode(iterator); + HSIteratorOrderNode* iterator = graph->nodes->iterator(); + while(iterator->hasNext()) { + OrderNode* node = iterator->next(); if(isMustBeTrueNode(node)){ bypassMustBeTrueNode(This,graph, node); } } - deleteIterOrderNode(iterator); + delete iterator; } /** This function computes a source set for every nodes, the set of @@ -143,7 +143,7 @@ void completePartialOrderGraph(OrderGraph *graph) { Vector finishNodes; DFS(graph, &finishNodes); resetNodeInfoStatusSCC(graph); - HashTableNodeToNodeSet *table = allocHashTableNodeToNodeSet(128, 0.25); + HashTableNodeToNodeSet *table = new HashTableNodeToNodeSet(128, 0.25); Vector sccNodes; @@ -151,8 +151,8 @@ void completePartialOrderGraph(OrderGraph *graph) { uint sccNum = 1; for (int i = size - 1; i >= 0; i--) { OrderNode *node = finishNodes.get(i); - HashSetOrderNode *sources = allocHashSetOrderNode(4, 0.25); - putNodeToNodeSet(table, node, sources); + HashSetOrderNode *sources = new HashSetOrderNode(4, 0.25); + table->put(node, sources); if (node->status == NOTVISITED) { //Need to do reverse traversal here... @@ -168,52 +168,52 @@ void completePartialOrderGraph(OrderGraph *graph) { for (uint j = 0; j < rSize; j++) { OrderNode *rnode = sccNodes.get(j); //Compute source sets - HSIteratorOrderEdge *iterator = iteratorOrderEdge(rnode->inEdges); - while (hasNextOrderEdge(iterator)) { - OrderEdge *edge = nextOrderEdge(iterator); + HSIteratorOrderEdge *iterator = rnode->inEdges->iterator(); + while (iterator->hasNext()) { + OrderEdge *edge = iterator->next(); OrderNode *parent = edge->source; if (edge->polPos) { - addHashSetOrderNode(sources, parent); - HashSetOrderNode *parent_srcs = (HashSetOrderNode *)getNodeToNodeSet(table, parent); - addAllHashSetOrderNode(sources, parent_srcs); + sources->add(parent); + HashSetOrderNode *parent_srcs = (HashSetOrderNode *)table->get(parent); + sources->addAll(parent_srcs); } } - deleteIterOrderEdge(iterator); + delete iterator; } for (uint j=0; j < rSize; j++) { //Copy in set of entire SCC OrderNode *rnode = sccNodes.get(j); - HashSetOrderNode * set = (j==0) ? sources : copyHashSetOrderNode(sources); - putNodeToNodeSet(table, rnode, set); + HashSetOrderNode * set = (j==0) ? sources : sources->copy(); + table->put(rnode, set); //Use source sets to compute pseudoPos edges - HSIteratorOrderEdge *iterator = iteratorOrderEdge(rnode->inEdges); - while (hasNextOrderEdge(iterator)) { - OrderEdge *edge = nextOrderEdge(iterator); + HSIteratorOrderEdge *iterator = node->inEdges->iterator(); + while (iterator->hasNext()) { + OrderEdge *edge = iterator->next(); OrderNode *parent = edge->source; ASSERT(parent != rnode); if (edge->polNeg && parent->sccNum != rnode->sccNum && - containsHashSetOrderNode(sources, parent)) { + sources->contains(parent)) { OrderEdge *newedge = getOrderEdgeFromOrderGraph(graph, rnode, parent); newedge->pseudoPos = true; } } - deleteIterOrderEdge(iterator); + delete iterator; } sccNodes.clear(); } } - resetAndDeleteHashTableNodeToNodeSet(table); - deleteHashTableNodeToNodeSet(table); + table->resetanddelete(); + delete table; resetNodeInfoStatusSCC(graph); } void DFSMust(OrderGraph *graph, Vector *finishNodes) { - HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes); - while (hasNextOrderNode(iterator)) { - OrderNode *node = nextOrderNode(iterator); + HSIteratorOrderNode *iterator = graph->nodes->iterator(); + while (iterator->hasNext()) { + OrderNode *node = iterator->next(); if (node->status == NOTVISITED) { node->status = VISITED; DFSNodeVisit(node, finishNodes, false, true, 0); @@ -221,81 +221,81 @@ void DFSMust(OrderGraph *graph, Vector *finishNodes) { finishNodes->push(node); } } - deleteIterOrderNode(iterator); + delete iterator; } void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector *finishNodes, bool computeTransitiveClosure) { uint size = finishNodes->getSize(); - HashTableNodeToNodeSet *table = allocHashTableNodeToNodeSet(128, 0.25); + HashTableNodeToNodeSet *table = new HashTableNodeToNodeSet(128, 0.25); for (int i = size - 1; i >= 0; i--) { OrderNode *node = finishNodes->get(i); - HashSetOrderNode *sources = allocHashSetOrderNode(4, 0.25); - putNodeToNodeSet(table, node, sources); + HashSetOrderNode *sources = new HashSetOrderNode(4, 0.25); + table->put(node, sources); { //Compute source sets - HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->inEdges); - while (hasNextOrderEdge(iterator)) { - OrderEdge *edge = nextOrderEdge(iterator); + HSIteratorOrderEdge *iterator = node->inEdges->iterator(); + while (iterator->hasNext()) { + OrderEdge *edge = iterator->next(); OrderNode *parent = edge->source; if (edge->mustPos) { - addHashSetOrderNode(sources, parent); - HashSetOrderNode *parent_srcs = (HashSetOrderNode *)getNodeToNodeSet(table, parent); - addAllHashSetOrderNode(sources, parent_srcs); + sources->add(parent); + HashSetOrderNode *parent_srcs = (HashSetOrderNode *) table->get(parent); + sources->addAll(parent_srcs); } } - deleteIterOrderEdge(iterator); + delete iterator; } if (computeTransitiveClosure) { //Compute full transitive closure for nodes - HSIteratorOrderNode *srciterator = iteratorOrderNode(sources); - while (hasNextOrderNode(srciterator)) { - OrderNode *srcnode = nextOrderNode(srciterator); + HSIteratorOrderNode *srciterator = sources->iterator(); + while (srciterator->hasNext()) { + OrderNode *srcnode = srciterator->next(); OrderEdge *newedge = getOrderEdgeFromOrderGraph(graph, srcnode, node); newedge->mustPos = true; newedge->polPos = true; if (newedge->mustNeg) solver->unsat = true; - addHashSetOrderEdge(srcnode->outEdges,newedge); - addHashSetOrderEdge(node->inEdges,newedge); + srcnode->outEdges->add(newedge); + node->inEdges->add(newedge); } - deleteIterOrderNode(srciterator); + delete srciterator; } { //Use source sets to compute mustPos edges - HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->inEdges); - while (hasNextOrderEdge(iterator)) { - OrderEdge *edge = nextOrderEdge(iterator); + HSIteratorOrderEdge *iterator =node->inEdges->iterator(); + while (iterator->hasNext()) { + OrderEdge *edge = iterator->next(); OrderNode *parent = edge->source; - if (!edge->mustPos && containsHashSetOrderNode(sources, parent)) { + if (!edge->mustPos && sources->contains(parent)) { edge->mustPos = true; edge->polPos = true; if (edge->mustNeg) solver->unsat = true; } } - deleteIterOrderEdge(iterator); + delete iterator; } { //Use source sets to compute mustNeg for edges that would introduce cycle if true - HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->outEdges); - while (hasNextOrderEdge(iterator)) { - OrderEdge *edge = nextOrderEdge(iterator); + HSIteratorOrderEdge *iterator = node->outEdges->iterator(); + while (iterator->hasNext()) { + OrderEdge *edge = iterator->next(); OrderNode *child = edge->sink; - if (!edge->mustNeg && containsHashSetOrderNode(sources, child)) { + if (!edge->mustNeg && sources->contains(child)) { edge->mustNeg = true; edge->polNeg = true; if (edge->mustPos) solver->unsat = true; } } - deleteIterOrderEdge(iterator); + delete iterator; } } - resetAndDeleteHashTableNodeToNodeSet(table); - deleteHashTableNodeToNodeSet(table); + table->resetanddelete(); + delete table; } /* This function finds edges that would form a cycle with must edges @@ -318,9 +318,9 @@ void reachMustAnalysis(CSolver * solver, OrderGraph *graph, bool computeTransiti had one). */ void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph) { - HSIteratorOrderEdge *iterator = iteratorOrderEdge(graph->edges); - while (hasNextOrderEdge(iterator)) { - OrderEdge *edge = nextOrderEdge(iterator); + HSIteratorOrderEdge *iterator = graph->edges->iterator(); + while (iterator->hasNext()) { + OrderEdge *edge = iterator->next(); if (edge->mustPos) { OrderEdge *invEdge = getInverseOrderEdge(graph, edge); if (invEdge != NULL) { @@ -334,7 +334,7 @@ void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph) { } } } - deleteIterOrderEdge(iterator); + delete iterator; } /** This finds edges that must be positive and forces the inverse edge @@ -343,9 +343,9 @@ void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph) { polarity. */ void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph) { - HSIteratorOrderEdge *iterator = iteratorOrderEdge(graph->edges); - while (hasNextOrderEdge(iterator)) { - OrderEdge *edge = nextOrderEdge(iterator); + HSIteratorOrderEdge *iterator = graph->edges->iterator(); + while (iterator->hasNext()) { + OrderEdge *edge = iterator->next(); if (edge->mustPos) { if (!edge->mustNeg) { edge->polNeg = false; @@ -366,7 +366,7 @@ void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph) { edge->polPos = false; } } - deleteIterOrderEdge(iterator); + delete iterator; } void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) { diff --git a/src/ASTAnalyses/ordergraph.cc b/src/ASTAnalyses/ordergraph.cc index a9d974d..ee970e1 100644 --- a/src/ASTAnalyses/ordergraph.cc +++ b/src/ASTAnalyses/ordergraph.cc @@ -7,8 +7,8 @@ OrderGraph *allocOrderGraph(Order *order) { OrderGraph *This = (OrderGraph *) ourmalloc(sizeof(OrderGraph)); - This->nodes = allocHashSetOrderNode(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR); - This->edges = allocHashSetOrderEdge(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR); + This->nodes = new HashSetOrderNode(); + This->edges = new HashSetOrderEdge(); This->order = order; return This; } @@ -110,43 +110,43 @@ void addMustOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, Boo OrderNode *getOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id) { OrderNode *node = allocOrderNode(id); - OrderNode *tmp = getHashSetOrderNode(graph->nodes, node); + OrderNode *tmp = graph->nodes->get(node); if ( tmp != NULL) { deleteOrderNode(node); node = tmp; } else { - addHashSetOrderNode(graph->nodes, node); + graph->nodes->add(node); } return node; } OrderNode *lookupOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id) { OrderNode node = {id, NULL, NULL, NOTVISITED, 0}; - OrderNode *tmp = getHashSetOrderNode(graph->nodes, &node); + OrderNode *tmp = graph->nodes->get(&node); return tmp; } OrderEdge *getOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end) { OrderEdge *edge = allocOrderEdge(begin, end); - OrderEdge *tmp = getHashSetOrderEdge(graph->edges, edge); + OrderEdge *tmp = graph->edges->get(edge); if ( tmp != NULL ) { deleteOrderEdge(edge); edge = tmp; } else { - addHashSetOrderEdge(graph->edges, edge); + graph->edges->add(edge); } return edge; } OrderEdge *lookupOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end) { OrderEdge edge = {begin, end, 0, 0, 0, 0, 0}; - OrderEdge *tmp = getHashSetOrderEdge(graph->edges, &edge); + OrderEdge *tmp = graph->edges->get(&edge); return tmp; } OrderEdge *getInverseOrderEdge(OrderGraph *graph, OrderEdge *edge) { OrderEdge inverseedge = {edge->sink, edge->source, false, false, false, false, false}; - OrderEdge *tmp = getHashSetOrderEdge(graph->edges, &inverseedge); + OrderEdge *tmp = graph->edges->get(&inverseedge); return tmp; } @@ -163,20 +163,20 @@ void addMustOrderConstraintToOrderGraph(OrderGraph *graph, BooleanOrder *bOrder) } void deleteOrderGraph(OrderGraph *graph) { - HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes); - while (hasNextOrderNode(iterator)) { - OrderNode *node = nextOrderNode(iterator); + HSIteratorOrderNode *iterator = graph->nodes->iterator(); + while (iterator->hasNext()) { + OrderNode *node = iterator->next(); deleteOrderNode(node); } - deleteIterOrderNode(iterator); + delete iterator; - HSIteratorOrderEdge *eiterator = iteratorOrderEdge(graph->edges); - while (hasNextOrderEdge(eiterator)) { - OrderEdge *edge = nextOrderEdge(eiterator); + HSIteratorOrderEdge *eiterator = graph->edges->iterator(); + while (eiterator->hasNext()) { + OrderEdge *edge = eiterator->next(); deleteOrderEdge(edge); } - deleteIterOrderEdge(eiterator); - deleteHashSetOrderNode(graph->nodes); - deleteHashSetOrderEdge(graph->edges); + delete eiterator; + delete graph->nodes; + delete graph->edges; ourfree(graph); } diff --git a/src/ASTAnalyses/ordernode.cc b/src/ASTAnalyses/ordernode.cc index c0bd096..c197a57 100644 --- a/src/ASTAnalyses/ordernode.cc +++ b/src/ASTAnalyses/ordernode.cc @@ -4,25 +4,23 @@ OrderNode *allocOrderNode(uint64_t id) { OrderNode *This = (OrderNode *) ourmalloc(sizeof(OrderNode)); This->id = id; - This->inEdges = allocHashSetOrderEdge(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR); - This->outEdges = allocHashSetOrderEdge(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR); + This->inEdges = new HashSetOrderEdge(); + This->outEdges = new HashSetOrderEdge(); This->status = NOTVISITED; This->sccNum = 0; return This; } void addNewIncomingEdge(OrderNode *node, OrderEdge *edge) { - ASSERT(!containsHashSetOrderEdge(node->inEdges, edge)); // Only for testing ... Should be removed after testing - addHashSetOrderEdge(node->inEdges, edge); + node->inEdges->add(edge); } void addNewOutgoingEdge(OrderNode *node, OrderEdge *edge) { - ASSERT(!containsHashSetOrderEdge(node->outEdges, edge)); - addHashSetOrderEdge(node->outEdges, edge); + node->outEdges->add(edge); } void deleteOrderNode(OrderNode *node) { - deleteHashSetOrderEdge(node->inEdges); - deleteHashSetOrderEdge(node->outEdges); + delete node->inEdges; + delete node->outEdges; ourfree(node); } diff --git a/src/ASTAnalyses/ordernode.h b/src/ASTAnalyses/ordernode.h index 81e1993..4ac6083 100644 --- a/src/ASTAnalyses/ordernode.h +++ b/src/ASTAnalyses/ordernode.h @@ -19,8 +19,8 @@ typedef enum NodeStatus NodeStatus; struct OrderNode { uint64_t id; - HashSetOrderEdge *inEdges; - HashSetOrderEdge *outEdges; + HashSetOrderEdge * inEdges; + HashSetOrderEdge * outEdges; NodeStatus status; uint sccNum; }; diff --git a/src/ASTAnalyses/polarityassignment.cc b/src/ASTAnalyses/polarityassignment.cc index 909195b..3e4f4ab 100644 --- a/src/ASTAnalyses/polarityassignment.cc +++ b/src/ASTAnalyses/polarityassignment.cc @@ -2,14 +2,14 @@ #include "csolver.h" void computePolarities(CSolver *This) { - HSIteratorBoolean *iterator=iteratorBoolean(This->constraints); - while(hasNextBoolean(iterator)) { - Boolean *boolean = nextBoolean(iterator); + HSIteratorBoolean *iterator=This->constraints.iterator(); + while(iterator->hasNext()) { + Boolean *boolean = iterator->next(); updatePolarity(boolean, P_TRUE); updateMustValue(boolean, BV_MUSTBETRUE); computePolarityAndBooleanValue(boolean); } - deleteIterBoolean(iterator); + delete iterator; } void updatePolarity(Boolean *This, Polarity polarity) { diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc index b95e0b1..4b3189f 100644 --- a/src/Backend/satencoder.cc +++ b/src/Backend/satencoder.cc @@ -29,15 +29,15 @@ void deleteSATEncoder(SATEncoder *This) { } void encodeAllSATEncoder(CSolver *csolver, SATEncoder *This) { - HSIteratorBoolean *iterator=iteratorBoolean(csolver->constraints); - while(hasNextBoolean(iterator)) { - Boolean *constraint = nextBoolean(iterator); + HSIteratorBoolean *iterator=csolver->constraints.iterator(); + while(iterator->hasNext()) { + Boolean *constraint = iterator->next(); model_print("Encoding All ...\n\n"); Edge c = encodeConstraintSATEncoder(This, constraint); model_print("Returned Constraint in EncodingAll:\n"); addConstraintCNF(This->cnf, c); } - deleteIterBoolean(iterator); + delete iterator; } Edge encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) { diff --git a/src/Backend/satfunctableencoder.cc b/src/Backend/satfunctableencoder.cc index 035968f..0efe02c 100644 --- a/src/Backend/satfunctableencoder.cc +++ b/src/Backend/satfunctableencoder.cc @@ -18,16 +18,16 @@ Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder *This, BooleanPredicat FunctionEncodingType encType = constraint->encoding.type; Array * inputs = &constraint->inputs; uint inputNum = inputs->getSize(); - uint size = getSizeHashSetTableEntry(table->entries); + uint size = table->entries->getSize(); bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE; Edge constraints[size]; Edge undefConst = encodeConstraintSATEncoder(This, constraint->undefStatus); printCNF(undefConst); model_print("**\n"); - HSIteratorTableEntry *iterator = iteratorTableEntry(table->entries); + HSIteratorTableEntry *iterator = table->entries->iterator(); uint i = 0; - while (hasNextTableEntry(iterator)) { - TableEntry *entry = nextTableEntry(iterator); + while (iterator->hasNext()) { + TableEntry *entry = iterator->next(); if (generateNegation == (entry->output != 0) && undefStatus == IGNOREBEHAVIOR) { //Skip the irrelevant entries continue; @@ -60,7 +60,7 @@ Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder *This, BooleanPredicat model_print("\n\n"); } - deleteIterTableEntry(iterator); + delete iterator; ASSERT(i != 0); Edge result = generateNegation ? constraintNegate(constraintOR(This->cnf, i, constraints)) : constraintOR(This->cnf, i, constraints); @@ -181,12 +181,12 @@ void encodeEnumEntriesTableElemFuncSATEncoder(SATEncoder *This, ElementFunction ASSERT(undefStatus == IGNOREBEHAVIOR || undefStatus == FLAGFORCEUNDEFINED); Array *elements = &func->inputs; Table *table = ((FunctionTable *) (func->function))->table; - uint size = getSizeHashSetTableEntry(table->entries); + uint size = table->entries->getSize(); Edge constraints[size]; - HSIteratorTableEntry *iterator = iteratorTableEntry(table->entries); + HSIteratorTableEntry *iterator = table->entries->iterator(); uint i = 0; - while (hasNextTableEntry(iterator)) { - TableEntry *entry = nextTableEntry(iterator); + while (iterator->hasNext()) { + TableEntry *entry = iterator->next(); ASSERT(entry != NULL); uint inputNum = elements->getSize(); Edge carray[inputNum]; @@ -212,7 +212,7 @@ void encodeEnumEntriesTableElemFuncSATEncoder(SATEncoder *This, ElementFunction } constraints[i++] = row; } - deleteIterTableEntry(iterator); + delete iterator; addConstraintCNF(This->cnf, constraintAND(This->cnf, size, constraints)); } diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc index ecd811f..7cbcd7f 100644 --- a/src/Backend/satorderencoder.cc +++ b/src/Backend/satorderencoder.cc @@ -100,17 +100,18 @@ Edge inferOrderConstraintFromGraph(Order* order, uint64_t _first, uint64_t _seco Element* getOrderIntegerElement(SATEncoder* This,Order *order, uint64_t item) { HashSetOrderElement* eset = order->elementTable; OrderElement oelement ={item, NULL}; - if( !containsHashSetOrderElement(eset, &oelement)){ + if( !eset->contains(&oelement)){ Element* elem = new ElementSet(order->set); ElementEncoding* encoding = getElementEncoding(elem); setElementEncodingType(encoding, BINARYINDEX); encodingArrayInitialization(encoding); encodeElementSATEncoder(This, elem); - addHashSetOrderElement(eset, allocOrderElement(item, elem)); + eset->add(allocOrderElement(item, elem)); return elem; - }else - return getHashSetOrderElement(eset, &oelement)->elem; + } else + return eset->get(&oelement)->elem; } + Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair) { Edge gvalue = inferOrderConstraintFromGraph(order, pair->first, pair->second); if(!edgeIsNull(gvalue)) @@ -126,13 +127,13 @@ Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair) { pair = &flipped; } Edge constraint; - if (!containsOrderPair(table, pair)) { + if (!(table->contains(pair))) { constraint = getNewVarSATEncoder(This); OrderPair *paircopy = allocOrderPair(pair->first, pair->second, constraint); - putOrderPair(table, paircopy, paircopy); + table->put(paircopy, paircopy); } else - constraint = getOrderPair(table, pair)->constraint; - + constraint = table->get(pair)->constraint; + return negate ? constraintNegate(constraint) : constraint; } @@ -188,10 +189,10 @@ Edge getOrderConstraint(HashTableOrderPair *table, OrderPair *pair) { flipped.second = pair->first; pair = &flipped; } - if (!containsOrderPair(table, pair)) { + if (!table->contains(pair)) { return E_NULL; } - Edge constraint = getOrderPair(table, pair)->constraint; + Edge constraint = table->get(pair)->constraint; ASSERT(!edgeIsNull(constraint)); return negate ? constraintNegate(constraint) : constraint; } diff --git a/src/Collections/hashset.h b/src/Collections/hashset.h index 087046f..cc9a1df 100644 --- a/src/Collections/hashset.h +++ b/src/Collections/hashset.h @@ -11,197 +11,217 @@ #define HASH_SET_H #include "hashtable.h" -#define HashSetDef(Name, _Key) \ - struct LinkNode ## Name { \ - _Key key; \ - struct LinkNode ## Name *prev; \ - struct LinkNode ## Name *next; \ - }; \ - typedef struct LinkNode ## Name LinkNode ## Name; \ - struct HashSet ## Name; \ - typedef struct HashSet ## Name HashSet ## Name; \ - struct HSIterator ## Name { \ - LinkNode ## Name * curr; \ - LinkNode ## Name * last; \ - HashSet ## Name * set; \ - }; \ - typedef struct HSIterator ## Name HSIterator ## Name; \ - HashTableDef(Name ## Set, _Key, LinkNode ## Name *); \ - HSIterator ## Name * allocHSIterator ## Name(LinkNode ## Name * _curr, HashSet ## Name * _set); \ - void deleteIter ## Name(HSIterator ## Name * hsit); \ - bool hasNext ## Name(HSIterator ## Name * hsit); \ - _Key next ## Name(HSIterator ## Name * hsit); \ - _Key currKey ## Name(HSIterator ## Name * hsit); \ - void removeIter ## Name(HSIterator ## Name * hsit); \ - struct HashSet ## Name { \ - HashTable ## Name ## Set * table; \ - LinkNode ## Name * list; \ - LinkNode ## Name * tail; \ - }; \ - typedef struct HashSet ## Name HashSet ## Name; \ - \ - HashSet ## Name * allocHashSet ## Name (unsigned int initialcapacity, double factor); \ - HashSet ## Name * allocDefHashSet ## Name (); \ - void deleteHashSet ## Name(struct HashSet ## Name *set); \ - HashSet ## Name * copyHashSet ## Name(HashSet ## Name * set); \ - void resetHashSet ## Name(HashSet ## Name * set); \ - bool addHashSet ## Name(HashSet ## Name * set,_Key key); \ - void addAllHashSet ## Name(HashSet ## Name * set,HashSet ## Name * other); \ - _Key getHashSet ## Name(HashSet ## Name * set,_Key key); \ - _Key getHashSetFirstKey ## Name(HashSet ## Name * set); \ - bool containsHashSet ## Name(HashSet ## Name * set,_Key key); \ - bool removeHashSet ## Name(HashSet ## Name * set,_Key key); \ - unsigned int getSizeHashSet ## Name(HashSet ## Name * set); \ - bool isEmptyHashSet ## Name(HashSet ## Name * set); \ - HSIterator ## Name * iterator ## Name(HashSet ## Name * set); - - -#define HashSetImpl(Name, _Key, hash_function, equals) \ - HashTableImpl(Name ## Set, _Key, LinkNode ## Name *, hash_function, equals, ourfree); \ - HSIterator ## Name * allocHSIterator ## Name(LinkNode ## Name * _curr, HashSet ## Name * _set) { \ - HSIterator ## Name * hsit = (HSIterator ## Name *)ourmalloc(sizeof(HSIterator ## Name)); \ - hsit->curr = _curr; \ - hsit->set = _set; \ - return hsit; \ - } \ - \ - void deleteIter ## Name(HSIterator ## Name * hsit) { \ - ourfree(hsit); \ - } \ - \ - bool hasNext ## Name(HSIterator ## Name * hsit) { \ - return hsit->curr != NULL; \ - } \ - \ - _Key next ## Name(HSIterator ## Name * hsit) { \ - _Key k = hsit->curr->key; \ - hsit->last = hsit->curr; \ - hsit->curr = hsit->curr->next; \ - return k; \ - } \ - \ - _Key currKey ## Name(HSIterator ## Name * hsit) { \ - return hsit->last->key; \ - } \ - \ - void removeIter ## Name(HSIterator ## Name * hsit) { \ - _Key k = hsit->last->key; \ - removeHashSet ## Name(hsit->set, k); \ - } \ - \ - HashSet ## Name * allocDefHashSet ## Name () { \ - return allocHashSet ## Name(16, 0.25); \ - } \ - \ - HashSet ## Name * allocHashSet ## Name (unsigned int initialcapacity, double factor) { \ - HashSet ## Name * set = (HashSet ## Name *)ourmalloc(sizeof(struct HashSet ## Name)); \ - set->table = allocHashTable ## Name ## Set(initialcapacity, factor); \ - set->list = NULL; \ - set->tail = NULL; \ - return set; \ - } \ - \ - void deleteHashSet ## Name(struct HashSet ## Name *set) { \ - LinkNode ## Name *tmp = set->list; \ - while (tmp != NULL) { \ - LinkNode ## Name * tmpnext = tmp->next; \ - ourfree(tmp); \ - tmp = tmpnext; \ - } \ - deleteHashTable ## Name ## Set(set->table); \ - ourfree(set); \ - } \ - \ - HashSet ## Name * copyHashSet ## Name(HashSet ## Name * set) { \ - HashSet ## Name * copy = allocHashSet ## Name(getCapacity ## Name ## Set(set->table), getLoadFactor ## Name ## Set(set->table)); \ - HSIterator ## Name * it = iterator ## Name(set); \ - while (hasNext ## Name(it)) \ - addHashSet ## Name(copy, next ## Name(it)); \ - deleteIter ## Name(it); \ - return copy; \ - } \ - \ - void resetHashSet ## Name(HashSet ## Name * set) { \ - LinkNode ## Name * tmp = set->list; \ - while (tmp != NULL) { \ - LinkNode ## Name * tmpnext = tmp->next; \ - ourfree(tmp); \ - tmp = tmpnext; \ - } \ - set->list = set->tail = NULL; \ - reset ## Name ## Set(set->table); \ - } \ - \ - void addAllHashSet ## Name(HashSet ## Name * set, HashSet ## Name * other) { \ - HSIterator ## Name * it = iterator ## Name(other); \ - while (hasNext ## Name(it)) \ - addHashSet ## Name(set, next ## Name(it)); \ - deleteIter ## Name(it); \ - } \ - \ - bool addHashSet ## Name(HashSet ## Name * set,_Key key) { \ - LinkNode ## Name * val = get ## Name ## Set(set->table, key); \ - if (val == NULL) { \ - LinkNode ## Name * newnode = (LinkNode ## Name *)ourmalloc(sizeof(struct LinkNode ## Name)); \ - newnode->prev = set->tail; \ - newnode->next = NULL; \ - newnode->key = key; \ - if (set->tail != NULL) \ - set->tail->next = newnode; \ - else \ - set->list = newnode; \ - set->tail = newnode; \ - put ## Name ## Set(set->table, key, newnode); \ - return true; \ - } else \ - return false; \ - } \ - \ - _Key getHashSet ## Name(HashSet ## Name * set,_Key key) { \ - LinkNode ## Name * val = get ## Name ## Set(set->table, key); \ - if (val != NULL) \ - return val->key; \ - else \ - return NULL; \ - } \ - \ - _Key getHashSetFirstKey ## Name(HashSet ## Name * set) { \ - return set->list->key; \ - } \ - \ - bool containsHashSet ## Name(HashSet ## Name * set,_Key key) { \ - return get ## Name ## Set(set->table, key) != NULL; \ - } \ - \ - bool removeHashSet ## Name(HashSet ## Name * set,_Key key) { \ - LinkNode ## Name * oldlinknode; \ - oldlinknode = get ## Name ## Set(set->table, key); \ - if (oldlinknode == NULL) { \ - return false; \ - } \ - remove ## Name ## Set(set->table, key); \ - \ - if (oldlinknode->prev == NULL) \ - set->list = oldlinknode->next; \ - else \ - oldlinknode->prev->next = oldlinknode->next; \ - if (oldlinknode->next != NULL) \ - oldlinknode->next->prev = oldlinknode->prev; \ - else \ - set->tail = oldlinknode->prev; \ - ourfree(oldlinknode); \ - return true; \ - } \ - \ - unsigned int getSizeHashSet ## Name(HashSet ## Name * set) { \ - return getSizeTable ## Name ## Set(set->table); \ - } \ - \ - bool isEmptyHashSet ## Name(HashSet ## Name * set) { \ - return getSizeHashSet ## Name(set) == 0; \ - } \ - \ - HSIterator ## Name * iterator ## Name(HashSet ## Name * set) { \ - return allocHSIterator ## Name(set->list, set); \ +template +struct LinkNode { + _Key key; + LinkNode<_Key> *prev; + LinkNode<_Key> *next; +}; + +template +class HashSet; + +template, bool (*equals)(_Key, _Key) = default_equals<_Key> > +class HSIterator { +public: + HSIterator(LinkNode<_Key> *_curr, HashSet <_Key, _KeyInt, _Shift, hash_function, equals> * _set) : + curr(_curr), + set(_set) + { + } + + /** Override: new operator */ + void * operator new(size_t size) { + return ourmalloc(size); + } + + /** Override: delete operator */ + void operator delete(void *p, size_t size) { + ourfree(p); + } + + /** Override: new[] operator */ + void * operator new[](size_t size) { + return ourmalloc(size); + } + + /** Override: delete[] operator */ + void operator delete[](void *p, size_t size) { + ourfree(p); + } + + bool hasNext() { + return curr!=NULL; + } + + _Key next() { + _Key k=curr->key; + last=curr; + curr=curr->next; + return k; + } + + _Key currKey() { + return last->key; + } + + void remove() { + _Key k=last->key; + set->remove(k); + } + +private: + LinkNode<_Key> *curr; + LinkNode<_Key> *last; + HashSet <_Key, _KeyInt, _Shift, hash_function, equals> * set; +}; + +template, bool (*equals)(_Key, _Key) = default_equals<_Key> > +class HashSet { +public: + HashSet(unsigned int initialcapacity = 16, double factor = 0.5) : + table(new HashTable<_Key, LinkNode<_Key> *, _KeyInt, _Shift, hash_function, equals>(initialcapacity, factor)), + list(NULL), + tail(NULL) + { + } + + /** @brief Hashset destructor */ + ~HashSet() { + LinkNode<_Key> *tmp=list; + while(tmp!=NULL) { + LinkNode<_Key> *tmpnext=tmp->next; + ourfree(tmp); + tmp=tmpnext; + } + delete table; + } + + HashSet<_Key, _KeyInt, _Shift, hash_function, equals> * copy() { + HashSet<_Key, _KeyInt, _Shift, hash_function, equals> *copy=new HashSet<_Key, _KeyInt, _Shift, hash_function, equals>(table->getCapacity(), table->getLoadFactor()); + HSIterator<_Key, _KeyInt, _Shift, hash_function, equals> * it=iterator(); + while(it->hasNext()) + copy->add(it->next()); + delete it; + return copy; + } + + void reset() { + LinkNode<_Key> *tmp=list; + while(tmp!=NULL) { + LinkNode<_Key> *tmpnext=tmp->next; + ourfree(tmp); + tmp=tmpnext; + } + list=tail=NULL; + table->reset(); + } + + /** @brief Adds a new key to the hashset. Returns false if the key + * is already present. */ + + void addAll(HashSet<_Key, _KeyInt, _Shift, hash_function, equals> * table) { + HSIterator<_Key, _KeyInt, _Shift, hash_function, equals> * it=iterator(); + while(it->hasNext()) + add(it->next()); + delete it; + } + + /** @brief Adds a new key to the hashset. Returns false if the key + * is already present. */ + + bool add(_Key key) { + LinkNode<_Key> * val=table->get(key); + if (val==NULL) { + LinkNode<_Key> * newnode=(LinkNode<_Key> *)ourmalloc(sizeof(struct LinkNode<_Key>)); + newnode->prev=tail; + newnode->next=NULL; + newnode->key=key; + if (tail!=NULL) + tail->next=newnode; + else + list=newnode; + tail=newnode; + table->put(key, newnode); + return true; + } else + return false; + } + + /** @brief Gets the original key corresponding to this one from the + * hashset. Returns NULL if not present. */ + + _Key get(_Key key) { + LinkNode<_Key> * val=table->get(key); + if (val!=NULL) + return val->key; + else + return NULL; + } + + _Key getFirstKey() { + return list->key; + } + + bool contains(_Key key) { + return table->get(key)!=NULL; + } + + bool remove(_Key key) { + LinkNode<_Key> * oldlinknode; + oldlinknode=table->get(key); + if (oldlinknode==NULL) { + return false; + } + table->remove(key); + + //remove link node from the list + if (oldlinknode->prev==NULL) + list=oldlinknode->next; + else + oldlinknode->prev->next=oldlinknode->next; + if (oldlinknode->next!=NULL) + oldlinknode->next->prev=oldlinknode->prev; + else + tail=oldlinknode->prev; + ourfree(oldlinknode); + return true; + } + + unsigned int getSize() { + return table->getSize(); + } + + bool isEmpty() { + return getSize()==0; + } + + HSIterator<_Key, _KeyInt, _Shift, hash_function, equals> * iterator() { + return new HSIterator<_Key, _KeyInt, _Shift, hash_function, equals>(list, this); + } + + /** Override: new operator */ + void * operator new(size_t size) { + return ourmalloc(size); + } + + /** Override: delete operator */ + void operator delete(void *p, size_t size) { + ourfree(p); + } + + /** Override: new[] operator */ + void * operator new[](size_t size) { + return ourmalloc(size); + } + + /** Override: delete[] operator */ + void operator delete[](void *p, size_t size) { + ourfree(p); } +private: + HashTable<_Key, LinkNode<_Key>*, _KeyInt, _Shift, hash_function, equals> * table; + LinkNode<_Key> *list; + LinkNode<_Key> *tail; +}; #endif diff --git a/src/Collections/hashtable.h b/src/Collections/hashtable.h index 59e7ece..c33fe60 100644 --- a/src/Collections/hashtable.h +++ b/src/Collections/hashtable.h @@ -20,286 +20,345 @@ #include "mymemory.h" #include "common.h" -#define HT_DEFAULT_FACTOR 0.75 -#define HT_INITIAL_CAPACITY 16 +/** + * @brief HashTable node + * + * @tparam _Key Type name for the key + * @tparam _Val Type name for the values to be stored + */ +template +struct hashlistnode { + _Key key; + _Val val; +}; + +template +inline unsigned int default_hash_function(_Key hash) { + return (unsigned int)(((_KeyInt)hash) >> _Shift); +} + +template +inline bool default_equals(_Key key1, _Key key2) { + return key1 == key2; +} /** * @brief A simple, custom hash table * - * By default it is model_malloc, but you can pass in your own allocation - * functions. Note that This table does not support the value 0 (NULL) used as + * By default it is snapshotting, but you can pass in your own allocation + * functions. Note that this table does not support the value 0 (NULL) used as * a key and is designed primarily with pointer-based keys in mind. Other * primitive key types are supported only for non-zero values. * * @tparam _Key Type name for the key * @tparam _Val Type name for the values to be stored + * @tparam _KeyInt Integer type that is at least as large as _Key. Used for key + * manipulation and storage. + * @tparam _Shift Logical shift to apply to all keys. Default 0. */ -#define HashTableDef(Name, _Key, _Val)\ - struct hashlistnode ## Name { \ - _Key key; \ - _Val val; \ - }; \ - \ - struct HashTable ## Name { \ - struct hashlistnode ## Name *table; \ - struct hashlistnode ## Name *zero; \ - unsigned int capacity; \ - unsigned int size; \ - unsigned int capacitymask; \ - unsigned int threshold; \ - double loadfactor; \ - }; \ - \ - typedef struct HashTable ## Name HashTable ## Name; \ - HashTable ## Name * allocHashTable ## Name(unsigned int initialcapacity, double factor); \ - void deleteHashTable ## Name(HashTable ## Name * tab); \ - void reset ## Name(HashTable ## Name * tab); \ - void resetandfree ## Name(HashTable ## Name * tab); \ - void put ## Name(HashTable ## Name * tab, _Key key, _Val val); \ - _Val get ## Name(const HashTable ## Name * tab, _Key key); \ - _Val remove ## Name(HashTable ## Name * tab, _Key key); \ - unsigned int getSizeTable ## Name(const HashTable ## Name * tab); \ - bool contains ## Name(const HashTable ## Name * tab, _Key key); \ - void resize ## Name(HashTable ## Name * tab, unsigned int newsize); \ - double getLoadFactor ## Name(HashTable ## Name * tab); \ - unsigned int getCapacity ## Name(HashTable ## Name * tab); \ - void resetAndDeleteHashTable ## Name(HashTable ## Name * tab); - -#define HashTableImpl(Name, _Key, _Val, hash_function, equals, freefunction) \ - HashTable ## Name * allocHashTable ## Name(unsigned int initialcapacity, double factor) { \ - HashTable ## Name * tab = (HashTable ## Name *)ourmalloc(sizeof(HashTable ## Name)); \ - tab->table = (struct hashlistnode ## Name *)ourcalloc(initialcapacity, sizeof(struct hashlistnode ## Name)); \ - tab->zero = NULL; \ - tab->loadfactor = factor; \ - tab->capacity = initialcapacity; \ - tab->capacitymask = initialcapacity - 1; \ - \ - tab->threshold = (unsigned int)(initialcapacity * factor); \ - tab->size = 0; \ - return tab; \ - } \ - \ - void deleteHashTable ## Name(HashTable ## Name * tab) { \ - ourfree(tab->table); \ - if (tab->zero) \ - ourfree(tab->zero); \ - ourfree(tab); \ - } \ - \ - void resetAndDeleteHashTable ## Name(HashTable ## Name * tab) { \ - for (uint i = 0; i < tab->capacity; i++) { \ - struct hashlistnode ## Name *bin = &tab->table[i]; \ - if (bin->key != NULL) { \ - bin->key = NULL; \ - if (bin->val != NULL) { \ - freefunction(bin->val); \ - bin->val = NULL; \ - } \ - } \ - } \ - if (tab->zero) { \ - if (tab->zero->val != NULL) \ - freefunction(tab->zero->val); \ - ourfree(tab->zero); \ - tab->zero = NULL; \ - } \ - tab->size = 0; \ - } \ - \ - void reset ## Name(HashTable ## Name * tab) { \ - memset(tab->table, 0, tab->capacity * sizeof(struct hashlistnode ## Name)); \ - if (tab->zero) { \ - ourfree(tab->zero); \ - tab->zero = NULL; \ - } \ - tab->size = 0; \ - } \ - \ - void resetandfree ## Name(HashTable ## Name * tab) { \ - for (unsigned int i = 0; i < tab->capacity; i++) { \ - struct hashlistnode ## Name *bin = &tab->table[i]; \ - if (bin->key != NULL) { \ - bin->key = NULL; \ - if (bin->val != NULL) { \ - ourfree(bin->val); \ - bin->val = NULL; \ - } \ - } \ - } \ - if (tab->zero) { \ - if (tab->zero->val != NULL) \ - ourfree(tab->zero->val); \ - ourfree(tab->zero); \ - tab->zero = NULL; \ - } \ - tab->size = 0; \ - } \ - \ - void put ## Name(HashTable ## Name * tab, _Key key, _Val val) { \ - if (!key) { \ - if (!tab->zero) { \ - tab->zero = (struct hashlistnode ## Name *)ourmalloc(sizeof(struct hashlistnode ## Name)); \ - tab->size++; \ - } \ - tab->zero->key = key; \ - tab->zero->val = val; \ - return; \ - } \ - \ - if (tab->size > tab->threshold) \ - resize ## Name (tab, tab->capacity << 1); \ - \ - struct hashlistnode ## Name *search; \ - \ - unsigned int index = hash_function(key); \ - do { \ - index &= tab->capacitymask; \ - search = &tab->table[index]; \ - if (!search->key) { \ - break; \ - } \ - if (equals(search->key, key)) { \ - search->val = val; \ - return; \ - } \ - index++; \ - } while (true); \ - \ - search->key = key; \ - search->val = val; \ - tab->size++; \ - } \ - \ - _Val get ## Name(const HashTable ## Name * tab, _Key key) { \ - struct hashlistnode ## Name *search; \ - \ - if (!key) { \ - if (tab->zero) \ - return tab->zero->val; \ - else \ - return (_Val) 0; \ - } \ - \ - unsigned int oindex = hash_function(key) & tab->capacitymask; \ - unsigned int index = oindex; \ - do { \ - search = &tab->table[index]; \ - if (!search->key) { \ - if (!search->val) \ - break; \ - } else \ - if (equals(search->key, key)) \ - return search->val; \ - index++; \ - index &= tab->capacitymask; \ - if (index == oindex) \ - break; \ - } while (true); \ - return (_Val)0; \ - } \ - \ - _Val remove ## Name(HashTable ## Name * tab, _Key key) { \ - struct hashlistnode ## Name *search; \ - \ - if (!key) { \ - if (!tab->zero) { \ - return (_Val)0; \ - } else { \ - _Val v = tab->zero->val; \ - ourfree(tab->zero); \ - tab->zero = NULL; \ - tab->size--; \ - return v; \ - } \ - } \ - \ - unsigned int index = hash_function(key); \ - do { \ - index &= tab->capacitymask; \ - search = &tab->table[index]; \ - if (!search->key) { \ - if (!search->val) \ - break; \ - } else \ - if (equals(search->key, key)) { \ - _Val v = search->val; \ - search->val = (_Val) 1; \ - search->key = 0; \ - tab->size--; \ - return v; \ - } \ - index++; \ - } while (true); \ - return (_Val)0; \ - } \ - \ - unsigned int getSizeTable ## Name(const HashTable ## Name * tab) { \ - return tab->size; \ - } \ - \ - \ - bool contains ## Name(const HashTable ## Name * tab, _Key key) { \ - struct hashlistnode ## Name *search; \ - if (!key) { \ - return tab->zero != NULL; \ - } \ - unsigned int index = hash_function(key); \ - do { \ - index &= tab->capacitymask; \ - search = &tab->table[index]; \ - if (!search->key) { \ - if (!search->val) \ - break; \ - } else \ - if (equals(search->key, key)) \ - return true; \ - index++; \ - } while (true); \ - return false; \ - } \ - \ - void resize ## Name(HashTable ## Name * tab, unsigned int newsize) { \ - struct hashlistnode ## Name *oldtable = tab->table; \ - struct hashlistnode ## Name *newtable; \ - unsigned int oldcapacity = tab->capacity; \ - \ - if ((newtable = (struct hashlistnode ## Name *)ourcalloc(newsize, sizeof(struct hashlistnode ## Name))) == NULL) { \ - model_print("calloc error %s %d\n", __FILE__, __LINE__); \ - exit(EXIT_FAILURE); \ - } \ - \ - tab->table = newtable; \ - tab->capacity = newsize; \ - tab->capacitymask = newsize - 1; \ - \ - tab->threshold = (unsigned int)(newsize * tab->loadfactor); \ - \ - struct hashlistnode ## Name *bin = &oldtable[0]; \ - struct hashlistnode ## Name *lastbin = &oldtable[oldcapacity]; \ - for (; bin < lastbin; bin++) { \ - _Key key = bin->key; \ - \ - struct hashlistnode ## Name *search; \ - if (!key) \ - continue; \ - \ - unsigned int index = hash_function(key); \ - do { \ - index &= tab->capacitymask; \ - search = &tab->table[index]; \ - index++; \ - } while (search->key); \ - \ - search->key = key; \ - search->val = bin->val; \ - } \ - \ - ourfree(oldtable); \ - } \ - double getLoadFactor ## Name(HashTable ## Name * tab) {return tab->loadfactor;} \ - unsigned int getCapacity ## Name(HashTable ## Name * tab) {return tab->capacity;} +template, bool (*equals)(_Key, _Key) = default_equals<_Key> > +class HashTable { +public: + /** + * @brief Hash table constructor + * @param initialcapacity Sets the initial capacity of the hash table. + * Default size 1024. + * @param factor Sets the percentage full before the hashtable is + * resized. Default ratio 0.5. + */ + HashTable(unsigned int initialcapacity = 1024, double factor = 0.5) { + // Allocate space for the hash table + table = (struct hashlistnode<_Key, _Val> *)ourcalloc(initialcapacity, sizeof(struct hashlistnode<_Key, _Val>)); + zero = NULL; + loadfactor = factor; + capacity = initialcapacity; + capacitymask = initialcapacity - 1; + + threshold = (unsigned int)(initialcapacity * loadfactor); + size = 0; // Initial number of elements in the hash + } + + /** @brief Hash table destructor */ + ~HashTable() { + ourfree(table); + if (zero) + ourfree(zero); + } + + /** Override: new operator */ + void * operator new(size_t size) { + return ourmalloc(size); + } + + /** Override: delete operator */ + void operator delete(void *p, size_t size) { + ourfree(p); + } + + /** Override: new[] operator */ + void * operator new[](size_t size) { + return ourmalloc(size); + } + + /** Override: delete[] operator */ + void operator delete[](void *p, size_t size) { + ourfree(p); + } + + /** @brief Reset the table to its initial state. */ + void reset() { + memset(table, 0, capacity * sizeof(struct hashlistnode<_Key, _Val>)); + if (zero) { + ourfree(zero); + zero = NULL; + } + size = 0; + } + + void resetanddelete() { + for(unsigned int i=0;i *bin = &table[i]; + if (bin->key != NULL) { + bin->key = NULL; + if (bin->val != NULL) { + delete bin->val; + bin->val = NULL; + } + } + } + if (zero) { + if (zero->val != NULL) + delete zero->val; + ourfree(zero); + zero = NULL; + } + size = 0; + } + + void resetandfree() { + for(unsigned int i=0;i *bin = &table[i]; + if (bin->key != NULL) { + bin->key = NULL; + if (bin->val != NULL) { + ourfree(bin->val); + bin->val = NULL; + } + } + } + if (zero) { + if (zero->val != NULL) + ourfree(zero->val); + ourfree(zero); + zero = NULL; + } + size = 0; + } + + /** + * @brief Put a key/value pair into the table + * @param key The key for the new value; must not be 0 or NULL + * @param val The value to store in the table + */ + void put(_Key key, _Val val) { + /* HashTable cannot handle 0 as a key */ + if (!key) { + if (!zero) { + zero=(struct hashlistnode<_Key, _Val> *)ourmalloc(sizeof(struct hashlistnode<_Key, _Val>)); + size++; + } + zero->key=key; + zero->val=val; + return; + } + + if (size > threshold) + resize(capacity << 1); + + struct hashlistnode<_Key, _Val> *search; + + unsigned int index = hash_function(key); + do { + index &= capacitymask; + search = &table[index]; + if (!search->key) { + //key is null, probably done + break; + } + if (equals(search->key, key)) { + search->val = val; + return; + } + index++; + } while (true); + + search->key = key; + search->val = val; + size++; + } + + /** + * @brief Lookup the corresponding value for the given key + * @param key The key for finding the value; must not be 0 or NULL + * @return The value in the table, if the key is found; otherwise 0 + */ + _Val get(_Key key) const { + struct hashlistnode<_Key, _Val> *search; + + /* HashTable cannot handle 0 as a key */ + if (!key) { + if (zero) + return zero->val; + else + return (_Val) 0; + } + + unsigned int oindex = hash_function(key) & capacitymask; + unsigned int index=oindex; + do { + search = &table[index]; + if (!search->key) { + if (!search->val) + break; + } else + if (equals(search->key, key)) + return search->val; + index++; + index &= capacitymask; + if (index==oindex) + break; + } while (true); + return (_Val)0; + } + + /** + * @brief Remove the given key and return the corresponding value + * @param key The key for finding the value; must not be 0 or NULL + * @return The value in the table, if the key is found; otherwise 0 + */ + _Val remove(_Key key) { + struct hashlistnode<_Key, _Val> *search; + + /* HashTable cannot handle 0 as a key */ + if (!key) { + if (!zero) { + return (_Val)0; + } else { + _Val v=zero->val; + ourfree(zero); + zero=NULL; + size--; + return v; + } + } + + + unsigned int index = hash_function(key); + do { + index &= capacitymask; + search = &table[index]; + if (!search->key) { + if (!search->val) + break; + } else + if (equals(search->key, key)) { + _Val v=search->val; + //empty out this bin + search->val=(_Val) 1; + search->key=0; + size--; + return v; + } + index++; + } while (true); + return (_Val)0; + } + + unsigned int getSize() const { + return size; + } + + + /** + * @brief Check whether the table contains a value for the given key + * @param key The key for finding the value; must not be 0 or NULL + * @return True, if the key is found; false otherwise + */ + bool contains(_Key key) const { + struct hashlistnode<_Key, _Val> *search; + + /* HashTable cannot handle 0 as a key */ + if (!key) { + return zero!=NULL; + } + + unsigned int index = hash_function(key); + do { + index &= capacitymask; + search = &table[index]; + if (!search->key) { + if (!search->val) + break; + } else + if (equals(search->key, key)) + return true; + index++; + } while (true); + return false; + } + + /** + * @brief Resize the table + * @param newsize The new size of the table + */ + void resize(unsigned int newsize) { + struct hashlistnode<_Key, _Val> *oldtable = table; + struct hashlistnode<_Key, _Val> *newtable; + unsigned int oldcapacity = capacity; + + if ((newtable = (struct hashlistnode<_Key, _Val> *)ourcalloc(newsize, sizeof(struct hashlistnode<_Key, _Val>))) == NULL) { + model_print("calloc error %s %d\n", __FILE__, __LINE__); + exit(EXIT_FAILURE); + } + + table = newtable; // Update the global hashtable upon resize() + capacity = newsize; + capacitymask = newsize - 1; + + threshold = (unsigned int)(newsize * loadfactor); + + struct hashlistnode<_Key, _Val> *bin = &oldtable[0]; + struct hashlistnode<_Key, _Val> *lastbin = &oldtable[oldcapacity]; + for (;bin < lastbin;bin++) { + _Key key = bin->key; + + struct hashlistnode<_Key, _Val> *search; + if (!key) + continue; + unsigned int index = hash_function(key); + do { + index &= capacitymask; + search = &table[index]; + index++; + } while (search->key); + search->key = key; + search->val = bin->val; + } + ourfree(oldtable); // Free the memory of the old hash table + } + double getLoadFactor() {return loadfactor;} + unsigned int getCapacity() {return capacity;} + struct hashlistnode<_Key, _Val> *table; + struct hashlistnode<_Key, _Val> *zero; + unsigned int capacity; + unsigned int size; +private: + unsigned int capacitymask; + unsigned int threshold; + double loadfactor; +}; #endif/* __HASHTABLE_H__ */ diff --git a/src/Collections/structs.cc b/src/Collections/structs.cc index 10b2f83..a6e19f0 100644 --- a/src/Collections/structs.cc +++ b/src/Collections/structs.cc @@ -1,29 +1,13 @@ #include "mymemory.h" -#include "structs.h" #include "orderpair.h" #include "tableentry.h" #include "ordernode.h" #include "orderedge.h" #include "ordergraph.h" #include "orderelement.h" +#include "structs.h" -static inline unsigned int Ptr_hash_function(void *hash) { - return (unsigned int)((int64)hash >> 4); -} - -static inline bool Ptr_equals(void *key1, void *key2) { - return key1 == key2; -} - -static inline unsigned int order_pair_hash_function(OrderPair *This) { - return (uint) (This->first << 2) ^ This->second; -} - -static inline unsigned int order_pair_equals(OrderPair *key1, OrderPair *key2) { - return key1->first == key2->first && key1->second == key2->second; -} - -static inline unsigned int table_entry_hash_function(TableEntry *This) { +unsigned int table_entry_hash_function(TableEntry *This) { unsigned int h = 0; for (uint i = 0; i < This->inputSize; i++) { h += This->inputs[i]; @@ -32,7 +16,7 @@ static inline unsigned int table_entry_hash_function(TableEntry *This) { return h; } -static inline bool table_entry_equals(TableEntry *key1, TableEntry *key2) { +bool table_entry_equals(TableEntry *key1, TableEntry *key2) { if (key1->inputSize != key2->inputSize) return false; for (uint i = 0; i < key1->inputSize; i++) @@ -41,37 +25,35 @@ static inline bool table_entry_equals(TableEntry *key1, TableEntry *key2) { return true; } -static inline unsigned int order_node_hash_function(OrderNode *This) { +unsigned int order_node_hash_function(OrderNode *This) { return (uint) This->id; - } -static inline bool order_node_equals(OrderNode *key1, OrderNode *key2) { +bool order_node_equals(OrderNode *key1, OrderNode *key2) { return key1->id == key2->id; } -static inline unsigned int order_edge_hash_function(OrderEdge *This) { +unsigned int order_edge_hash_function(OrderEdge *This) { return (uint) (((uintptr_t)This->sink) ^ ((uintptr_t)This->source << 4)); } -static inline bool order_edge_equals(OrderEdge *key1, OrderEdge *key2) { +bool order_edge_equals(OrderEdge *key1, OrderEdge *key2) { return key1->sink == key2->sink && key1->source == key2->source; } -static inline unsigned int order_element_hash_function(OrderElement* This) { +unsigned int order_element_hash_function(OrderElement* This) { return (uint)This->item; } -static inline bool order_element_equals(OrderElement* key1, OrderElement* key2) { +bool order_element_equals(OrderElement* key1, OrderElement* key2) { return key1->item == key2->item; } +unsigned int order_pair_hash_function(OrderPair *This) { + return (uint) (This->first << 2) ^ This->second; +} -HashSetImpl(Boolean, Boolean *, Ptr_hash_function, Ptr_equals); -HashSetImpl(TableEntry, TableEntry *, table_entry_hash_function, table_entry_equals); -HashSetImpl(OrderNode, OrderNode *, order_node_hash_function, order_node_equals); -HashSetImpl(OrderEdge, OrderEdge *, order_edge_hash_function, order_edge_equals); -HashSetImpl(OrderElement, OrderElement *, order_element_hash_function, order_element_equals); +bool order_pair_equals(OrderPair *key1, OrderPair *key2) { + return key1->first == key2->first && key1->second == key2->second; +} -HashTableImpl(NodeToNodeSet, OrderNode *, HashSetOrderNode *, Ptr_hash_function, Ptr_equals, deleteHashSetOrderNode); -HashTableImpl(OrderPair, OrderPair *, OrderPair *, order_pair_hash_function, order_pair_equals, ourfree); diff --git a/src/Collections/structs.h b/src/Collections/structs.h index b153f3a..4a882fb 100644 --- a/src/Collections/structs.h +++ b/src/Collections/structs.h @@ -6,14 +6,28 @@ #include "classlist.h" #include "array.h" -HashTableDef(Void, void *, void *); -HashTableDef(OrderPair, OrderPair *, OrderPair *); +unsigned int table_entry_hash_function(TableEntry *This); +bool table_entry_equals(TableEntry *key1, TableEntry *key2); +unsigned int order_node_hash_function(OrderNode *This); +bool order_node_equals(OrderNode *key1, OrderNode *key2); +unsigned int order_edge_hash_function(OrderEdge *This); +bool order_edge_equals(OrderEdge *key1, OrderEdge *key2); +unsigned int order_element_hash_function(OrderElement* This); +bool order_element_equals(OrderElement* key1, OrderElement* key2); +unsigned int order_pair_hash_function(OrderPair *This); +bool order_pair_equals(OrderPair *key1, OrderPair *key2); -HashSetDef(Boolean, Boolean *); -HashSetDef(TableEntry, TableEntry *); -HashSetDef(OrderNode, OrderNode *); -HashSetDef(OrderEdge, OrderEdge *); -HashSetDef(OrderElement, OrderElement *); +typedef HashSet HashSetBoolean; +typedef HashSet HashSetTableEntry; +typedef HashSet HashSetOrderNode; +typedef HashSet HashSetOrderEdge; +typedef HashSet HashSetOrderElement; +typedef HashTable HashTableNodeToNodeSet; +typedef HashTable HashTableOrderPair; + +typedef HSIterator HSIteratorTableEntry; +typedef HSIterator HSIteratorBoolean; +typedef HSIterator HSIteratorOrderEdge; +typedef HSIterator HSIteratorOrderNode; -HashTableDef(NodeToNodeSet, OrderNode *, HashSetOrderNode *); #endif diff --git a/src/Encoders/naiveencoder.cc b/src/Encoders/naiveencoder.cc index 5ae9d85..5cd785c 100644 --- a/src/Encoders/naiveencoder.cc +++ b/src/Encoders/naiveencoder.cc @@ -14,12 +14,12 @@ #include void naiveEncodingDecision(CSolver *This) { - HSIteratorBoolean *iterator=iteratorBoolean(This->constraints); - while(hasNextBoolean(iterator)) { - Boolean *boolean = nextBoolean(iterator); + HSIteratorBoolean *iterator=This->constraints.iterator(); + while(iterator->hasNext()) { + Boolean *boolean = iterator->next(); naiveEncodingConstraint(boolean); } - deleteIterBoolean(iterator); + delete iterator; } void naiveEncodingConstraint(Boolean *This) { diff --git a/src/classlist.h b/src/classlist.h index 32230d0..1bdaff4 100644 --- a/src/classlist.h +++ b/src/classlist.h @@ -12,9 +12,6 @@ #include "mymemory.h" #include -#define bool int -#define true 1 -#define false 0 class CSolver; struct SATEncoder; diff --git a/src/csolver.cc b/src/csolver.cc index e8ea646..e2bb4bc 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -14,7 +14,6 @@ #include "polarityassignment.h" CSolver::CSolver() : unsat(false) { - constraints = allocDefHashSetBoolean(); tuner = allocTuner(); satEncoder = allocSATEncoder(this); } @@ -22,8 +21,6 @@ CSolver::CSolver() : unsat(false) { /** This function tears down the solver and the entire AST */ CSolver::~CSolver() { - deleteHashSetBoolean(constraints); - uint size = allBooleans.getSize(); for (uint i = 0; i < size; i++) { delete allBooleans.get(i); @@ -168,7 +165,7 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) } void CSolver::addConstraint(Boolean *constraint) { - addHashSetBoolean(constraints, constraint); + constraints.add(constraint); } Order *CSolver::createOrder(OrderType type, Set *set) { diff --git a/src/csolver.h b/src/csolver.h index b2741fd..d611e1d 100644 --- a/src/csolver.h +++ b/src/csolver.h @@ -14,7 +14,7 @@ class CSolver { Tuner *tuner; /** This is a vector of constraints that must be satisfied. */ - HashSetBoolean *constraints; + HashSetBoolean constraints; /** This is a vector of all boolean structs that we have allocated. */ Vector allBooleans;