From: bdemsky Date: Sat, 26 Aug 2017 20:19:33 +0000 (-0700) Subject: More conversion to classes X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=265f7ab437520507811eceb70d4b05f111a11ac5 More conversion to classes --- diff --git a/src/ASTAnalyses/orderedge.cc b/src/ASTAnalyses/orderedge.cc index c4632da..c0cd678 100644 --- a/src/ASTAnalyses/orderedge.cc +++ b/src/ASTAnalyses/orderedge.cc @@ -1,19 +1,12 @@ #include "orderedge.h" #include "ordergraph.h" -OrderEdge *allocOrderEdge(OrderNode *source, OrderNode *sink) { - OrderEdge *This = (OrderEdge *) ourmalloc(sizeof(OrderEdge)); - This->source = source; - This->sink = sink; - This->polPos = false; - This->polNeg = false; - This->mustPos = false; - This->mustNeg = false; - This->pseudoPos = false; - return This; +OrderEdge::OrderEdge(OrderNode *_source, OrderNode *_sink) { + source = _source; + sink = _sink; + polPos = false; + polNeg = false; + mustPos = false; + mustNeg = false; + pseudoPos = false; } - -void deleteOrderEdge(OrderEdge *This) { - ourfree(This); -} - diff --git a/src/ASTAnalyses/orderedge.h b/src/ASTAnalyses/orderedge.h index 21fa903..bbe6200 100644 --- a/src/ASTAnalyses/orderedge.h +++ b/src/ASTAnalyses/orderedge.h @@ -10,7 +10,10 @@ #include "classlist.h" #include "mymemory.h" -struct OrderEdge { +class OrderEdge { + public: + OrderEdge(OrderNode *begin, OrderNode *end); + OrderNode *source; OrderNode *sink; unsigned int polPos : 1; @@ -20,13 +23,5 @@ struct OrderEdge { unsigned int pseudoPos : 1; }; -OrderEdge *allocOrderEdge(OrderNode *begin, OrderNode *end); -void deleteOrderEdge(OrderEdge *This); -void setPseudoPos(OrderGraph *graph, OrderEdge *edge); -void setMustPos(OrderGraph *graph, OrderEdge *edge); -void setMustNeg(OrderGraph *graph, OrderEdge *edge); -void setPolPos(OrderGraph *graph, OrderEdge *edge); -void setPolNeg(OrderGraph *graph, OrderEdge *edge); - #endif/* ORDEREDGE_H */ diff --git a/src/ASTAnalyses/orderencoder.cc b/src/ASTAnalyses/orderencoder.cc index 05e2ae0..8eb56ad 100644 --- a/src/ASTAnalyses/orderencoder.cc +++ b/src/ASTAnalyses/orderencoder.cc @@ -39,7 +39,7 @@ void DFSReverse(OrderGraph *graph, Vector *finishNodes) { } void DFSNodeVisit(OrderNode *node, Vector *finishNodes, bool isReverse, bool mustvisit, uint sccNum) { - HSIteratorOrderEdge *iterator = isReverse ? node->inEdges->iterator() : node->outEdges->iterator(); + HSIteratorOrderEdge *iterator = isReverse ? node->inEdges.iterator() : node->outEdges.iterator(); while (iterator->hasNext()) { OrderEdge *edge = iterator->next(); if (mustvisit) { @@ -81,14 +81,14 @@ void computeStronglyConnectedComponentGraph(OrderGraph *graph) { } bool isMustBeTrueNode(OrderNode* node){ - HSIteratorOrderEdge* iterator = node->inEdges->iterator(); + HSIteratorOrderEdge* iterator = node->inEdges.iterator(); while(iterator->hasNext()){ OrderEdge* edge = iterator->next(); if(!edge->mustPos) return false; } delete iterator; - iterator = node->outEdges->iterator(); + iterator = node->outEdges.iterator(); while(iterator->hasNext()){ OrderEdge* edge = iterator->next(); if(!edge->mustPos) @@ -99,24 +99,24 @@ bool isMustBeTrueNode(OrderNode* node){ } void bypassMustBeTrueNode(CSolver *This, OrderGraph* graph, OrderNode* node){ - HSIteratorOrderEdge* iterin = node->inEdges->iterator(); + HSIteratorOrderEdge* iterin = node->inEdges.iterator(); while(iterin->hasNext()){ OrderEdge* inEdge = iterin->next(); OrderNode* srcNode = inEdge->source; - srcNode->outEdges->remove(inEdge); - HSIteratorOrderEdge* iterout = node->outEdges->iterator(); + srcNode->outEdges.remove(inEdge); + HSIteratorOrderEdge* iterout = node->outEdges.iterator(); while(iterout->hasNext()){ OrderEdge* outEdge = iterout->next(); OrderNode* sinkNode = outEdge->sink; - sinkNode->inEdges->remove(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; - srcNode->outEdges->add(newEdge); - sinkNode->inEdges->add(newEdge); + srcNode->outEdges.add(newEdge); + sinkNode->inEdges.add(newEdge); } delete iterout; } @@ -168,7 +168,7 @@ void completePartialOrderGraph(OrderGraph *graph) { for (uint j = 0; j < rSize; j++) { OrderNode *rnode = sccNodes.get(j); //Compute source sets - HSIteratorOrderEdge *iterator = rnode->inEdges->iterator(); + HSIteratorOrderEdge *iterator = rnode->inEdges.iterator(); while (iterator->hasNext()) { OrderEdge *edge = iterator->next(); OrderNode *parent = edge->source; @@ -187,7 +187,7 @@ void completePartialOrderGraph(OrderGraph *graph) { table->put(rnode, set); //Use source sets to compute pseudoPos edges - HSIteratorOrderEdge *iterator = node->inEdges->iterator(); + HSIteratorOrderEdge *iterator = node->inEdges.iterator(); while (iterator->hasNext()) { OrderEdge *edge = iterator->next(); OrderNode *parent = edge->source; @@ -235,7 +235,7 @@ void DFSClearContradictions(CSolver *solver, OrderGraph *graph, VectorinEdges->iterator(); + HSIteratorOrderEdge *iterator = node->inEdges.iterator(); while (iterator->hasNext()) { OrderEdge *edge = iterator->next(); OrderNode *parent = edge->source; @@ -257,14 +257,14 @@ void DFSClearContradictions(CSolver *solver, OrderGraph *graph, VectorpolPos = true; if (newedge->mustNeg) solver->unsat = true; - srcnode->outEdges->add(newedge); - node->inEdges->add(newedge); + srcnode->outEdges.add(newedge); + node->inEdges.add(newedge); } delete srciterator; } { //Use source sets to compute mustPos edges - HSIteratorOrderEdge *iterator =node->inEdges->iterator(); + HSIteratorOrderEdge *iterator =node->inEdges.iterator(); while (iterator->hasNext()) { OrderEdge *edge = iterator->next(); OrderNode *parent = edge->source; @@ -279,7 +279,7 @@ void DFSClearContradictions(CSolver *solver, OrderGraph *graph, VectoroutEdges->iterator(); + HSIteratorOrderEdge *iterator = node->outEdges.iterator(); while (iterator->hasNext()) { OrderEdge *edge = iterator->next(); OrderNode *child = edge->sink; diff --git a/src/ASTAnalyses/ordergraph.cc b/src/ASTAnalyses/ordergraph.cc index ee970e1..d81218e 100644 --- a/src/ASTAnalyses/ordergraph.cc +++ b/src/ASTAnalyses/ordergraph.cc @@ -43,8 +43,8 @@ void addOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, Boolean if (mustval == BV_MUSTBETRUE || mustval == BV_UNSAT) _1to2->mustPos = true; _1to2->polPos = true; - addNewOutgoingEdge(node1, _1to2); - addNewIncomingEdge(node2, _1to2); + node1->addNewOutgoingEdge(_1to2); + node2->addNewIncomingEdge(_1to2); if (constr->polarity == P_TRUE) break; } @@ -54,15 +54,15 @@ void addOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, Boolean if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT) _2to1->mustPos = true; _2to1->polPos = true; - addNewOutgoingEdge(node2, _2to1); - addNewIncomingEdge(node1, _2to1); + node2->addNewOutgoingEdge(_2to1); + node1->addNewIncomingEdge(_2to1); } else { OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2); if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT) _1to2->mustNeg = true; _1to2->polNeg = true; - addNewOutgoingEdge(node1, _1to2); - addNewIncomingEdge(node2, _1to2); + node1->addNewOutgoingEdge(_1to2); + node2->addNewIncomingEdge(_1to2); } break; } @@ -81,8 +81,8 @@ void addMustOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, Boo OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2); _1to2->mustPos = true; _1to2->polPos = true; - addNewOutgoingEdge(node1, _1to2); - addNewIncomingEdge(node2, _1to2); + node1->addNewOutgoingEdge(_1to2); + node2->addNewIncomingEdge(_1to2); if (constr->boolVal == BV_MUSTBETRUE) break; } @@ -91,14 +91,14 @@ void addMustOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, Boo OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(graph, node2, node1); _2to1->mustPos = true; _2to1->polPos = true; - addNewOutgoingEdge(node2, _2to1); - addNewIncomingEdge(node1, _2to1); + node2->addNewOutgoingEdge(_2to1); + node1->addNewIncomingEdge(_2to1); } else { OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2); _1to2->mustNeg = true; _1to2->polNeg = true; - addNewOutgoingEdge(node1, _1to2); - addNewIncomingEdge(node2, _1to2); + node1->addNewOutgoingEdge(_1to2); + node2->addNewIncomingEdge(_1to2); } break; } @@ -109,10 +109,10 @@ void addMustOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, Boo } OrderNode *getOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id) { - OrderNode *node = allocOrderNode(id); + OrderNode *node = new OrderNode(id); OrderNode *tmp = graph->nodes->get(node); if ( tmp != NULL) { - deleteOrderNode(node); + delete node; node = tmp; } else { graph->nodes->add(node); @@ -121,16 +121,16 @@ OrderNode *getOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id) { } OrderNode *lookupOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id) { - OrderNode node = {id, NULL, NULL, NOTVISITED, 0}; + OrderNode node(id); OrderNode *tmp = graph->nodes->get(&node); return tmp; } OrderEdge *getOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end) { - OrderEdge *edge = allocOrderEdge(begin, end); + OrderEdge *edge = new OrderEdge(begin, end); OrderEdge *tmp = graph->edges->get(edge); if ( tmp != NULL ) { - deleteOrderEdge(edge); + delete edge; edge = tmp; } else { graph->edges->add(edge); @@ -139,13 +139,13 @@ OrderEdge *getOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, Order } OrderEdge *lookupOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end) { - OrderEdge edge = {begin, end, 0, 0, 0, 0, 0}; + OrderEdge edge(begin, end); 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 inverseedge(edge->sink, edge->source); OrderEdge *tmp = graph->edges->get(&inverseedge); return tmp; } @@ -166,14 +166,14 @@ void deleteOrderGraph(OrderGraph *graph) { HSIteratorOrderNode *iterator = graph->nodes->iterator(); while (iterator->hasNext()) { OrderNode *node = iterator->next(); - deleteOrderNode(node); + delete node; } delete iterator; HSIteratorOrderEdge *eiterator = graph->edges->iterator(); while (eiterator->hasNext()) { OrderEdge *edge = eiterator->next(); - deleteOrderEdge(edge); + delete edge; } delete eiterator; delete graph->nodes; diff --git a/src/ASTAnalyses/ordernode.cc b/src/ASTAnalyses/ordernode.cc index c197a57..02f3146 100644 --- a/src/ASTAnalyses/ordernode.cc +++ b/src/ASTAnalyses/ordernode.cc @@ -1,26 +1,18 @@ #include "ordernode.h" #include "orderedge.h" -OrderNode *allocOrderNode(uint64_t id) { - OrderNode *This = (OrderNode *) ourmalloc(sizeof(OrderNode)); - This->id = id; - This->inEdges = new HashSetOrderEdge(); - This->outEdges = new HashSetOrderEdge(); - This->status = NOTVISITED; - This->sccNum = 0; - return This; +OrderNode::OrderNode(uint64_t _id) : + id(_id), + status(NOTVISITED), + sccNum(0), + inEdges(), + outEdges() { } -void addNewIncomingEdge(OrderNode *node, OrderEdge *edge) { - node->inEdges->add(edge); +void OrderNode::addNewIncomingEdge(OrderEdge *edge) { + inEdges.add(edge); } -void addNewOutgoingEdge(OrderNode *node, OrderEdge *edge) { - node->outEdges->add(edge); -} - -void deleteOrderNode(OrderNode *node) { - delete node->inEdges; - delete node->outEdges; - ourfree(node); +void OrderNode::addNewOutgoingEdge(OrderEdge *edge) { + outEdges.add(edge); } diff --git a/src/ASTAnalyses/ordernode.h b/src/ASTAnalyses/ordernode.h index 4ac6083..95862ae 100644 --- a/src/ASTAnalyses/ordernode.h +++ b/src/ASTAnalyses/ordernode.h @@ -17,18 +17,17 @@ enum NodeStatus {NOTVISITED, VISITED, FINISHED, ADDEDTOSET}; typedef enum NodeStatus NodeStatus; -struct OrderNode { +class OrderNode { + public: + OrderNode(uint64_t id); + void addNewIncomingEdge(OrderEdge *edge); + void addNewOutgoingEdge(OrderEdge *edge); + uint64_t id; - HashSetOrderEdge * inEdges; - HashSetOrderEdge * outEdges; NodeStatus status; uint sccNum; + HashSetOrderEdge inEdges; + HashSetOrderEdge outEdges; }; - -OrderNode *allocOrderNode(uint64_t id); -void addNewIncomingEdge(OrderNode *node, OrderEdge *edge); -void addNewOutgoingEdge(OrderNode *node, OrderEdge *edge); -void deleteOrderNode(OrderNode *node); - #endif/* ORDERNODE_H */ diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc index bada3f0..343c93a 100644 --- a/src/ASTTransform/integerencoding.cc +++ b/src/ASTTransform/integerencoding.cc @@ -32,11 +32,11 @@ void orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder){ Element* getOrderIntegerElement(SATEncoder* This,Order *order, uint64_t item) { HashSetOrderElement* eset = order->elementTable; - OrderElement oelement ={item, NULL}; + OrderElement oelement(item, NULL); if( !eset->contains(&oelement)){ Set* set = new Set(order->set->type, 1, (uint64_t) order->set->getSize()); Element* elem = new ElementSet(set); - eset->add(allocOrderElement(item, elem)); + eset->add(new OrderElement(item, elem)); This->solver->allElements.push(elem); This->solver->allSets.push(set); return elem; diff --git a/src/ASTTransform/orderdecompose.cc b/src/ASTTransform/orderdecompose.cc index 8b3aa73..1eadffd 100644 --- a/src/ASTTransform/orderdecompose.cc +++ b/src/ASTTransform/orderdecompose.cc @@ -56,7 +56,7 @@ void orderAnalysis(CSolver *This) { decomposeOrder(This, order, graph); deleteOrderGraph(graph); - bool doIntegerEncoding = GETVARTUNABLE(This->tuner, order->order.type, ORDERINTEGERENCODING, &onoff ); + bool doIntegerEncoding = GETVARTUNABLE(This->tuner, order->order.type, ORDERINTEGERENCODING, &offon ); if(!doIntegerEncoding) continue; uint size = order->constraints.getSize(); diff --git a/src/Backend/orderelement.cc b/src/Backend/orderelement.cc index 1355011..01d0ada 100644 --- a/src/Backend/orderelement.cc +++ b/src/Backend/orderelement.cc @@ -1,13 +1,7 @@ #include "orderelement.h" -OrderElement *allocOrderElement(uint64_t item, Element* elem) { - OrderElement *This = (OrderElement *) ourmalloc(sizeof(OrderElement)); - This->elem = elem; - This->item = item; - return This; -} - -void deleteOrderElement(OrderElement *pair) { - ourfree(pair); +OrderElement::OrderElement(uint64_t _item, Element* _elem) { + elem = _elem; + item = _item; } diff --git a/src/Backend/orderelement.h b/src/Backend/orderelement.h index 6bdcbc6..7199405 100644 --- a/src/Backend/orderelement.h +++ b/src/Backend/orderelement.h @@ -12,13 +12,14 @@ #include "mymemory.h" #include "constraint.h" -struct OrderElement { +class OrderElement { + public: + OrderElement(uint64_t item, Element* elem); uint64_t item; Element* elem; + MEMALLOC; }; -OrderElement *allocOrderElement(uint64_t item, Element* elem); -void deleteOrderElement(OrderElement *pair); #endif/* ORDERELEMENT_H */ diff --git a/src/Backend/sattranslator.cc b/src/Backend/sattranslator.cc index 94f6e18..ff1317a 100644 --- a/src/Backend/sattranslator.cc +++ b/src/Backend/sattranslator.cc @@ -13,8 +13,8 @@ uint64_t getElementValueBinaryIndexSATTranslator(CSolver *This, ElementEncoding if (getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] ))) index |= 1; } - model_print("index:%u\tencArraySize:%u\tisInUseElement:%u\n", index, elemEnc->encArraySize, elemEnc->isinUseElement(index)); - ASSERT(elemEnc->encArraySize > index && elemEnc->isinUseElement(index)); + if (elemEnc->encArraySize <= index || !elemEnc->isinUseElement(index)) + model_print("WARNING: Element has undefined value!\n"); return elemEnc->encodingArray[index]; } diff --git a/src/classlist.h b/src/classlist.h index 92cc697..993a147 100644 --- a/src/classlist.h +++ b/src/classlist.h @@ -47,8 +47,7 @@ typedef struct IncrementalSolver IncrementalSolver; -struct OrderElement; -typedef struct OrderElement OrderElement; +class OrderElement; class ElementEncoding; class FunctionEncoding; @@ -60,11 +59,8 @@ typedef struct TableEntry TableEntry; struct OrderGraph; typedef struct OrderGraph OrderGraph; -struct OrderNode; -typedef struct OrderNode OrderNode; - -struct OrderEdge; -typedef struct OrderEdge OrderEdge; +class OrderNode; +class OrderEdge; struct OrderEncoder; typedef struct OrderEncoder OrderEncoder;