More conversion to classes

diff --git a/src/ASTAnalyses/orderedge.cc b/src/ASTAnalyses/orderedge.cc
index c4632dafcc376abc1a78f379ce0f65c22935867b..c0cd678f7130807ec7c56959b0c89f91c39a29e2 100644 (file)
--- 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 21fa9034fb8d061e5f6f3bf8fd77dabe6c2b91ec..bbe62004dfc3314cb29d7cc7f621070f17a7619e 100644 (file)
--- 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 05e2ae00f22765690b92726b13f3513cf5de0102..8eb56adf664559a58d33cb23f3b3a2fd690f2cbf 100644 (file)
--- a/src/ASTAnalyses/orderencoder.cc
+++ b/src/ASTAnalyses/orderencoder.cc
@@ -39,7 +39,7 @@ void DFSReverse(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
 }
 
 void DFSNodeVisit(OrderNode *node, Vector<OrderNode *> *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, Vector<OrderNode
 
                {
                        //Compute source sets
-                       HSIteratorOrderEdge *iterator = node->inEdges->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, Vector<OrderNode
                                newedge->polPos = 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, Vector<OrderNode
                }
                {
                        //Use source sets to compute mustNeg for edges that would introduce cycle if true
-                       HSIteratorOrderEdge *iterator = node->outEdges->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 ee970e1d551c1f3281e541a092c318f57f33cc79..d81218e7e514e37c7fb2f40eafeece31f2c61cf9 100644 (file)
--- 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 c197a57e71510b56e1ca5c83f7307af0f60e79ce..02f314694d31039468b7e31e60f3f10d33cb3c88 100644 (file)
--- 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 4ac6083d31596854db7f3a07aa0139a7adcfeead..95862aea200b799a092ccda7eda4a614c634ca9a 100644 (file)
--- 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 bada3f0593d94f1d95fd6db8eeff68913236b4d0..343c93a7c02adbfeb2a846750a7f0255150afd4d 100644 (file)
--- 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 8b3aa73fef662ad5b5ad5862472e16a97285540b..1eadffd71058cd925ebff6f1fd84c075c94de17f 100644 (file)
--- 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 135501120e20f129dc57f679bce2a6400ca71905..01d0adaa9f76259142d87dc387cd1e5a361b4185 100644 (file)
--- 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 6bdcbc6482a7e2c164ed8bfe4b608cd7f8f7824f..7199405469a3961ea0402abad58ef52116a219af 100644 (file)
--- 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 94f6e18cf15d1beab675ed38b0b3407b67d9e281..ff1317a2a992c897808bcf687b0fe92bfc6e4ca5 100644 (file)
--- 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 92cc697f4f14c007e1c198337e06c578866f10f4..993a14733bfb0590d3bdd055c7e2295e65c57351 100644 (file)
--- 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;