Switch to vector class
authorbdemsky <bdemsky@uci.edu>
Fri, 25 Aug 2017 05:56:17 +0000 (22:56 -0700)
committerbdemsky <bdemsky@uci.edu>
Fri, 25 Aug 2017 05:56:17 +0000 (22:56 -0700)
23 files changed:
src/AST/boolean.cc
src/AST/boolean.h
src/AST/element.cc
src/AST/element.h
src/AST/mutableset.cc
src/AST/mutableset.h
src/AST/order.cc
src/AST/order.h
src/AST/rewriter.cc
src/AST/set.cc
src/AST/set.h
src/ASTAnalyses/orderencoder.cc
src/ASTAnalyses/orderencoder.h
src/ASTAnalyses/ordergraph.cc
src/Backend/satfunctableencoder.cc
src/Backend/satorderencoder.cc
src/Collections/cppvector.h [new file with mode: 0644]
src/Collections/structs.cc
src/Collections/structs.h
src/Encoders/naiveencoder.cc
src/classlist.h
src/csolver.cc
src/csolver.h

index 08af722b1c2e406f1559450b6aca3f7b5cedaaec..3e05452019f17d6a576e68a610889ed2b81f4187 100644 (file)
@@ -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() {
index 80dc004c7583d3b5640568619a6aa56f11148eb3..d958dc02af701afdeb4f47ac578818512e592db8 100644 (file)
@@ -22,8 +22,7 @@ class Boolean : public ASTNode {
        Boolean(ASTNodeType _type);
        Polarity polarity;
        BooleanValue boolVal;
-       VectorBoolean parents;
-       ~Boolean();
+       Vector<Boolean *> parents;
        MEMALLOC;
 };
 
index b2007c124c17d4ab87ef23e5f954836adee78023..fd9e470b696be28a953bcfdc57bd9cc673d19f2e 100644 (file)
@@ -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));
 }
index 3385d41bdd24f0e9225f0ef9f4680912965ae710..fe5f42b0b3b83c76bb99293743301f7b6916b687 100644 (file)
@@ -14,7 +14,7 @@ class Element : public ASTNode {
  public:
        Element(ASTNodeType type);
        ~Element();
-       VectorASTNode parents;
+       Vector<ASTNode *> parents;
        ElementEncoding encoding;
        MEMALLOC;
 };
index 19552f6cfa01359010cb1fbf77bd6c3ba75258b8..19f6dec8b3878a02126245be10f5a246ad4ec55b 100644 (file)
@@ -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);
 }
index 754d39586dbca1db842f1cbf3030ce8830867cec..b0359d3d5165d9e1241f6e7affa35bd749f311d1 100644 (file)
@@ -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
index f797d9b029d7e176c9503cb26119987bff415385..544307553a4bb3246927d7c9ed9e8ab8db7be2bb 100644 (file)
@@ -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);
index 65ff8fc180829b76543df89765cefb9c0e0a154d..2cc07b99cdcdd7db393c03c77910dc75ef594de7 100644 (file)
@@ -16,7 +16,7 @@ class Order {
        HashTableOrderPair *orderPairTable;
        HashSetOrderElement* elementTable;
        OrderGraph *graph;
-       VectorBooleanOrder constraints;
+       Vector<BooleanOrder *> constraints;
        OrderEncoding order;
        void initializeOrderHashTable();
        void initializeOrderElementsHashTable();
index 386eba038e995d4fc25f4122ad50affcc602ef6a..b96a3b5041e694e6ab60a00df46dfb41085168f9 100644 (file)
@@ -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:
index c9e64ffb035a60b8cf6c6f8777b1400efad8ba92..4b66dfe956d499d5a6a653ed25ab767c40fe1eae 100644 (file)
@@ -1,8 +1,12 @@
 #include "set.h"
 #include <stddef.h>
 
+Set::Set(VarType t) : type(t), isRange(false), low(0), high(0) {
+       members = new Vector<uint64_t>();
+}
+
 Set::Set(VarType t, uint64_t *elements, uint num) : type(t), isRange(false), low(0), high(0) {
-       members = allocVectorArrayInt(num, elements);
+       members = new Vector<uint64_t>(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;
 }
index 172f0a7abfb8bb28aa37111e0e1948d20667fc30..9303fa843cc059d6bb6348641b7b50b1bde8e431 100644 (file)
@@ -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<uint64_t> *members;
        MEMALLOC;
 };
 
-
 #endif/* SET_H */
 
index 42ac5aa07b027cff094e3b60a2b9cdd062af6aeb..56cfdaef7e672e26783d48be04a574a64601a150 100644 (file)
@@ -9,7 +9,7 @@
 #include "mutableset.h"
 #include "tunable.h"
 
-void DFS(OrderGraph *graph, VectorOrderNode *finishNodes) {
+void DFS(OrderGraph *graph, Vector<OrderNode *> *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<OrderNode *> *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<OrderNode *> *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<OrderNode *> 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<OrderNode *> finishNodes;
        DFS(graph, &finishNodes);
        resetNodeInfoStatusSCC(graph);
        HashTableNodeToNodeSet *table = allocHashTableNodeToNodeSet(128, 0.25);
 
-       VectorOrderNode sccNodes;
-       initDefVectorOrderNode(&sccNodes);
+       Vector<OrderNode *> 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<OrderNode *> *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<OrderNode *> *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<OrderNode *> 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<Order *> ordervec;
+       Vector<Order *> 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;i<pcvsize;i++) {
-               Order * neworder=getVectorOrder(&partialcandidatevec, i);
+               Order * neworder=partialcandidatevec.get(i);
                if (neworder != NULL){
                        neworder->type = 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;
index f9b4d5f2edb0fe2fdefcf35ee8b92be437a0edc6..ad050bb7ac33e380c1ae2a6fcd957c65e58eb553 100644 (file)
 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<OrderNode *> *finishNodes, bool isReverse, bool mustvisit, uint sccNum);
+void DFS(OrderGraph *graph, Vector<OrderNode *> *finishNodes);
+void DFSReverse(OrderGraph *graph, Vector<OrderNode *> *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<OrderNode *> *finishNodes);
+void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode *> *finishNodes, bool computeTransitiveClosure);
 void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure);
 void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph);
 void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph);
