From 3e22517a4f2edbc67f6f575ac6379ba8ab0edb70 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Thu, 24 Aug 2017 22:56:17 -0700 Subject: [PATCH] Switch to vector class --- src/AST/boolean.cc | 28 +++++---- src/AST/boolean.h | 3 +- src/AST/element.cc | 4 +- src/AST/element.h | 2 +- src/AST/mutableset.cc | 13 +--- src/AST/mutableset.h | 8 ++- src/AST/order.cc | 4 +- src/AST/order.h | 2 +- src/AST/rewriter.cc | 14 ++--- src/AST/set.cc | 16 +++-- src/AST/set.h | 4 +- src/ASTAnalyses/orderencoder.cc | 95 +++++++++++++----------------- src/ASTAnalyses/orderencoder.h | 10 ++-- src/ASTAnalyses/ordergraph.cc | 8 +-- src/Backend/satfunctableencoder.cc | 1 - src/Backend/satorderencoder.cc | 18 +++--- src/Collections/cppvector.h | 87 +++++++++++++++++++++++++++ src/Collections/structs.cc | 16 +---- src/Collections/structs.h | 16 +---- src/Encoders/naiveencoder.cc | 4 +- src/classlist.h | 2 +- src/csolver.cc | 79 +++++++++++-------------- src/csolver.h | 14 ++--- 23 files changed, 241 insertions(+), 207 deletions(-) create mode 100644 src/Collections/cppvector.h diff --git a/src/AST/boolean.cc b/src/AST/boolean.cc index 08af722..3e05452 100644 --- a/src/AST/boolean.cc +++ b/src/AST/boolean.cc @@ -4,15 +4,25 @@ #include "element.h" #include "order.h" -Boolean::Boolean(ASTNodeType _type) : ASTNode(_type), polarity(P_UNDEFINED), boolVal(BV_UNDEFINED) { - initDefVectorBoolean(GETBOOLEANPARENTS(this)); +Boolean::Boolean(ASTNodeType _type) : + ASTNode(_type), + polarity(P_UNDEFINED), + boolVal(BV_UNDEFINED), + parents() { } -BooleanVar::BooleanVar(VarType t) : Boolean(BOOLEANVAR), vtype(t), var(E_NULL) { +BooleanVar::BooleanVar(VarType t) : + Boolean(BOOLEANVAR), + vtype(t), + var(E_NULL) { } -BooleanOrder::BooleanOrder(Order *_order, uint64_t _first, uint64_t _second) : Boolean(ORDERCONST), order(_order), first(_first), second(_second) { - pushVectorBooleanOrder(&order->constraints, this); +BooleanOrder::BooleanOrder(Order *_order, uint64_t _first, uint64_t _second) : + Boolean(ORDERCONST), + order(_order), + first(_first), + second(_second) { + order->constraints.push(this); } BooleanPredicate::BooleanPredicate(Predicate *_predicate, Element **_inputs, uint _numInputs, Boolean *_undefinedStatus) : @@ -21,7 +31,7 @@ BooleanPredicate::BooleanPredicate(Predicate *_predicate, Element **_inputs, uin inputs(_inputs, _numInputs), undefStatus(_undefinedStatus) { for (uint i = 0; i < _numInputs; i++) { - pushVectorASTNode(GETELEMENTPARENTS(_inputs[i]), this); + GETELEMENTPARENTS(_inputs[i])->push(this); } initPredicateEncoding(&encoding, this); } @@ -30,11 +40,7 @@ BooleanLogic::BooleanLogic(CSolver *solver, LogicOp _op, Boolean **array, uint a Boolean(LOGICOP), op(_op), inputs(array, asize) { - pushVectorBoolean(solver->allBooleans, (Boolean *) this); -} - -Boolean::~Boolean() { - deleteVectorArrayBoolean(GETBOOLEANPARENTS(this)); + solver->allBooleans.push(this); } BooleanPredicate::~BooleanPredicate() { diff --git a/src/AST/boolean.h b/src/AST/boolean.h index 80dc004..d958dc0 100644 --- a/src/AST/boolean.h +++ b/src/AST/boolean.h @@ -22,8 +22,7 @@ class Boolean : public ASTNode { Boolean(ASTNodeType _type); Polarity polarity; BooleanValue boolVal; - VectorBoolean parents; - ~Boolean(); + Vector parents; MEMALLOC; }; diff --git a/src/AST/element.cc b/src/AST/element.cc index b2007c1..fd9e470 100644 --- a/src/AST/element.cc +++ b/src/AST/element.cc @@ -6,7 +6,6 @@ #include "table.h" Element::Element(ASTNodeType _type) : ASTNode(_type) { - initDefVectorASTNode(GETELEMENTPARENTS(this)); initElementEncoding(&encoding, (Element *) this); } @@ -15,7 +14,7 @@ ElementSet::ElementSet(Set *s) : Element(ELEMSET), set(s) { ElementFunction::ElementFunction(Function *_function, Element **array, uint numArrays, Boolean *_overflowstatus) : Element(ELEMFUNCRETURN), function(_function), inputs(array, numArrays), overflowstatus(_overflowstatus) { for (uint i = 0; i < numArrays; i++) - pushVectorASTNode(GETELEMENTPARENTS(array[i]), this); + GETELEMENTPARENTS(array[i])->push(this); initFunctionEncoding(&functionencoding, this); } @@ -58,5 +57,4 @@ ElementConst::~ElementConst() { Element::~Element() { deleteElementEncoding(&encoding); - deleteVectorArrayASTNode(GETELEMENTPARENTS(this)); } diff --git a/src/AST/element.h b/src/AST/element.h index 3385d41..fe5f42b 100644 --- a/src/AST/element.h +++ b/src/AST/element.h @@ -14,7 +14,7 @@ class Element : public ASTNode { public: Element(ASTNodeType type); ~Element(); - VectorASTNode parents; + Vector parents; ElementEncoding encoding; MEMALLOC; }; diff --git a/src/AST/mutableset.cc b/src/AST/mutableset.cc index 19552f6..19f6dec 100644 --- a/src/AST/mutableset.cc +++ b/src/AST/mutableset.cc @@ -1,15 +1,8 @@ #include "mutableset.h" -MutableSet *allocMutableSet(VarType t) { - MutableSet *This = (MutableSet *)ourmalloc(sizeof(MutableSet)); - This->type = t; - This->isRange = false; - This->low = 0; - This->high = 0; - This->members = allocDefVectorInt(); - return This; +MutableSet::MutableSet(VarType t) : Set(t) { } -void addElementMSet(MutableSet *set, uint64_t element) { - pushVectorInt(set->members, element); +void MutableSet::addElementMSet(uint64_t element) { + members->push(element); } diff --git a/src/AST/mutableset.h b/src/AST/mutableset.h index 754d395..b0359d3 100644 --- a/src/AST/mutableset.h +++ b/src/AST/mutableset.h @@ -2,6 +2,10 @@ #define MUTABLESET_H #include "set.h" -MutableSet *allocMutableSet(VarType t); -void addElementMSet(MutableSet *set, uint64_t element); +class MutableSet : public Set { + public: + MutableSet(VarType t); + void addElementMSet(uint64_t element); + MEMALLOC; +}; #endif diff --git a/src/AST/order.cc b/src/AST/order.cc index f797d9b..5443075 100644 --- a/src/AST/order.cc +++ b/src/AST/order.cc @@ -5,7 +5,6 @@ #include "ordergraph.h" Order::Order(OrderType _type, Set *_set) : type(_type), set(_set), orderPairTable(NULL), elementTable(NULL), graph(NULL) { - initDefVectorBooleanOrder(&constraints); initOrderEncoding(&order, this); } @@ -18,7 +17,7 @@ void Order::initializeOrderElementsHashTable() { } void Order::addOrderConstraint(BooleanOrder *constraint) { - pushVectorBooleanOrder(&constraints, constraint); + constraints.push(constraint); } void Order::setOrderEncodingType(OrderEncodingType type) { @@ -26,7 +25,6 @@ void Order::setOrderEncodingType(OrderEncodingType type) { } Order::~Order() { - deleteVectorArrayBooleanOrder(&constraints); deleteOrderEncoding(&order); if (orderPairTable != NULL) { resetAndDeleteHashTableOrderPair(orderPairTable); diff --git a/src/AST/order.h b/src/AST/order.h index 65ff8fc..2cc07b9 100644 --- a/src/AST/order.h +++ b/src/AST/order.h @@ -16,7 +16,7 @@ class Order { HashTableOrderPair *orderPairTable; HashSetOrderElement* elementTable; OrderGraph *graph; - VectorBooleanOrder constraints; + Vector constraints; OrderEncoding order; void initializeOrderHashTable(); void initializeOrderElementsHashTable(); diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc index 386eba0..b96a3b5 100644 --- a/src/AST/rewriter.cc +++ b/src/AST/rewriter.cc @@ -7,9 +7,9 @@ void replaceBooleanWithTrue(CSolver * This, Boolean *bexpr) { removeHashSetBoolean(This->constraints, bexpr); } - uint size = getSizeVectorBoolean(&bexpr->parents); + uint size = bexpr->parents.getSize(); for (uint i = 0; i < size; i++) { - Boolean *parent = getVectorBoolean(&bexpr->parents, i); + Boolean *parent = bexpr->parents.get(i); BooleanLogic *logicop = (BooleanLogic *) parent; switch (logicop->op) { case L_AND: @@ -37,9 +37,9 @@ void replaceBooleanWithBoolean(CSolver * This, Boolean *oldb, Boolean *newb) { addHashSetBoolean(This->constraints, newb); } - uint size = getSizeVectorBoolean(&oldb->parents); + uint size = oldb->parents.getSize(); for (uint i = 0; i < size; i++) { - Boolean *parent = getVectorBoolean(&oldb->parents, i); + Boolean *parent = oldb->parents.get(i); BooleanLogic *logicop = (BooleanLogic *) parent; uint parentsize = logicop->inputs.getSize(); @@ -48,7 +48,7 @@ void replaceBooleanWithBoolean(CSolver * This, Boolean *oldb, Boolean *newb) { Boolean *b = logicop->inputs.get(i); if (b == oldb) { logicop->inputs.set(i, newb); - pushVectorBoolean(&newb->parents, parent); + newb->parents.push(parent); } } } @@ -139,9 +139,9 @@ void replaceBooleanWithFalse(CSolver * This, Boolean *bexpr) { removeHashSetBoolean(This->constraints, bexpr); } - uint size = getSizeVectorBoolean(&bexpr->parents); + uint size = bexpr->parents.getSize(); for (uint i = 0; i < size; i++) { - Boolean *parent = getVectorBoolean(&bexpr->parents, i); + Boolean *parent = bexpr->parents.get(i); BooleanLogic *logicop = (BooleanLogic *) parent; switch (logicop->op) { case L_AND: diff --git a/src/AST/set.cc b/src/AST/set.cc index c9e64ff..4b66dfe 100644 --- a/src/AST/set.cc +++ b/src/AST/set.cc @@ -1,8 +1,12 @@ #include "set.h" #include +Set::Set(VarType t) : type(t), isRange(false), low(0), high(0) { + members = new Vector(); +} + Set::Set(VarType t, uint64_t *elements, uint num) : type(t), isRange(false), low(0), high(0) { - members = allocVectorArrayInt(num, elements); + members = new Vector(num, elements); } Set::Set(VarType t, uint64_t lowrange, uint64_t highrange) : type(t), isRange(true), low(lowrange), high(highrange), members(NULL) { @@ -12,9 +16,9 @@ bool Set::exists(uint64_t element) { if (isRange) { return element >= low && element <= high; } else { - uint size = getSizeVectorInt(members); + uint size = members->getSize(); for (uint i = 0; i < size; i++) { - if (element == getVectorInt(members, i)) + if (element == members->get(i)) return true; } return false; @@ -25,18 +29,18 @@ uint64_t Set::getElement(uint index) { if (isRange) return low + index; else - return getVectorInt(members, index); + return members->get(index); } uint Set::getSize() { if (isRange) { return high - low + 1; } else { - return getSizeVectorInt(members); + return members->getSize(); } } Set::~Set() { if (!isRange) - deleteVectorInt(members); + delete members; } diff --git a/src/AST/set.h b/src/AST/set.h index 172f0a7..9303fa8 100644 --- a/src/AST/set.h +++ b/src/AST/set.h @@ -14,6 +14,7 @@ class Set { public: + Set(VarType t); Set(VarType t, uint64_t *elements, uint num); Set(VarType t, uint64_t lowrange, uint64_t highrange); ~Set(); @@ -25,10 +26,9 @@ class Set { bool isRange; uint64_t low;//also used to count unique items uint64_t high; - VectorInt *members; + Vector *members; MEMALLOC; }; - #endif/* SET_H */ diff --git a/src/ASTAnalyses/orderencoder.cc b/src/ASTAnalyses/orderencoder.cc index 42ac5aa..56cfdae 100644 --- a/src/ASTAnalyses/orderencoder.cc +++ b/src/ASTAnalyses/orderencoder.cc @@ -9,7 +9,7 @@ #include "mutableset.h" #include "tunable.h" -void DFS(OrderGraph *graph, VectorOrderNode *finishNodes) { +void DFS(OrderGraph *graph, Vector *finishNodes) { HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes); while (hasNextOrderNode(iterator)) { OrderNode *node = nextOrderNode(iterator); @@ -17,17 +17,17 @@ void DFS(OrderGraph *graph, VectorOrderNode *finishNodes) { node->status = VISITED; DFSNodeVisit(node, finishNodes, false, false, 0); node->status = FINISHED; - pushVectorOrderNode(finishNodes, node); + finishNodes->push(node); } } deleteIterOrderNode(iterator); } -void DFSReverse(OrderGraph *graph, VectorOrderNode *finishNodes) { - uint size = getSizeVectorOrderNode(finishNodes); +void DFSReverse(OrderGraph *graph, Vector *finishNodes) { + uint size = finishNodes->getSize(); uint sccNum = 1; for (int i = size - 1; i >= 0; i--) { - OrderNode *node = getVectorOrderNode(finishNodes, i); + OrderNode *node = finishNodes->get(i); if (node->status == NOTVISITED) { node->status = VISITED; DFSNodeVisit(node, NULL, true, false, sccNum); @@ -38,7 +38,7 @@ void DFSReverse(OrderGraph *graph, VectorOrderNode *finishNodes) { } } -void DFSNodeVisit(OrderNode *node, VectorOrderNode *finishNodes, bool isReverse, bool mustvisit, uint sccNum) { +void DFSNodeVisit(OrderNode *node, Vector *finishNodes, bool isReverse, bool mustvisit, uint sccNum) { HSIteratorOrderEdge *iterator = isReverse ? iteratorOrderEdge(node->inEdges) : iteratorOrderEdge(node->outEdges); while (hasNextOrderEdge(iterator)) { OrderEdge *edge = nextOrderEdge(iterator); @@ -56,7 +56,7 @@ void DFSNodeVisit(OrderNode *node, VectorOrderNode *finishNodes, bool isReverse, DFSNodeVisit(child, finishNodes, isReverse, mustvisit, sccNum); child->status = FINISHED; if (finishNodes != NULL) - pushVectorOrderNode(finishNodes, child); + finishNodes->push(child); if (isReverse) child->sccNum = sccNum; } @@ -73,13 +73,11 @@ void resetNodeInfoStatusSCC(OrderGraph *graph) { } void computeStronglyConnectedComponentGraph(OrderGraph *graph) { - VectorOrderNode finishNodes; - initDefVectorOrderNode(&finishNodes); + Vector finishNodes; DFS(graph, &finishNodes); resetNodeInfoStatusSCC(graph); DFSReverse(graph, &finishNodes); resetNodeInfoStatusSCC(graph); - deleteVectorArrayOrderNode(&finishNodes); } bool isMustBeTrueNode(OrderNode* node){ @@ -142,19 +140,17 @@ void removeMustBeTrueNodes(CSolver *This, OrderGraph *graph) { to determine whether we need to generate pseudoPos edges. */ void completePartialOrderGraph(OrderGraph *graph) { - VectorOrderNode finishNodes; - initDefVectorOrderNode(&finishNodes); + Vector finishNodes; DFS(graph, &finishNodes); resetNodeInfoStatusSCC(graph); HashTableNodeToNodeSet *table = allocHashTableNodeToNodeSet(128, 0.25); - VectorOrderNode sccNodes; - initDefVectorOrderNode(&sccNodes); + Vector sccNodes; - uint size = getSizeVectorOrderNode(&finishNodes); + uint size = finishNodes.getSize(); uint sccNum = 1; for (int i = size - 1; i >= 0; i--) { - OrderNode *node = getVectorOrderNode(&finishNodes, i); + OrderNode *node = finishNodes.get(i); HashSetOrderNode *sources = allocHashSetOrderNode(4, 0.25); putNodeToNodeSet(table, node, sources); @@ -165,12 +161,12 @@ void completePartialOrderGraph(OrderGraph *graph) { node->status = FINISHED; node->sccNum = sccNum; sccNum++; - pushVectorOrderNode(&sccNodes, node); + sccNodes.push(node); //Compute in set for entire SCC - uint rSize = getSizeVectorOrderNode(&sccNodes); + uint rSize = sccNodes.getSize(); for (uint j = 0; j < rSize; j++) { - OrderNode *rnode = getVectorOrderNode(&sccNodes, j); + OrderNode *rnode = sccNodes.get(j); //Compute source sets HSIteratorOrderEdge *iterator = iteratorOrderEdge(rnode->inEdges); while (hasNextOrderEdge(iterator)) { @@ -186,7 +182,7 @@ void completePartialOrderGraph(OrderGraph *graph) { } for (uint j=0; j < rSize; j++) { //Copy in set of entire SCC - OrderNode *rnode = getVectorOrderNode(&sccNodes, j); + OrderNode *rnode = sccNodes.get(j); HashSetOrderNode * set = (j==0) ? sources : copyHashSetOrderNode(sources); putNodeToNodeSet(table, rnode, set); @@ -205,18 +201,16 @@ void completePartialOrderGraph(OrderGraph *graph) { deleteIterOrderEdge(iterator); } - clearVectorOrderNode(&sccNodes); + sccNodes.clear(); } } resetAndDeleteHashTableNodeToNodeSet(table); deleteHashTableNodeToNodeSet(table); resetNodeInfoStatusSCC(graph); - deleteVectorArrayOrderNode(&sccNodes); - deleteVectorArrayOrderNode(&finishNodes); } -void DFSMust(OrderGraph *graph, VectorOrderNode *finishNodes) { +void DFSMust(OrderGraph *graph, Vector *finishNodes) { HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes); while (hasNextOrderNode(iterator)) { OrderNode *node = nextOrderNode(iterator); @@ -224,18 +218,18 @@ void DFSMust(OrderGraph *graph, VectorOrderNode *finishNodes) { node->status = VISITED; DFSNodeVisit(node, finishNodes, false, true, 0); node->status = FINISHED; - pushVectorOrderNode(finishNodes, node); + finishNodes->push(node); } } deleteIterOrderNode(iterator); } -void DFSClearContradictions(CSolver *solver, OrderGraph *graph, VectorOrderNode *finishNodes, bool computeTransitiveClosure) { - uint size = getSizeVectorOrderNode(finishNodes); +void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector *finishNodes, bool computeTransitiveClosure) { + uint size = finishNodes->getSize(); HashTableNodeToNodeSet *table = allocHashTableNodeToNodeSet(128, 0.25); for (int i = size - 1; i >= 0; i--) { - OrderNode *node = getVectorOrderNode(finishNodes, i); + OrderNode *node = finishNodes->get(i); HashSetOrderNode *sources = allocHashSetOrderNode(4, 0.25); putNodeToNodeSet(table, node, sources); @@ -310,15 +304,13 @@ void DFSClearContradictions(CSolver *solver, OrderGraph *graph, VectorOrderNode edges. */ void reachMustAnalysis(CSolver * solver, OrderGraph *graph, bool computeTransitiveClosure) { - VectorOrderNode finishNodes; - initDefVectorOrderNode(&finishNodes); + Vector finishNodes; //Topologically sort the mustPos edge graph DFSMust(graph, &finishNodes); resetNodeInfoStatusSCC(graph); //Find any backwards edges that complete cycles and force them to be mustNeg DFSClearContradictions(solver, graph, &finishNodes, computeTransitiveClosure); - deleteVectorArrayOrderNode(&finishNodes); } /* This function finds edges that must be positive and forces the @@ -378,13 +370,11 @@ void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph) { } void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) { - VectorOrder ordervec; - VectorOrder partialcandidatevec; - initDefVectorOrder(&ordervec); - initDefVectorOrder(&partialcandidatevec); - uint size = getSizeVectorBooleanOrder(&order->constraints); + Vector ordervec; + Vector partialcandidatevec; + uint size = order->constraints.getSize(); for (uint i = 0; i < size; i++) { - BooleanOrder *orderconstraint = getVectorBooleanOrder(&order->constraints, i); + BooleanOrder *orderconstraint = order->constraints.get(i); OrderNode *from = getOrderNodeFromOrderGraph(graph, orderconstraint->first); OrderNode *to = getOrderNodeFromOrderGraph(graph, orderconstraint->second); model_print("from->sccNum:%u\tto->sccNum:%u\n", from->sccNum, to->sccNum); @@ -401,53 +391,50 @@ void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) { } else { //Build new order and change constraint's order Order *neworder = NULL; - if (getSizeVectorOrder(&ordervec) > from->sccNum) - neworder = getVectorOrder(&ordervec, from->sccNum); + if (ordervec.getSize() > from->sccNum) + neworder = ordervec.get(from->sccNum); if (neworder == NULL) { - Set *set = (Set *) allocMutableSet(order->set->type); + MutableSet *set = new MutableSet(order->set->type); neworder = new Order(order->type, set); - pushVectorOrder(This->allOrders, neworder); - setExpandVectorOrder(&ordervec, from->sccNum, neworder); + This->allOrders.push(neworder); + ordervec.setExpand(from->sccNum, neworder); if (order->type == PARTIAL) - setExpandVectorOrder(&partialcandidatevec, from->sccNum, neworder); + partialcandidatevec.setExpand(from->sccNum, neworder); else - setExpandVectorOrder(&partialcandidatevec, from->sccNum, NULL); + partialcandidatevec.setExpand(from->sccNum, NULL); } if (from->status != ADDEDTOSET) { from->status = ADDEDTOSET; - addElementMSet((MutableSet *)neworder->set, from->id); + ((MutableSet *)neworder->set)->addElementMSet(from->id); } if (to->status != ADDEDTOSET) { to->status = ADDEDTOSET; - addElementMSet((MutableSet *)neworder->set, to->id); + ((MutableSet *)neworder->set)->addElementMSet(to->id); } if (order->type == PARTIAL) { OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to); if (edge->polNeg) - setExpandVectorOrder(&partialcandidatevec, from->sccNum, NULL); + partialcandidatevec.setExpand(from->sccNum, NULL); } orderconstraint->order = neworder; neworder->addOrderConstraint(orderconstraint); } } - uint pcvsize=getSizeVectorOrder(&partialcandidatevec); + uint pcvsize=partialcandidatevec.getSize(); for(uint i=0;itype = TOTAL; model_print("i=%u\t", i); } } - - deleteVectorArrayOrder(&ordervec); - deleteVectorArrayOrder(&partialcandidatevec); } void orderAnalysis(CSolver *This) { - uint size = getSizeVectorOrder(This->allOrders); + uint size = This->allOrders.getSize(); for (uint i = 0; i < size; i++) { - Order *order = getVectorOrder(This->allOrders, i); + Order *order = This->allOrders.get(i); bool doDecompose=GETVARTUNABLE(This->tuner, order->type, DECOMPOSEORDER, &onoff); if (!doDecompose) continue; diff --git a/src/ASTAnalyses/orderencoder.h b/src/ASTAnalyses/orderencoder.h index f9b4d5f..ad050bb 100644 --- a/src/ASTAnalyses/orderencoder.h +++ b/src/ASTAnalyses/orderencoder.h @@ -14,17 +14,17 @@ void computeStronglyConnectedComponentGraph(OrderGraph *graph); void orderAnalysis(CSolver *solver); void initializeNodeInfoSCC(OrderGraph *graph); -void DFSNodeVisit(OrderNode *node, VectorOrderNode *finishNodes, bool isReverse, bool mustvisit, uint sccNum); -void DFS(OrderGraph *graph, VectorOrderNode *finishNodes); -void DFSReverse(OrderGraph *graph, VectorOrderNode *finishNodes); +void DFSNodeVisit(OrderNode *node, Vector *finishNodes, bool isReverse, bool mustvisit, uint sccNum); +void DFS(OrderGraph *graph, Vector *finishNodes); +void DFSReverse(OrderGraph *graph, Vector *finishNodes); void completePartialOrderGraph(OrderGraph *graph); void resetNodeInfoStatusSCC(OrderGraph *graph); bool isMustBeTrueNode(OrderNode* node); void bypassMustBeTrueNode(CSolver *This, OrderGraph* graph, OrderNode* node); void removeMustBeTrueNodes(CSolver *This, OrderGraph *graph); void completePartialOrderGraph(OrderGraph *graph); -void DFSMust(OrderGraph *graph, VectorOrderNode *finishNodes); -void DFSClearContradictions(CSolver *solver, OrderGraph *graph, VectorOrderNode *finishNodes, bool computeTransitiveClosure); +void DFSMust(OrderGraph *graph, Vector *finishNodes); +void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector *finishNodes, bool computeTransitiveClosure); void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure); void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph); void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph); diff --git a/src/ASTAnalyses/ordergraph.cc b/src/ASTAnalyses/ordergraph.cc index 0871a41..a9d974d 100644 --- a/src/ASTAnalyses/ordergraph.cc +++ b/src/ASTAnalyses/ordergraph.cc @@ -15,9 +15,9 @@ OrderGraph *allocOrderGraph(Order *order) { OrderGraph *buildOrderGraph(Order *order) { OrderGraph *orderGraph = allocOrderGraph(order); - uint constrSize = getSizeVectorBooleanOrder(&order->constraints); + uint constrSize = order->constraints.getSize(); for (uint j = 0; j < constrSize; j++) { - addOrderConstraintToOrderGraph(orderGraph, getVectorBooleanOrder(&order->constraints, j)); + addOrderConstraintToOrderGraph(orderGraph, order->constraints.get(j)); } return orderGraph; } @@ -25,9 +25,9 @@ OrderGraph *buildOrderGraph(Order *order) { //Builds only the subgraph for the must order graph. OrderGraph *buildMustOrderGraph(Order *order) { OrderGraph *orderGraph = allocOrderGraph(order); - uint constrSize = getSizeVectorBooleanOrder(&order->constraints); + uint constrSize = order->constraints.getSize(); for (uint j = 0; j < constrSize; j++) { - addMustOrderConstraintToOrderGraph(orderGraph, getVectorBooleanOrder(&order->constraints, j)); + addMustOrderConstraintToOrderGraph(orderGraph, order->constraints.get(j)); } return orderGraph; } diff --git a/src/Backend/satfunctableencoder.cc b/src/Backend/satfunctableencoder.cc index f8ceebe..035968f 100644 --- a/src/Backend/satfunctableencoder.cc +++ b/src/Backend/satfunctableencoder.cc @@ -319,5 +319,4 @@ void encodeEnumTableElemFunctionSATEncoder(SATEncoder *This, ElementFunction *el Edge cor = constraintAND(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses)); addConstraintCNF(This->cnf, cor); deleteVectorEdge(clauses); - } diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc index a22f31a..ecd811f 100644 --- a/src/Backend/satorderencoder.cc +++ b/src/Backend/satorderencoder.cc @@ -64,10 +64,10 @@ Edge orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder){ BooleanPredicate * boolean=new BooleanPredicate(predicate, parray, 2, NULL); setFunctionEncodingType(boolean->getFunctionEncoding(), CIRCUIT); {//Adding new elements and boolean/predicate to solver regarding memory management - pushVectorBoolean(This->solver->allBooleans, boolean); - pushVectorPredicate(This->solver->allPredicates, predicate); - pushVectorElement(This->solver->allElements, elem1); - pushVectorElement(This->solver->allElements, elem2); + This->solver->allBooleans.push(boolean); + This->solver->allPredicates.push(predicate); + This->solver->allElements.push(elem1); + This->solver->allElements.push(elem2); } return encodeConstraintSATEncoder(This, boolean); } @@ -158,16 +158,16 @@ void createAllTotalOrderConstraintsSATEncoder(SATEncoder *This, Order *order) { model_print("in total order ...\n"); #endif ASSERT(order->type == TOTAL); - VectorInt *mems = order->set->members; - uint size = getSizeVectorInt(mems); + Vector *mems = order->set->members; + uint size = mems->getSize(); for (uint i = 0; i < size; i++) { - uint64_t valueI = getVectorInt(mems, i); + uint64_t valueI = mems->get(i); for (uint j = i + 1; j < size; j++) { - uint64_t valueJ = getVectorInt(mems, j); + uint64_t valueJ = mems->get(j); OrderPair pairIJ = {valueI, valueJ}; Edge constIJ = getPairConstraint(This, order, &pairIJ); for (uint k = j + 1; k < size; k++) { - uint64_t valueK = getVectorInt(mems, k); + uint64_t valueK = mems->get(k); OrderPair pairJK = {valueJ, valueK}; OrderPair pairIK = {valueI, valueK}; Edge constIK = getPairConstraint(This, order, &pairIK); diff --git a/src/Collections/cppvector.h b/src/Collections/cppvector.h new file mode 100644 index 0000000..a10403e --- /dev/null +++ b/src/Collections/cppvector.h @@ -0,0 +1,87 @@ +#ifndef CPPVECTOR_H +#define CPPVECTOR_H +#include + +#define VECTOR_DEFCAP 8 + +template +class Vector { + public: + Vector(uint _capacity = VECTOR_DEFCAP) : + size(0), + capacity(_capacity), + array((type *) ourmalloc(sizeof(type) * _capacity)) { + } + + Vector(uint _capacity, type * _array) : + size(_capacity), + capacity(_capacity), + array((type *) ourmalloc(sizeof(type) * _capacity)) { + memcpy(array, _array, capacity * sizeof(type)); + } + + void pop() { + size--; + } + + type last() { + return array[size - 1]; + } + + void setSize(uint _size) { + if (_size <= size) { + size = _size; + return; + } else if (_size > capacity) { + array = (type *)ourrealloc(array, _size * sizeof(type)); + capacity = _size; + } + bzero(&array[size], (_size - size) * sizeof(type)); + size = _size; + } + + void push(type item) { + if (size >= capacity) { + uint newcap = capacity << 1; + array = (type *)ourrealloc(array, newcap * sizeof(type)); + capacity = newcap; + } + array[size++] = item; + } + + type get(uint index) { + return array[index]; + } + + void setExpand(uint index, type item) { + if (index >= size) + setSize(index + 1); + set(index, item); + } + + void set(uint index, type item) { + array[index] = item; + } + + uint getSize() { + return size; + } + + ~Vector() { + ourfree(array); + } + + void clear() { + size = 0; + } + + type *expose() { + return array; + } + + private: + uint size; + uint capacity; + type *array; +}; +#endif diff --git a/src/Collections/structs.cc b/src/Collections/structs.cc index d6cdd16..10b2f83 100644 --- a/src/Collections/structs.cc +++ b/src/Collections/structs.cc @@ -1,5 +1,5 @@ -#include "structs.h" #include "mymemory.h" +#include "structs.h" #include "orderpair.h" #include "tableentry.h" #include "ordernode.h" @@ -7,20 +7,6 @@ #include "ordergraph.h" #include "orderelement.h" -VectorImpl(Table, Table *, 4); -VectorImpl(Set, Set *, 4); -VectorImpl(Boolean, Boolean *, 4); -VectorImpl(BooleanOrder, BooleanOrder *, 4); -VectorImpl(Function, Function *, 4); -VectorImpl(Predicate, Predicate *, 4); -VectorImpl(Element, Element *, 4); -VectorImpl(Order, Order *, 4); -VectorImpl(TableEntry, TableEntry *, 4); -VectorImpl(ASTNode, ASTNode *, 4); -VectorImpl(Int, uint64_t, 4); -VectorImpl(OrderNode, OrderNode *, 4); -VectorImpl(OrderGraph, OrderGraph *, 4); - static inline unsigned int Ptr_hash_function(void *hash) { return (unsigned int)((int64)hash >> 4); } diff --git a/src/Collections/structs.h b/src/Collections/structs.h index 83b47b0..b153f3a 100644 --- a/src/Collections/structs.h +++ b/src/Collections/structs.h @@ -1,25 +1,11 @@ #ifndef STRUCTS_H #define STRUCTS_H -#include "vector.h" +#include "cppvector.h" #include "hashtable.h" #include "hashset.h" #include "classlist.h" #include "array.h" -VectorDef(Table, Table *); -VectorDef(Set, Set *); -VectorDef(Boolean, Boolean *); -VectorDef(BooleanOrder, BooleanOrder *); -VectorDef(Function, Function *); -VectorDef(Predicate, Predicate *); -VectorDef(Element, Element *); -VectorDef(Order, Order *); -VectorDef(TableEntry, TableEntry *); -VectorDef(ASTNode, ASTNode *); -VectorDef(Int, uint64_t); -VectorDef(OrderNode, OrderNode *); -VectorDef(OrderGraph, OrderGraph *); - HashTableDef(Void, void *, void *); HashTableDef(OrderPair, OrderPair *, OrderPair *); diff --git a/src/Encoders/naiveencoder.cc b/src/Encoders/naiveencoder.cc index 9596628..5ae9d85 100644 --- a/src/Encoders/naiveencoder.cc +++ b/src/Encoders/naiveencoder.cc @@ -97,12 +97,12 @@ void encodingArrayInitialization(ElementEncoding *This) { Element *element = This->element; Set *set = getElementSet(element); ASSERT(set->isRange == false); - uint size = getSizeVectorInt(set->members); + uint size = set->members->getSize(); uint encSize = getSizeEncodingArray(This, size); allocEncodingArrayElement(This, encSize); allocInUseArrayElement(This, encSize); for (uint i = 0; i < size; i++) { - This->encodingArray[i] = getVectorInt(set->members, i); + This->encodingArray[i] = set->members->get(i); setInUseElement(This, i); } } diff --git a/src/classlist.h b/src/classlist.h index 38aee74..32230d0 100644 --- a/src/classlist.h +++ b/src/classlist.h @@ -27,7 +27,7 @@ class BooleanLogic; class BooleanPredicate; class ASTNode; class Set; -typedef class Set MutableSet; +class MutableSet; class ElementFunction; class ElementSet; diff --git a/src/csolver.cc b/src/csolver.cc index b6adc3f..e8ea646 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -15,13 +15,6 @@ CSolver::CSolver() : unsat(false) { constraints = allocDefHashSetBoolean(); - allBooleans = allocDefVectorBoolean(); - allSets = allocDefVectorSet(); - allElements = allocDefVectorElement(); - allPredicates = allocDefVectorPredicate(); - allTables = allocDefVectorTable(); - allOrders = allocDefVectorOrder(); - allFunctions = allocDefVectorFunction(); tuner = allocTuner(); satEncoder = allocSATEncoder(this); } @@ -31,118 +24,112 @@ CSolver::CSolver() : unsat(false) { CSolver::~CSolver() { deleteHashSetBoolean(constraints); - uint size = getSizeVectorBoolean(allBooleans); + uint size = allBooleans.getSize(); for (uint i = 0; i < size; i++) { - delete getVectorBoolean(allBooleans, i); + delete allBooleans.get(i); } - deleteVectorBoolean(allBooleans); - size = getSizeVectorSet(allSets); + size = allSets.getSize(); for (uint i = 0; i < size; i++) { - delete getVectorSet(allSets, i); + delete allSets.get(i); } - deleteVectorSet(allSets); - size = getSizeVectorElement(allElements); + size = allElements.getSize(); for (uint i = 0; i < size; i++) { - delete getVectorElement(allElements, i); + delete allElements.get(i); } - deleteVectorElement(allElements); - size = getSizeVectorTable(allTables); + size = allTables.getSize(); for (uint i = 0; i < size; i++) { - delete getVectorTable(allTables, i); + delete allTables.get(i); } - deleteVectorTable(allTables); - size = getSizeVectorPredicate(allPredicates); + size = allPredicates.getSize(); for (uint i = 0; i < size; i++) { - delete getVectorPredicate(allPredicates, i); + delete allPredicates.get(i); } - deleteVectorPredicate(allPredicates); - size = getSizeVectorOrder(allOrders); + size = allOrders.getSize(); for (uint i = 0; i < size; i++) { - delete getVectorOrder(allOrders, i); + delete allOrders.get(i); } - deleteVectorOrder(allOrders); - size = getSizeVectorFunction(allFunctions); + size = allFunctions.getSize(); for (uint i = 0; i < size; i++) { - delete getVectorFunction(allFunctions, i); + delete allFunctions.get(i); } - deleteVectorFunction(allFunctions); + deleteSATEncoder(satEncoder); deleteTuner(tuner); } Set *CSolver::createSet(VarType type, uint64_t *elements, uint numelements) { Set *set = new Set(type, elements, numelements); - pushVectorSet(allSets, set); + allSets.push(set); return set; } Set *CSolver::createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange) { Set *set = new Set(type, lowrange, highrange); - pushVectorSet(allSets, set); + allSets.push(set); return set; } MutableSet *CSolver::createMutableSet(VarType type) { - MutableSet *set = allocMutableSet(type); - pushVectorSet(allSets, set); + MutableSet *set = new MutableSet(type); + allSets.push(set); return set; } void CSolver::addItem(MutableSet *set, uint64_t element) { - addElementMSet(set, element); + set->addElementMSet(element); } uint64_t CSolver::createUniqueItem(MutableSet *set) { uint64_t element = set->low++; - addElementMSet(set, element); + set->addElementMSet(element); return element; } Element *CSolver::getElementVar(Set *set) { Element *element = new ElementSet(set); - pushVectorElement(allElements, element); + allElements.push(element); return element; } Element *CSolver::getElementConst(VarType type, uint64_t value) { Element *element = new ElementConst(value, type); - pushVectorElement(allElements, element); + allElements.push(element); return element; } Boolean *CSolver::getBooleanVar(VarType type) { Boolean *boolean = new BooleanVar(type); - pushVectorBoolean(allBooleans, boolean); + allBooleans.push(boolean); return boolean; } Function *CSolver::createFunctionOperator(ArithOp op, Set **domain, uint numDomain, Set *range,OverFlowBehavior overflowbehavior) { Function *function = new FunctionOperator(op, domain, numDomain, range, overflowbehavior); - pushVectorFunction(allFunctions, function); + allFunctions.push(function); return function; } Predicate *CSolver::createPredicateOperator(CompOp op, Set **domain, uint numDomain) { Predicate *predicate = new PredicateOperator(op, domain,numDomain); - pushVectorPredicate(allPredicates, predicate); + allPredicates.push(predicate); return predicate; } Predicate *CSolver::createPredicateTable(Table *table, UndefinedBehavior behavior) { Predicate *predicate = new PredicateTable(table, behavior); - pushVectorPredicate(allPredicates, predicate); + allPredicates.push(predicate); return predicate; } Table *CSolver::createTable(Set **domains, uint numDomain, Set *range) { Table *table = new Table(domains,numDomain,range); - pushVectorTable(allTables, table); + allTables.push(table); return table; } @@ -156,13 +143,13 @@ void CSolver::addTableEntry(Table *table, uint64_t *inputs, uint inputSize, uint Function *CSolver::completeTable(Table *table, UndefinedBehavior behavior) { Function *function = new FunctionTable(table, behavior); - pushVectorFunction(allFunctions,function); + allFunctions.push(function); return function; } Element *CSolver::applyFunction(Function *function, Element **array, uint numArrays, Boolean *overflowstatus) { Element *element = new ElementFunction(function,array,numArrays,overflowstatus); - pushVectorElement(allElements, element); + allElements.push(element); return element; } @@ -172,7 +159,7 @@ Boolean *CSolver::applyPredicate(Predicate *predicate, Element **inputs, uint nu Boolean *CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, uint numInputs, Boolean *undefinedStatus) { Boolean *boolean = new BooleanPredicate(predicate, inputs, numInputs, undefinedStatus); - pushVectorBoolean(allBooleans, boolean); + allBooleans.push(boolean); return boolean; } @@ -186,13 +173,13 @@ void CSolver::addConstraint(Boolean *constraint) { Order *CSolver::createOrder(OrderType type, Set *set) { Order *order = new Order(type, set); - pushVectorOrder(allOrders, order); + allOrders.push(order); return order; } Boolean *CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second) { Boolean *constraint = new BooleanOrder(order, first, second); - pushVectorBoolean(allBooleans,constraint); + allBooleans.push(constraint); return constraint; } diff --git a/src/csolver.h b/src/csolver.h index e8527f0..b2741fd 100644 --- a/src/csolver.h +++ b/src/csolver.h @@ -17,25 +17,25 @@ class CSolver { HashSetBoolean *constraints; /** This is a vector of all boolean structs that we have allocated. */ - VectorBoolean *allBooleans; + Vector allBooleans; /** This is a vector of all set structs that we have allocated. */ - VectorSet *allSets; + Vector allSets; /** This is a vector of all element structs that we have allocated. */ - VectorElement *allElements; + Vector allElements; /** This is a vector of all predicate structs that we have allocated. */ - VectorPredicate *allPredicates; + Vector allPredicates; /** This is a vector of all table structs that we have allocated. */ - VectorTable *allTables; + Vector allTables; /** This is a vector of all order structs that we have allocated. */ - VectorOrder *allOrders; + Vector allOrders; /** This is a vector of all function structs that we have allocated. */ - VectorFunction *allFunctions; + Vector allFunctions; /** This function creates a set containing the elements passed in the array. */ -- 2.34.1