}
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) {
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);
#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();
}
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();
}
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();
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) {
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;
}
#include "tunable.h"
void DFS(OrderGraph *graph, Vector<OrderNode *> *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);
finishNodes->push(node);
}
}
- deleteIterOrderNode(iterator);
+ delete iterator;
}
void DFSReverse(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
}
void DFSNodeVisit(OrderNode *node, Vector<OrderNode *> *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;
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) {
}
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
Vector<OrderNode *> finishNodes;
DFS(graph, &finishNodes);
resetNodeInfoStatusSCC(graph);
- HashTableNodeToNodeSet *table = allocHashTableNodeToNodeSet(128, 0.25);
+ HashTableNodeToNodeSet *table = new HashTableNodeToNodeSet(128, 0.25);
Vector<OrderNode *> sccNodes;
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...
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<OrderNode *> *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);
finishNodes->push(node);
}
}
- deleteIterOrderNode(iterator);
+ delete iterator;
}
void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode *> *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
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) {
}
}
}
- deleteIterOrderEdge(iterator);
+ delete iterator;
}
/** This finds edges that must be positive and forces the inverse edge
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;
edge->polPos = false;
}
}
- deleteIterOrderEdge(iterator);
+ delete iterator;
}
void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
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;
}
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;
}
}
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);
}
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);
}
struct OrderNode {
uint64_t id;
- HashSetOrderEdge *inEdges;
- HashSetOrderEdge *outEdges;
+ HashSetOrderEdge * inEdges;
+ HashSetOrderEdge * outEdges;
NodeStatus status;
uint sccNum;
};
#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) {
}
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) {
FunctionEncodingType encType = constraint->encoding.type;
Array<Element*> * 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;
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);
ASSERT(undefStatus == IGNOREBEHAVIOR || undefStatus == FLAGFORCEUNDEFINED);
Array<Element *> *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];
}
constraints[i++] = row;
}
- deleteIterTableEntry(iterator);
+ delete iterator;
addConstraintCNF(This->cnf, constraintAND(This->cnf, size, constraints));
}
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))
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;
}
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;
}
#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<typename _Key>
+struct LinkNode {
+ _Key key;
+ LinkNode<_Key> *prev;
+ LinkNode<_Key> *next;
+};
+
+template<typename _Key, typename _KeyInt, int _Shift, unsigned int (*hash_function)(_Key), bool (*equals)(_Key, _Key)>
+class HashSet;
+
+template<typename _Key, typename _KeyInt, int _Shift, unsigned int (*hash_function)(_Key) = default_hash_function<_Key, _Shift, _KeyInt>, 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<typename _Key, typename _KeyInt, int _Shift = 0, unsigned int (*hash_function)(_Key) = default_hash_function<_Key, _Shift, _KeyInt>, 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
#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<typename _Key, typename _Val>
+struct hashlistnode {
+ _Key key;
+ _Val val;
+};
+
+template<typename _Key, int _Shift, typename _KeyInt>
+inline unsigned int default_hash_function(_Key hash) {
+ return (unsigned int)(((_KeyInt)hash) >> _Shift);
+}
+
+template<typename _Key>
+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<typename _Key, typename _Val, typename _KeyInt, int _Shift = 0, unsigned int (*hash_function)(_Key) = default_hash_function<_Key, _Shift, _KeyInt>, 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<capacity;i++) {
+ struct hashlistnode<_Key, _Val> *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<capacity;i++) {
+ struct hashlistnode<_Key, _Val> *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__ */
#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];
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++)
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);
#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<Boolean *, uintptr_t, 4> HashSetBoolean;
+typedef HashSet<TableEntry *, uintptr_t, 4, table_entry_hash_function, table_entry_equals> HashSetTableEntry;
+typedef HashSet<OrderNode *, uintptr_t, 4, order_node_hash_function, order_node_equals> HashSetOrderNode;
+typedef HashSet<OrderEdge *, uintptr_t, 4, order_edge_hash_function, order_edge_equals> HashSetOrderEdge;
+typedef HashSet<OrderElement *, uintptr_t, 4, order_element_hash_function, order_element_equals> HashSetOrderElement;
+typedef HashTable<OrderNode *, HashSetOrderNode *, uintptr_t, 4> HashTableNodeToNodeSet;
+typedef HashTable<OrderPair *, OrderPair *, uintptr_t, 4, order_pair_hash_function, order_pair_equals> HashTableOrderPair;
+
+typedef HSIterator<TableEntry *, uintptr_t, 4, table_entry_hash_function, table_entry_equals> HSIteratorTableEntry;
+typedef HSIterator<Boolean *, uintptr_t, 4> HSIteratorBoolean;
+typedef HSIterator<OrderEdge *, uintptr_t, 4, order_edge_hash_function, order_edge_equals> HSIteratorOrderEdge;
+typedef HSIterator<OrderNode *, uintptr_t, 4, order_node_hash_function, order_node_equals> HSIteratorOrderNode;
-HashTableDef(NodeToNodeSet, OrderNode *, HashSetOrderNode *);
#endif
#include <strings.h>
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) {
#include "mymemory.h"
#include <inttypes.h>
-#define bool int
-#define true 1
-#define false 0
class CSolver;
struct SATEncoder;
#include "polarityassignment.h"
CSolver::CSolver() : unsat(false) {
- constraints = allocDefHashSetBoolean();
tuner = allocTuner();
satEncoder = allocSATEncoder(this);
}
/** 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);
}
void CSolver::addConstraint(Boolean *constraint) {
- addHashSetBoolean(constraints, constraint);
+ constraints.add(constraint);
}
Order *CSolver::createOrder(OrderType type, Set *set) {
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<Boolean *> allBooleans;
projects / satune.git / commitdiff