index 0871a414d450f5a2906dd86d80f3f9f586e1a491..a9d974d48ddee38baf0b927c6ddc5d9837567459 100644 (file)
@@ -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;
 }
index f8ceebe28a78bd49b3e01ff7d5b52c1e1969738e..035968f62f99e410c5d8b6cfb723ee3e546040f8 100644 (file)
@@ -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);
-
 }
index a22f31add710430d00ad8c6325ba8c578bca154e..ecd811fe2d349a2bad08a716e54dc80c034d264b 100644 (file)
@@ -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<uint64_t> *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 (file)
index 0000000..a10403e
--- /dev/null
@@ -0,0 +1,87 @@
+#ifndef CPPVECTOR_H
+#define CPPVECTOR_H
+#include <string.h>
+
+#define VECTOR_DEFCAP 8
+
+template<typename type>
+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
index d6cdd164ab1e6a42eb3db386c79c130bff2f6ef0..10b2f83c4874f39e8d9639ebd0d30cf968a09f09 100644 (file)
@@ -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);
 }
index 83b47b0168115f0d8e2c5562bdbd16bd53b3938f..b153f3aafc3ac196335be2feb6523d37a98c1459 100644 (file)
@@ -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 *);
 
index 959662823fe58c0f11299222e2936100de7bb8e7..5ae9d859e21e2981915b593965e5e17173a97e54 100644 (file)
@@ -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);
        }
 }
index 38aee744173f28a58c418eb737278b3dcf3fc01e..32230d0b3e69399a17ff1ee706aacc0c769bb145 100644 (file)
@@ -27,7 +27,7 @@ class BooleanLogic;
 class BooleanPredicate;
 class ASTNode;
 class Set;
-typedef class Set MutableSet;
+class MutableSet;
 
 class ElementFunction;
 class ElementSet;
index b6adc3f3039edc99e9bfb0a33e0b3e037ed471c5..e8ea646fc66368a8461b935cec2a5bead4c242da 100644 (file)
 
 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;
 }
 
index e8527f0eed35b418a41b03c453469bfd8f5c93e4..b2741fdb6fcef7c3e79d6b323083005ea81be758 100644 (file)
@@ -17,25 +17,25 @@ class CSolver {
        HashSetBoolean *constraints;
 
        /** This is a vector of all boolean structs that we have allocated. */
-       VectorBoolean *allBooleans;
+       Vector<Boolean *> allBooleans;
 
        /** This is a vector of all set structs that we have allocated. */
-       VectorSet *allSets;
+       Vector<Set *> allSets;
 
        /** This is a vector of all element structs that we have allocated. */
-       VectorElement *allElements;
+       Vector<Element *> allElements;
 
        /** This is a vector of all predicate structs that we have allocated. */
-       VectorPredicate *allPredicates;
+       Vector<Predicate *> allPredicates;
 
        /** This is a vector of all table structs that we have allocated. */
-       VectorTable *allTables;
+       Vector<Table *> allTables;
 
        /** This is a vector of all order structs that we have allocated. */
-       VectorOrder *allOrders;
+       Vector<Order *> allOrders;
 
        /** This is a vector of all function structs that we have allocated. */
-       VectorFunction *allFunctions;
+       Vector<Function *> allFunctions;
 
        /** This function creates a set containing the elements passed in the array. */