From 7ab5516d0205e463969af92c1b200a316d4a08f0 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Sat, 26 Aug 2017 18:11:20 -0700 Subject: [PATCH] Run tabbing pass --- src/AST/astnode.h | 4 +- src/AST/boolean.h | 12 +-- src/AST/element.cc | 2 +- src/AST/element.h | 8 +- src/AST/function.h | 8 +- src/AST/mutableset.h | 2 +- src/AST/order.h | 4 +- src/AST/predicate.cc | 2 +- src/AST/predicate.h | 8 +- src/AST/rewriter.cc | 2 +- src/AST/set.h | 4 +- src/AST/table.cc | 2 +- src/AST/table.h | 2 +- src/ASTAnalyses/orderedge.h | 2 +- src/ASTAnalyses/orderencoder.cc | 66 ++++++++-------- src/ASTAnalyses/orderencoder.h | 4 +- src/ASTAnalyses/ordergraph.h | 10 +-- src/ASTAnalyses/ordernode.h | 2 +- src/ASTAnalyses/polarityassignment.cc | 4 +- src/ASTTransform/integerencoding.cc | 26 +++---- src/ASTTransform/integerencoding.h | 6 +- src/ASTTransform/orderdecompose.cc | 46 ++++++------ src/ASTTransform/orderdecompose.h | 4 +- src/Backend/constraint.cc | 20 ++--- src/Backend/orderelement.cc | 2 +- src/Backend/orderelement.h | 6 +- src/Backend/orderpair.h | 4 +- src/Backend/satencoder.cc | 6 +- src/Backend/satfuncopencoder.cc | 18 ++--- src/Backend/satfunctableencoder.cc | 2 +- src/Backend/satorderencoder.cc | 32 ++++---- src/Backend/satorderencoder.h | 2 +- src/Backend/sattranslator.h | 2 +- src/Collections/array.h | 82 ++++++++++---------- src/Collections/cppvector.h | 100 ++++++++++++------------- src/Collections/hashset.h | 104 +++++++++++++------------- src/Collections/hashtable.h | 32 ++++---- src/Collections/structs.cc | 4 +- src/Collections/structs.h | 4 +- src/Encoders/elementencoding.h | 4 +- src/Encoders/functionencoding.h | 2 +- src/Encoders/naiveencoder.cc | 4 +- src/Encoders/orderencoding.h | 2 +- src/Test/logicopstest.cc | 10 +-- src/Test/ordergraphtest.cc | 36 ++++----- src/Test/tablefuncencodetest.cc | 2 +- src/Test/tablepredicencodetest.cc | 4 +- src/Tuner/tunable.cc | 4 +- src/Tuner/tunable.h | 10 +-- src/csolver.cc | 2 +- src/csolver.h | 28 +++---- src/mymemory.h | 30 ++++---- 52 files changed, 394 insertions(+), 394 deletions(-) diff --git a/src/AST/astnode.h b/src/AST/astnode.h index 8cc126a..749bf8e 100644 --- a/src/AST/astnode.h +++ b/src/AST/astnode.h @@ -4,8 +4,8 @@ #include "ops.h" class ASTNode { - public: - ASTNode(ASTNodeType _type) : type(_type) {} +public: + ASTNode(ASTNodeType _type) : type(_type) {} ASTNodeType type; MEMALLOC; }; diff --git a/src/AST/boolean.h b/src/AST/boolean.h index 4bab811..c9722a9 100644 --- a/src/AST/boolean.h +++ b/src/AST/boolean.h @@ -18,7 +18,7 @@ #define GETBOOLEANVALUE(b) (b->boolVal) class Boolean : public ASTNode { - public: +public: Boolean(ASTNodeType _type); virtual ~Boolean() {} Polarity polarity; @@ -28,7 +28,7 @@ class Boolean : public ASTNode { }; class BooleanVar : public Boolean { - public: +public: BooleanVar(VarType t); VarType vtype; Edge var; @@ -36,7 +36,7 @@ class BooleanVar : public Boolean { }; class BooleanOrder : public Boolean { - public: +public: BooleanOrder(Order *_order, uint64_t _first, uint64_t _second); Order *order; uint64_t first; @@ -45,19 +45,19 @@ class BooleanOrder : public Boolean { }; class BooleanPredicate : public Boolean { - public: +public: BooleanPredicate(Predicate *_predicate, Element **_inputs, uint _numInputs, Boolean *_undefinedStatus); ~BooleanPredicate(); Predicate *predicate; FunctionEncoding encoding; Array inputs; Boolean *undefStatus; - FunctionEncoding * getFunctionEncoding() {return &encoding;} + FunctionEncoding *getFunctionEncoding() {return &encoding;} MEMALLOC; }; class BooleanLogic : public Boolean { - public: +public: BooleanLogic(CSolver *solver, LogicOp _op, Boolean **array, uint asize); LogicOp op; Array inputs; diff --git a/src/AST/element.cc b/src/AST/element.cc index be4f77b..32b372a 100644 --- a/src/AST/element.cc +++ b/src/AST/element.cc @@ -26,7 +26,7 @@ ElementFunction::ElementFunction(Function *_function, Element **array, uint numA } ElementConst::ElementConst(uint64_t _value, VarType _type) : Element(ELEMCONST), value(_value) { - uint64_t array[]={value}; + uint64_t array[] = {value}; set = new Set(_type, array, 1); } diff --git a/src/AST/element.h b/src/AST/element.h index 6a8ea95..f563586 100644 --- a/src/AST/element.h +++ b/src/AST/element.h @@ -11,7 +11,7 @@ #define GETELEMENTTYPE(o) (o->type) #define GETELEMENTPARENTS(o) (&((Element *)o)->parents) class Element : public ASTNode { - public: +public: Element(ASTNodeType type); virtual ~Element(); Vector parents; @@ -20,7 +20,7 @@ class Element : public ASTNode { }; class ElementConst : public Element { - public: +public: ElementConst(uint64_t value, VarType type); ~ElementConst(); Set *set; @@ -29,14 +29,14 @@ class ElementConst : public Element { }; class ElementSet : public Element { - public: +public: ElementSet(Set *s); Set *set; MEMALLOC; }; class ElementFunction : public Element { - public: +public: ElementFunction(Function *function, Element **array, uint numArrays, Boolean *overflowstatus); ~ElementFunction(); Function *function; diff --git a/src/AST/function.h b/src/AST/function.h index 9b6f254..2cd5cca 100644 --- a/src/AST/function.h +++ b/src/AST/function.h @@ -8,15 +8,15 @@ #define GETFUNCTIONTYPE(o) (((Function *)o)->type) class Function { - public: - Function(FunctionType _type) : type(_type) {} +public: + Function(FunctionType _type) : type(_type) {} FunctionType type; MEMALLOC; virtual ~Function() {} }; class FunctionOperator : public Function { - public: +public: ArithOp op; Array domains; Set *range; @@ -28,7 +28,7 @@ class FunctionOperator : public Function { }; class FunctionTable : public Function { - public: +public: Table *table; UndefinedBehavior undefBehavior; FunctionTable (Table *table, UndefinedBehavior behavior); diff --git a/src/AST/mutableset.h b/src/AST/mutableset.h index b0359d3..3c2f937 100644 --- a/src/AST/mutableset.h +++ b/src/AST/mutableset.h @@ -3,7 +3,7 @@ #include "set.h" class MutableSet : public Set { - public: +public: MutableSet(VarType t); void addElementMSet(uint64_t element); MEMALLOC; diff --git a/src/AST/order.h b/src/AST/order.h index 1645786..8d21240 100644 --- a/src/AST/order.h +++ b/src/AST/order.h @@ -9,13 +9,13 @@ #include "orderpair.h" class Order { - public: +public: Order(OrderType type, Set *set); ~Order(); OrderType type; Set *set; HashTableOrderPair *orderPairTable; - HashSetOrderElement* elementTable; + HashSetOrderElement *elementTable; OrderGraph *graph; Vector constraints; OrderEncoding order; diff --git a/src/AST/predicate.cc b/src/AST/predicate.cc index feff67a..0e04668 100644 --- a/src/AST/predicate.cc +++ b/src/AST/predicate.cc @@ -3,7 +3,7 @@ #include "set.h" #include "table.h" -PredicateOperator::PredicateOperator(CompOp _op, Set **domain, uint numDomain) : Predicate(OPERATORPRED) , op(_op), domains(domain, numDomain) { +PredicateOperator::PredicateOperator(CompOp _op, Set **domain, uint numDomain) : Predicate(OPERATORPRED), op(_op), domains(domain, numDomain) { } PredicateTable::PredicateTable(Table *_table, UndefinedBehavior _undefBehavior) : Predicate(TABLEPRED), table(_table), undefinedbehavior(_undefBehavior) { diff --git a/src/AST/predicate.h b/src/AST/predicate.h index 96f462d..46bc5af 100644 --- a/src/AST/predicate.h +++ b/src/AST/predicate.h @@ -8,15 +8,15 @@ #define GETPREDICATETYPE(o) (((Predicate *)(o))->type) class Predicate { - public: - Predicate(PredicateType _type) : type(_type) {} +public: + Predicate(PredicateType _type) : type(_type) {} virtual ~Predicate() {} PredicateType type; MEMALLOC; }; class PredicateOperator : public Predicate { - public: +public: PredicateOperator(CompOp op, Set **domain, uint numDomain); bool evalPredicateOperator(uint64_t *inputs); CompOp op; @@ -25,7 +25,7 @@ class PredicateOperator : public Predicate { }; class PredicateTable : public Predicate { - public: +public: PredicateTable(Table *table, UndefinedBehavior undefBehavior); Table *table; UndefinedBehavior undefinedbehavior; diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc index e8e9c84..f32fc91 100644 --- a/src/AST/rewriter.cc +++ b/src/AST/rewriter.cc @@ -138,7 +138,7 @@ void CSolver::replaceBooleanWithFalse(Boolean *bexpr) { setUnSAT(); constraints.remove(bexpr); } - + uint size = bexpr->parents.getSize(); for (uint i = 0; i < size; i++) { Boolean *parent = bexpr->parents.get(i); diff --git a/src/AST/set.h b/src/AST/set.h index 9303fa8..bb246b6 100644 --- a/src/AST/set.h +++ b/src/AST/set.h @@ -13,7 +13,7 @@ #include "mymemory.h" class Set { - public: +public: Set(VarType t); Set(VarType t, uint64_t *elements, uint num); Set(VarType t, uint64_t lowrange, uint64_t highrange); @@ -21,7 +21,7 @@ class Set { bool exists(uint64_t element); uint getSize(); uint64_t getElement(uint index); - + VarType type; bool isRange; uint64_t low;//also used to count unique items diff --git a/src/AST/table.cc b/src/AST/table.cc index 016b3cc..d54aefb 100644 --- a/src/AST/table.cc +++ b/src/AST/table.cc @@ -21,7 +21,7 @@ void Table::addNewTableEntry(uint64_t *inputs, uint inputSize, uint64_t result) ASSERT(status); } -TableEntry * Table::getTableEntry(uint64_t *inputs, uint inputSize) { +TableEntry *Table::getTableEntry(uint64_t *inputs, uint inputSize) { TableEntry *temp = allocTableEntry(inputs, inputSize, -1); TableEntry *result = entries->get(temp); deleteTableEntry(temp); diff --git a/src/AST/table.h b/src/AST/table.h index f232615..28b13e4 100644 --- a/src/AST/table.h +++ b/src/AST/table.h @@ -5,7 +5,7 @@ #include "structs.h" class Table { - public: +public: Table(Set **domains, uint numDomain, Set *range); void addNewTableEntry(uint64_t *inputs, uint inputSize, uint64_t result); TableEntry *getTableEntry(uint64_t *inputs, uint inputSize); diff --git a/src/ASTAnalyses/orderedge.h b/src/ASTAnalyses/orderedge.h index 7063f34..9b1af29 100644 --- a/src/ASTAnalyses/orderedge.h +++ b/src/ASTAnalyses/orderedge.h @@ -11,7 +11,7 @@ #include "mymemory.h" class OrderEdge { - public: +public: OrderEdge(OrderNode *begin, OrderNode *end); OrderNode *source; diff --git a/src/ASTAnalyses/orderencoder.cc b/src/ASTAnalyses/orderencoder.cc index 10adc81..5d94206 100644 --- a/src/ASTAnalyses/orderencoder.cc +++ b/src/ASTAnalyses/orderencoder.cc @@ -46,8 +46,8 @@ void DFSNodeVisit(OrderNode *node, Vector *finishNodes, bool isReve if (!edge->mustPos) continue; } else - if (!edge->polPos && !edge->pseudoPos)//Ignore edges that do not have positive polarity - continue; + if (!edge->polPos && !edge->pseudoPos) //Ignore edges that do not have positive polarity + continue; OrderNode *child = isReverse ? edge->source : edge->sink; @@ -80,34 +80,34 @@ void computeStronglyConnectedComponentGraph(OrderGraph *graph) { resetNodeInfoStatusSCC(graph); } -bool isMustBeTrueNode(OrderNode* node){ - HSIteratorOrderEdge* iterator = node->inEdges.iterator(); - while(iterator->hasNext()){ - OrderEdge* edge = iterator->next(); - if(!edge->mustPos) +bool isMustBeTrueNode(OrderNode *node) { + HSIteratorOrderEdge *iterator = node->inEdges.iterator(); + while (iterator->hasNext()) { + OrderEdge *edge = iterator->next(); + if (!edge->mustPos) return false; } delete iterator; iterator = node->outEdges.iterator(); - while(iterator->hasNext()){ - OrderEdge* edge = iterator->next(); - if(!edge->mustPos) + while (iterator->hasNext()) { + OrderEdge *edge = iterator->next(); + if (!edge->mustPos) return false; } delete iterator; return true; } -void bypassMustBeTrueNode(CSolver *This, OrderGraph* graph, OrderNode* node){ - HSIteratorOrderEdge* iterin = node->inEdges.iterator(); - while(iterin->hasNext()){ - OrderEdge* inEdge = iterin->next(); - OrderNode* srcNode = inEdge->source; +void bypassMustBeTrueNode(CSolver *This, OrderGraph *graph, OrderNode *node) { + 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(); - while(iterout->hasNext()){ - OrderEdge* outEdge = iterout->next(); - OrderNode* sinkNode = outEdge->sink; + HSIteratorOrderEdge *iterout = node->outEdges.iterator(); + while (iterout->hasNext()) { + OrderEdge *outEdge = iterout->next(); + OrderNode *sinkNode = outEdge->sink; sinkNode->inEdges.remove(outEdge); //Adding new edge to new sink and src nodes ... OrderEdge *newEdge = graph->getOrderEdgeFromOrderGraph(srcNode, sinkNode); @@ -124,10 +124,10 @@ void bypassMustBeTrueNode(CSolver *This, OrderGraph* graph, OrderNode* node){ } void removeMustBeTrueNodes(CSolver *This, OrderGraph *graph) { - HSIteratorOrderNode* iterator = graph->getNodes(); - while(iterator->hasNext()) { - OrderNode* node = iterator->next(); - if(isMustBeTrueNode(node)){ + HSIteratorOrderNode *iterator = graph->getNodes(); + while (iterator->hasNext()) { + OrderNode *node = iterator->next(); + if (isMustBeTrueNode(node)) { bypassMustBeTrueNode(This, graph, node); } } @@ -135,9 +135,9 @@ void removeMustBeTrueNodes(CSolver *This, OrderGraph *graph) { } /** This function computes a source set for every nodes, the set of - nodes that can reach that node via pospolarity edges. It then - looks for negative polarity edges from nodes in the the source set - to determine whether we need to generate pseudoPos edges. */ + nodes that can reach that node via pospolarity edges. It then + looks for negative polarity edges from nodes in the the source set + to determine whether we need to generate pseudoPos edges. */ void completePartialOrderGraph(OrderGraph *graph) { Vector finishNodes; @@ -146,14 +146,14 @@ void completePartialOrderGraph(OrderGraph *graph) { HashTableNodeToNodeSet *table = new HashTableNodeToNodeSet(128, 0.25); Vector sccNodes; - + uint size = finishNodes.getSize(); uint sccNum = 1; for (int i = size - 1; i >= 0; i--) { OrderNode *node = finishNodes.get(i); HashSetOrderNode *sources = new HashSetOrderNode(4, 0.25); table->put(node, sources); - + if (node->status == NOTVISITED) { //Need to do reverse traversal here... node->status = VISITED; @@ -180,10 +180,10 @@ void completePartialOrderGraph(OrderGraph *graph) { } delete iterator; } - for (uint j=0; j < rSize; j++) { + for (uint j = 0; j < rSize; j++) { //Copy in set of entire SCC OrderNode *rnode = sccNodes.get(j); - HashSetOrderNode * set = (j==0) ? sources : sources->copy(); + HashSetOrderNode *set = (j == 0) ? sources : sources->copy(); table->put(rnode, set); //Use source sets to compute pseudoPos edges @@ -200,7 +200,7 @@ void completePartialOrderGraph(OrderGraph *graph) { } delete iterator; } - + sccNodes.clear(); } } @@ -264,7 +264,7 @@ void DFSClearContradictions(CSolver *solver, OrderGraph *graph, VectorinEdges.iterator(); + HSIteratorOrderEdge *iterator = node->inEdges.iterator(); while (iterator->hasNext()) { OrderEdge *edge = iterator->next(); OrderNode *parent = edge->source; @@ -303,7 +303,7 @@ void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector finishNodes; //Topologically sort the mustPos edge graph DFSMust(graph, &finishNodes); diff --git a/src/ASTAnalyses/orderencoder.h b/src/ASTAnalyses/orderencoder.h index 19240cf..57a6e5c 100644 --- a/src/ASTAnalyses/orderencoder.h +++ b/src/ASTAnalyses/orderencoder.h @@ -18,8 +18,8 @@ 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); +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, Vector *finishNodes); diff --git a/src/ASTAnalyses/ordergraph.h b/src/ASTAnalyses/ordergraph.h index 8dd2e65..eb756a8 100644 --- a/src/ASTAnalyses/ordergraph.h +++ b/src/ASTAnalyses/ordergraph.h @@ -12,7 +12,7 @@ #include "mymemory.h" class OrderGraph { - public: +public: OrderGraph(Order *order); ~OrderGraph(); void addOrderConstraintToOrderGraph(BooleanOrder *bOrder); @@ -25,11 +25,11 @@ class OrderGraph { void addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr); OrderEdge *getInverseOrderEdge(OrderEdge *edge); Order *getOrder() {return order;} - HSIteratorOrderNode * getNodes() {return nodes->iterator();} - HSIteratorOrderEdge * getEdges() {return edges->iterator();} - + HSIteratorOrderNode *getNodes() {return nodes->iterator();} + HSIteratorOrderEdge *getEdges() {return edges->iterator();} + MEMALLOC; - private: +private: HashSetOrderNode *nodes; HashSetOrderEdge *edges; Order *order; diff --git a/src/ASTAnalyses/ordernode.h b/src/ASTAnalyses/ordernode.h index a63dd7f..36bb3df 100644 --- a/src/ASTAnalyses/ordernode.h +++ b/src/ASTAnalyses/ordernode.h @@ -18,7 +18,7 @@ enum NodeStatus {NOTVISITED, VISITED, FINISHED, ADDEDTOSET}; typedef enum NodeStatus NodeStatus; class OrderNode { - public: +public: OrderNode(uint64_t id); void addNewIncomingEdge(OrderEdge *edge); void addNewOutgoingEdge(OrderEdge *edge); diff --git a/src/ASTAnalyses/polarityassignment.cc b/src/ASTAnalyses/polarityassignment.cc index 947f28e..705f5d9 100644 --- a/src/ASTAnalyses/polarityassignment.cc +++ b/src/ASTAnalyses/polarityassignment.cc @@ -2,8 +2,8 @@ #include "csolver.h" void computePolarities(CSolver *This) { - HSIteratorBoolean *iterator=This->getConstraints(); - while(iterator->hasNext()) { + HSIteratorBoolean *iterator = This->getConstraints(); + while (iterator->hasNext()) { Boolean *boolean = iterator->next(); updatePolarity(boolean, P_TRUE); updateMustValue(boolean, BV_MUSTBETRUE); diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc index 4fe381a..0a415b9 100644 --- a/src/ASTTransform/integerencoding.cc +++ b/src/ASTTransform/integerencoding.cc @@ -9,29 +9,29 @@ #include "set.h" -void orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder){ - Order* order = boolOrder->order; +void orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder) { + Order *order = boolOrder->order; if (order->elementTable == NULL) { order->initializeOrderElementsHashTable(); } //getting two elements and using LT predicate ... - ElementSet* elem1 = (ElementSet*)getOrderIntegerElement(This, order, boolOrder->first); - ElementSet* elem2 = (ElementSet*)getOrderIntegerElement(This, order, boolOrder->second); - Set * sarray[]={elem1->set, elem2->set}; - Predicate *predicate =This->solver->createPredicateOperator(LT, sarray, 2); - Element * parray[]={elem1, elem2}; - Boolean * boolean=This->solver->applyPredicate(predicate, parray, 2); + ElementSet *elem1 = (ElementSet *)getOrderIntegerElement(This, order, boolOrder->first); + ElementSet *elem2 = (ElementSet *)getOrderIntegerElement(This, order, boolOrder->second); + Set *sarray[] = {elem1->set, elem2->set}; + Predicate *predicate = This->solver->createPredicateOperator(LT, sarray, 2); + Element *parray[] = {elem1, elem2}; + Boolean *boolean = This->solver->applyPredicate(predicate, parray, 2); This->solver->addConstraint(boolean); This->solver->replaceBooleanWithBoolean(boolOrder, boolean); } -Element* getOrderIntegerElement(SATEncoder* This,Order *order, uint64_t item) { - HashSetOrderElement* eset = order->elementTable; +Element *getOrderIntegerElement(SATEncoder *This,Order *order, uint64_t item) { + HashSetOrderElement *eset = order->elementTable; OrderElement oelement(item, NULL); - if( !eset->contains(&oelement)){ - Set* set = This->solver->createRangeSet(order->set->type, 1, (uint64_t) order->set->getSize()); - Element* elem = This->solver->getElementVar(set); + if ( !eset->contains(&oelement)) { + Set *set = This->solver->createRangeSet(order->set->type, 1, (uint64_t) order->set->getSize()); + Element *elem = This->solver->getElementVar(set); eset->add(new OrderElement(item, elem)); return elem; } else diff --git a/src/ASTTransform/integerencoding.h b/src/ASTTransform/integerencoding.h index 9b5a808..15fbdd7 100644 --- a/src/ASTTransform/integerencoding.h +++ b/src/ASTTransform/integerencoding.h @@ -4,7 +4,7 @@ * and open the template in the editor. */ -/* +/* * File: integerencoding.h * Author: hamed * @@ -16,9 +16,9 @@ #include "classlist.h" #include "structs.h" -Element* getOrderIntegerElement(SATEncoder* This,Order *order, uint64_t item); +Element *getOrderIntegerElement(SATEncoder *This,Order *order, uint64_t item); void orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder); -#endif /* INTEGERENCODING_H */ +#endif/* INTEGERENCODING_H */ diff --git a/src/ASTTransform/orderdecompose.cc b/src/ASTTransform/orderdecompose.cc index 4962046..18602cc 100644 --- a/src/ASTTransform/orderdecompose.cc +++ b/src/ASTTransform/orderdecompose.cc @@ -14,14 +14,14 @@ #include "integerencoding.h" void orderAnalysis(CSolver *This) { - Vector * orders=This->getOrders(); + Vector *orders = This->getOrders(); uint size = orders->getSize(); for (uint i = 0; i < size; i++) { Order *order = orders->get(i); - bool doDecompose=GETVARTUNABLE(This->getTuner(), order->type, DECOMPOSEORDER, &onoff); + bool doDecompose = GETVARTUNABLE(This->getTuner(), order->type, DECOMPOSEORDER, &onoff); if (!doDecompose) continue; - + OrderGraph *graph = buildOrderGraph(order); if (order->type == PARTIAL) { //Required to do SCC analysis for partial order graphs. It @@ -31,13 +31,13 @@ void orderAnalysis(CSolver *This) { } - bool mustReachGlobal=GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHGLOBAL, &onoff); + bool mustReachGlobal = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHGLOBAL, &onoff); if (mustReachGlobal) reachMustAnalysis(This, graph, false); - bool mustReachLocal=GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHLOCAL, &onoff); - + bool mustReachLocal = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHLOCAL, &onoff); + if (mustReachLocal) { //This pair of analysis is also optional if (order->type == PARTIAL) { @@ -47,26 +47,26 @@ void orderAnalysis(CSolver *This) { } } - bool mustReachPrune=GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHPRUNE, &onoff); - + bool mustReachPrune = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHPRUNE, &onoff); + if (mustReachPrune) removeMustBeTrueNodes(This, graph); - + //This is needed for splitorder computeStronglyConnectedComponentGraph(graph); decomposeOrder(This, order, graph); delete graph; - + /* - OrderIntegerEncodingSATEncoder wants a private field that it really shoukldn't need... + OrderIntegerEncodingSATEncoder wants a private field that it really shoukldn't need... - bool doIntegerEncoding = GETVARTUNABLE(This->getTuner(), order->order.type, ORDERINTEGERENCODING, &offon ); - if(!doIntegerEncoding) - continue; - uint size = order->constraints.getSize(); - for(uint i=0; isatEncoder, order->constraints.get(i)); - }*/ + bool doIntegerEncoding = GETVARTUNABLE(This->getTuner(), order->order.type, ORDERINTEGERENCODING, &offon ); + if(!doIntegerEncoding) + continue; + uint size = order->constraints.getSize(); + for(uint i=0; isatEncoder, order->constraints.get(i)); + }*/ } } @@ -81,7 +81,7 @@ void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) { OrderNode *to = graph->getOrderNodeFromOrderGraph(orderconstraint->second); model_print("from->sccNum:%u\tto->sccNum:%u\n", from->sccNum, to->sccNum); if (from->sccNum != to->sccNum) { - OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to); + OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to); if (edge->polPos) { This->replaceBooleanWithTrue(orderconstraint); } else if (edge->polNeg) { @@ -122,10 +122,10 @@ void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) { } } - uint pcvsize=partialcandidatevec.getSize(); - for(uint i=0;itype = TOTAL; model_print("i=%u\t", i); } diff --git a/src/ASTTransform/orderdecompose.h b/src/ASTTransform/orderdecompose.h index b88fded..85a5481 100644 --- a/src/ASTTransform/orderdecompose.h +++ b/src/ASTTransform/orderdecompose.h @@ -4,7 +4,7 @@ * and open the template in the editor. */ -/* +/* * File: orderdecompose.h * Author: hamed * @@ -19,5 +19,5 @@ void orderAnalysis(CSolver *This); void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph); -#endif /* ORDERDECOMPOSE_H */ +#endif/* ORDERDECOMPOSE_H */ diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc index df812df..1c36cd1 100644 --- a/src/Backend/constraint.cc +++ b/src/Backend/constraint.cc @@ -885,26 +885,26 @@ Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) { return constraintAND(cnf, numvars, array); } -Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2){ - if(numvars == 0 ) +Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) { + if (numvars == 0 ) return E_False; - Edge result =constraintAND2(cnf, constraintNegate( var1[0]), var2[0]); + Edge result = constraintAND2(cnf, constraintNegate( var1[0]), var2[0]); for (uint i = 1; i < numvars; i++) { Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]); - Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result); - result = constraintOR2(cnf, lt, eq); + Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result); + result = constraintOR2(cnf, lt, eq); } return result; } -Edge generateLTEConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2){ - if(numvars == 0 ) +Edge generateLTEConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) { + if (numvars == 0 ) return E_True; - Edge result =constraintIMPLIES(cnf, var1[0], var2[0]); + Edge result = constraintIMPLIES(cnf, var1[0], var2[0]); for (uint i = 1; i < numvars; i++) { Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]); - Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result); - result = constraintOR2(cnf, lt, eq); + Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result); + result = constraintOR2(cnf, lt, eq); } return result; } diff --git a/src/Backend/orderelement.cc b/src/Backend/orderelement.cc index 01d0ada..679a656 100644 --- a/src/Backend/orderelement.cc +++ b/src/Backend/orderelement.cc @@ -1,7 +1,7 @@ #include "orderelement.h" -OrderElement::OrderElement(uint64_t _item, Element* _elem) { +OrderElement::OrderElement(uint64_t _item, Element *_elem) { elem = _elem; item = _item; } diff --git a/src/Backend/orderelement.h b/src/Backend/orderelement.h index 7199405..a5f08a3 100644 --- a/src/Backend/orderelement.h +++ b/src/Backend/orderelement.h @@ -13,10 +13,10 @@ #include "constraint.h" class OrderElement { - public: - OrderElement(uint64_t item, Element* elem); +public: + OrderElement(uint64_t item, Element *elem); uint64_t item; - Element* elem; + Element *elem; MEMALLOC; }; diff --git a/src/Backend/orderpair.h b/src/Backend/orderpair.h index b34ea1a..6fc5df1 100644 --- a/src/Backend/orderpair.h +++ b/src/Backend/orderpair.h @@ -13,10 +13,10 @@ #include "constraint.h" class OrderPair { - public: +public: OrderPair(uint64_t first, uint64_t second, Edge constraint); OrderPair(); - uint64_t first; + uint64_t first; uint64_t second; Edge constraint; MEMALLOC; diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc index 91e323d..3dd9933 100644 --- a/src/Backend/satencoder.cc +++ b/src/Backend/satencoder.cc @@ -29,13 +29,13 @@ void deleteSATEncoder(SATEncoder *This) { } void encodeAllSATEncoder(CSolver *csolver, SATEncoder *This) { - HSIteratorBoolean *iterator=csolver->getConstraints(); - while(iterator->hasNext()) { + HSIteratorBoolean *iterator = csolver->getConstraints(); + while (iterator->hasNext()) { Boolean *constraint = iterator->next(); model_print("Encoding All ...\n\n"); Edge c = encodeConstraintSATEncoder(This, constraint); model_print("Returned Constraint in EncodingAll:\n"); - ASSERT( ! equalsEdge(c, E_BOGUS)); + ASSERT( !equalsEdge(c, E_BOGUS)); addConstraintCNF(This->cnf, c); } delete iterator; diff --git a/src/Backend/satfuncopencoder.cc b/src/Backend/satfuncopencoder.cc index 7f7341a..695493b 100644 --- a/src/Backend/satfuncopencoder.cc +++ b/src/Backend/satfuncopencoder.cc @@ -49,7 +49,7 @@ Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder *This, BooleanPredicate *c bool notfinished = true; while (notfinished) { Edge carray[numDomains]; - + if (predicate->evalPredicateOperator(vals) != generateNegation) { //Include this in the set of terms for (uint i = 0; i < numDomains; i++) { @@ -206,14 +206,14 @@ Edge encodeCircuitOperatorPredicateEncoder(SATEncoder *This, BooleanPredicate *c ASSERT(ee0->numVars == ee1->numVars); uint numVars = ee0->numVars; switch (predicate->op) { - case EQUALS: - return generateEquivNVConstraint(This->cnf, numVars, ee0->variables, ee1->variables); - case LT: - return generateLTConstraint(This->cnf, numVars, ee0->variables, ee1->variables); - case GT: - return generateLTConstraint(This->cnf, numVars, ee1->variables, ee0->variables); - default: - ASSERT(0); + case EQUALS: + return generateEquivNVConstraint(This->cnf, numVars, ee0->variables, ee1->variables); + case LT: + return generateLTConstraint(This->cnf, numVars, ee0->variables, ee1->variables); + case GT: + return generateLTConstraint(This->cnf, numVars, ee1->variables, ee0->variables); + default: + ASSERT(0); } exit(-1); } diff --git a/src/Backend/satfunctableencoder.cc b/src/Backend/satfunctableencoder.cc index 0efe02c..27cf8c7 100644 --- a/src/Backend/satfunctableencoder.cc +++ b/src/Backend/satfunctableencoder.cc @@ -16,7 +16,7 @@ Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder *This, BooleanPredicat ASSERT(undefStatus == IGNOREBEHAVIOR || undefStatus == FLAGFORCEUNDEFINED); Table *table = ((PredicateTable *)constraint->predicate)->table; FunctionEncodingType encType = constraint->encoding.type; - Array * inputs = &constraint->inputs; + Array *inputs = &constraint->inputs; uint inputNum = inputs->getSize(); uint size = table->entries->getSize(); bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE; diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc index 640ac1a..5744736 100644 --- a/src/Backend/satorderencoder.cc +++ b/src/Backend/satorderencoder.cc @@ -15,30 +15,30 @@ Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint) { switch ( constraint->order->type) { - case PARTIAL: - return encodePartialOrderSATEncoder(This, constraint); - case TOTAL: - return encodeTotalOrderSATEncoder(This, constraint); - default: - ASSERT(0); + case PARTIAL: + return encodePartialOrderSATEncoder(This, constraint); + case TOTAL: + return encodeTotalOrderSATEncoder(This, constraint); + default: + ASSERT(0); } return E_BOGUS; } -Edge inferOrderConstraintFromGraph(Order* order, uint64_t _first, uint64_t _second){ +Edge inferOrderConstraintFromGraph(Order *order, uint64_t _first, uint64_t _second) { if (order->graph != NULL) { - OrderGraph *graph=order->graph; - OrderNode *first=graph->lookupOrderNodeFromOrderGraph(_first); - OrderNode *second=graph->lookupOrderNodeFromOrderGraph(_second); + OrderGraph *graph = order->graph; + OrderNode *first = graph->lookupOrderNodeFromOrderGraph(_first); + OrderNode *second = graph->lookupOrderNodeFromOrderGraph(_second); if ((first != NULL) && (second != NULL)) { - OrderEdge *edge=graph->lookupOrderEdgeFromOrderGraph(first, second); + OrderEdge *edge = graph->lookupOrderEdgeFromOrderGraph(first, second); if (edge != NULL) { if (edge->mustPos) return E_True; else if (edge->mustNeg) return E_False; } - OrderEdge *invedge=graph->lookupOrderEdgeFromOrderGraph(second, first); + OrderEdge *invedge = graph->lookupOrderEdgeFromOrderGraph(second, first); if (invedge != NULL) { if (invedge->mustPos) return E_False; @@ -52,9 +52,9 @@ Edge inferOrderConstraintFromGraph(Order* order, uint64_t _first, uint64_t _seco Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair) { Edge gvalue = inferOrderConstraintFromGraph(order, pair->first, pair->second); - if(!edgeIsNull(gvalue)) + if (!edgeIsNull(gvalue)) return gvalue; - + HashTableOrderPair *table = order->orderPairTable; bool negate = false; OrderPair flipped; @@ -71,7 +71,7 @@ Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair) { table->put(paircopy, paircopy); } else constraint = table->get(pair)->constraint; - + return negate ? constraintNegate(constraint) : constraint; } @@ -79,7 +79,7 @@ Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder *boolOrder) { ASSERT(boolOrder->order->type == TOTAL); if (boolOrder->order->orderPairTable == NULL) { boolOrder->order->initializeOrderHashTable(); - bool doOptOrderStructure=GETVARTUNABLE(This->solver->getTuner(), boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff); + bool doOptOrderStructure = GETVARTUNABLE(This->solver->getTuner(), boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff); if (doOptOrderStructure) { boolOrder->order->graph = buildMustOrderGraph(boolOrder->order); reachMustAnalysis(This->solver, boolOrder->order->graph, true); diff --git a/src/Backend/satorderencoder.h b/src/Backend/satorderencoder.h index 9b143d9..ca6b4d4 100644 --- a/src/Backend/satorderencoder.h +++ b/src/Backend/satorderencoder.h @@ -2,7 +2,7 @@ #define SATORDERENCODER_H Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint); -Edge inferOrderConstraintFromGraph(Order* order, uint64_t _first, uint64_t _second); +Edge inferOrderConstraintFromGraph(Order *order, uint64_t _first, uint64_t _second); Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair); Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint); Edge encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint); diff --git a/src/Backend/sattranslator.h b/src/Backend/sattranslator.h index be5c8c0..1d9964f 100644 --- a/src/Backend/sattranslator.h +++ b/src/Backend/sattranslator.h @@ -15,7 +15,7 @@ bool getBooleanVariableValueSATTranslator( CSolver *This, Boolean *boolean); HappenedBefore getOrderConstraintValueSATTranslator(CSolver *This, Order *order, uint64_t first, uint64_t second); /** - * most significant bit is represented by variable index 0 + * most significant bit is represented by variable index 0 */ uint64_t getElementValueBinaryIndexSATTranslator(CSolver *This, ElementEncoding *elemEnc); uint64_t getElementValueBinaryValueSATTranslator(CSolver *This, ElementEncoding *elemEnc); diff --git a/src/Collections/array.h b/src/Collections/array.h index 6197de7..496bdc6 100644 --- a/src/Collections/array.h +++ b/src/Collections/array.h @@ -3,49 +3,49 @@ template class Array { - public: - Array(uint _size) : - array((type *)ourcalloc(1, sizeof(type) * _size)), +public: + Array(uint _size) : + array((type *)ourcalloc(1, sizeof(type) * _size)), size(_size) - { - } - - Array(type * _array, uint _size) : - array((type *)ourcalloc(1, sizeof(type) * _size)), + { + } + + Array(type *_array, uint _size) : + array((type *)ourcalloc(1, sizeof(type) * _size)), size(_size) { - memcpy(array, _array, _size * sizeof(type)); - } - - ~Array() { - ourfree(array); - } - - void remove(uint index) { - size--; - for (; index < size; index++) { - array[index] = array[index + 1]; - } - } - - type get(uint index) { - return array[index]; - } - - void set(uint index, type item) { - array[index] = item; - } - - uint getSize() { - return size; - } - - type *expose() { - return array; - } - - private: - type *array; - uint size; + memcpy(array, _array, _size * sizeof(type)); + } + + ~Array() { + ourfree(array); + } + + void remove(uint index) { + size--; + for (; index < size; index++) { + array[index] = array[index + 1]; + } + } + + type get(uint index) { + return array[index]; + } + + void set(uint index, type item) { + array[index] = item; + } + + uint getSize() { + return size; + } + + type *expose() { + return array; + } + +private: + type *array; + uint size; }; diff --git a/src/Collections/cppvector.h b/src/Collections/cppvector.h index a10403e..377ffe4 100644 --- a/src/Collections/cppvector.h +++ b/src/Collections/cppvector.h @@ -6,80 +6,80 @@ template class Vector { - public: - Vector(uint _capacity = VECTOR_DEFCAP) : - size(0), +public: + Vector(uint _capacity = VECTOR_DEFCAP) : + size(0), capacity(_capacity), array((type *) ourmalloc(sizeof(type) * _capacity)) { - } + } - Vector(uint _capacity, type * _array) : - size(_capacity), + Vector(uint _capacity, type *_array) : + size(_capacity), capacity(_capacity), array((type *) ourmalloc(sizeof(type) * _capacity)) { - memcpy(array, _array, capacity * sizeof(type)); + memcpy(array, _array, capacity * sizeof(type)); } - + void pop() { size--; - } + } type last() { - return array[size - 1]; + 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)); + + 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; + 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]; + + type get(uint index) { + return array[index]; } - - void setExpand(uint index, type item) { - if (index >= size) - setSize(index + 1); - set(index, item); + + void setExpand(uint index, type item) { + if (index >= size) + setSize(index + 1); + set(index, item); } - - void set(uint index, type item) { - array[index] = item; + + void set(uint index, type item) { + array[index] = item; } - + uint getSize() { - return size; + return size; } - + ~Vector() { - ourfree(array); + ourfree(array); } - + void clear() { - size = 0; + size = 0; } - + type *expose() { - return array; - } - - private: + return array; + } + +private: uint size; uint capacity; type *array; diff --git a/src/Collections/hashset.h b/src/Collections/hashset.h index b0b987a..6a823f5 100644 --- a/src/Collections/hashset.h +++ b/src/Collections/hashset.h @@ -24,14 +24,14 @@ class HashSet; template, bool (*equals)(_Key, _Key) = default_equals<_Key> > class HSIterator { public: - HSIterator(LinkNode<_Key> *_curr, HashSet <_Key, _KeyInt, _Shift, hash_function, equals> * _set) : + HSIterator(LinkNode<_Key> *_curr, HashSet <_Key, _KeyInt, _Shift, hash_function, equals> *_set) : curr(_curr), set(_set) { } /** Override: new operator */ - void * operator new(size_t size) { + void *operator new(size_t size) { return ourmalloc(size); } @@ -41,7 +41,7 @@ public: } /** Override: new[] operator */ - void * operator new[](size_t size) { + void *operator new[](size_t size) { return ourmalloc(size); } @@ -51,13 +51,13 @@ public: } bool hasNext() { - return curr!=NULL; + return curr != NULL; } _Key next() { - _Key k=curr->key; - last=curr; - curr=curr->next; + _Key k = curr->key; + last = curr; + curr = curr->next; return k; } @@ -66,14 +66,14 @@ public: } void remove() { - _Key k=last->key; + _Key k = last->key; set->remove(k); } private: LinkNode<_Key> *curr; LinkNode<_Key> *last; - HashSet <_Key, _KeyInt, _Shift, hash_function, equals> * set; + HashSet <_Key, _KeyInt, _Shift, hash_function, equals> *set; }; template, bool (*equals)(_Key, _Key) = default_equals<_Key> > @@ -88,41 +88,41 @@ public: /** @brief Hashset destructor */ ~HashSet() { - LinkNode<_Key> *tmp=list; - while(tmp!=NULL) { - LinkNode<_Key> *tmpnext=tmp->next; + LinkNode<_Key> *tmp = list; + while (tmp != NULL) { + LinkNode<_Key> *tmpnext = tmp->next; ourfree(tmp); - tmp=tmpnext; + tmp = tmpnext; } delete table; } - HashSet<_Key, _KeyInt, _Shift, hash_function, equals> * copy() { - HashSet<_Key, _KeyInt, _Shift, hash_function, equals> *copy=new HashSet<_Key, _KeyInt, _Shift, hash_function, equals>(table->getCapacity(), table->getLoadFactor()); - HSIterator<_Key, _KeyInt, _Shift, hash_function, equals> * it=iterator(); - while(it->hasNext()) + HashSet<_Key, _KeyInt, _Shift, hash_function, equals> *copy() { + HashSet<_Key, _KeyInt, _Shift, hash_function, equals> *copy = new HashSet<_Key, _KeyInt, _Shift, hash_function, equals>(table->getCapacity(), table->getLoadFactor()); + HSIterator<_Key, _KeyInt, _Shift, hash_function, equals> *it = iterator(); + while (it->hasNext()) copy->add(it->next()); delete it; return copy; } void reset() { - LinkNode<_Key> *tmp=list; - while(tmp!=NULL) { - LinkNode<_Key> *tmpnext=tmp->next; + LinkNode<_Key> *tmp = list; + while (tmp != NULL) { + LinkNode<_Key> *tmpnext = tmp->next; ourfree(tmp); - tmp=tmpnext; + tmp = tmpnext; } - list=tail=NULL; + list = tail = NULL; table->reset(); } /** @brief Adds a new key to the hashset. Returns false if the key * is already present. */ - void addAll(HashSet<_Key, _KeyInt, _Shift, hash_function, equals> * table) { - HSIterator<_Key, _KeyInt, _Shift, hash_function, equals> * it=iterator(); - while(it->hasNext()) + void addAll(HashSet<_Key, _KeyInt, _Shift, hash_function, equals> *table) { + HSIterator<_Key, _KeyInt, _Shift, hash_function, equals> *it = iterator(); + while (it->hasNext()) add(it->next()); delete it; } @@ -131,17 +131,17 @@ public: * is already present. */ bool add(_Key key) { - LinkNode<_Key> * val=table->get(key); - if (val==NULL) { - LinkNode<_Key> * newnode=(LinkNode<_Key> *)ourmalloc(sizeof(struct LinkNode<_Key>)); - newnode->prev=tail; - newnode->next=NULL; - newnode->key=key; - if (tail!=NULL) - tail->next=newnode; + LinkNode<_Key> *val = table->get(key); + if (val == NULL) { + LinkNode<_Key> *newnode = (LinkNode<_Key> *)ourmalloc(sizeof(struct LinkNode<_Key>)); + newnode->prev = tail; + newnode->next = NULL; + newnode->key = key; + if (tail != NULL) + tail->next = newnode; else - list=newnode; - tail=newnode; + list = newnode; + tail = newnode; table->put(key, newnode); return true; } else @@ -152,8 +152,8 @@ public: * hashset. Returns NULL if not present. */ _Key get(_Key key) { - LinkNode<_Key> * val=table->get(key); - if (val!=NULL) + LinkNode<_Key> *val = table->get(key); + if (val != NULL) return val->key; else return NULL; @@ -164,26 +164,26 @@ public: } bool contains(_Key key) { - return table->get(key)!=NULL; + return table->get(key) != NULL; } bool remove(_Key key) { - LinkNode<_Key> * oldlinknode; - oldlinknode=table->get(key); - if (oldlinknode==NULL) { + LinkNode<_Key> *oldlinknode; + oldlinknode = table->get(key); + if (oldlinknode == NULL) { return false; } table->remove(key); //remove link node from the list - if (oldlinknode->prev==NULL) - list=oldlinknode->next; + if (oldlinknode->prev == NULL) + list = oldlinknode->next; else - oldlinknode->prev->next=oldlinknode->next; - if (oldlinknode->next!=NULL) - oldlinknode->next->prev=oldlinknode->prev; + oldlinknode->prev->next = oldlinknode->next; + if (oldlinknode->next != NULL) + oldlinknode->next->prev = oldlinknode->prev; else - tail=oldlinknode->prev; + tail = oldlinknode->prev; ourfree(oldlinknode); return true; } @@ -193,15 +193,15 @@ public: } bool isEmpty() { - return getSize()==0; + return getSize() == 0; } - HSIterator<_Key, _KeyInt, _Shift, hash_function, equals> * iterator() { + HSIterator<_Key, _KeyInt, _Shift, hash_function, equals> *iterator() { return new HSIterator<_Key, _KeyInt, _Shift, hash_function, equals>(list, this); } /** Override: new operator */ - void * operator new(size_t size) { + void *operator new(size_t size) { return ourmalloc(size); } @@ -211,7 +211,7 @@ public: } /** Override: new[] operator */ - void * operator new[](size_t size) { + void *operator new[](size_t size) { return ourmalloc(size); } @@ -220,7 +220,7 @@ public: ourfree(p); } private: - HashTable<_Key, LinkNode<_Key>*, _KeyInt, _Shift, hash_function, equals> * table; + HashTable<_Key, LinkNode<_Key> *, _KeyInt, _Shift, hash_function, equals> *table; LinkNode<_Key> *list; LinkNode<_Key> *tail; }; diff --git a/src/Collections/hashtable.h b/src/Collections/hashtable.h index c33fe60..528f5f2 100644 --- a/src/Collections/hashtable.h +++ b/src/Collections/hashtable.h @@ -86,7 +86,7 @@ public: } /** Override: new operator */ - void * operator new(size_t size) { + void *operator new(size_t size) { return ourmalloc(size); } @@ -96,7 +96,7 @@ public: } /** Override: new[] operator */ - void * operator new[](size_t size) { + void *operator new[](size_t size) { return ourmalloc(size); } @@ -116,7 +116,7 @@ public: } void resetanddelete() { - for(unsigned int i=0;i *bin = &table[i]; if (bin->key != NULL) { bin->key = NULL; @@ -136,7 +136,7 @@ public: } void resetandfree() { - for(unsigned int i=0;i *bin = &table[i]; if (bin->key != NULL) { bin->key = NULL; @@ -164,11 +164,11 @@ public: /* HashTable cannot handle 0 as a key */ if (!key) { if (!zero) { - zero=(struct hashlistnode<_Key, _Val> *)ourmalloc(sizeof(struct hashlistnode<_Key, _Val>)); + zero = (struct hashlistnode<_Key, _Val> *)ourmalloc(sizeof(struct hashlistnode<_Key, _Val>)); size++; } - zero->key=key; - zero->val=val; + zero->key = key; + zero->val = val; return; } @@ -214,7 +214,7 @@ public: } unsigned int oindex = hash_function(key) & capacitymask; - unsigned int index=oindex; + unsigned int index = oindex; do { search = &table[index]; if (!search->key) { @@ -225,7 +225,7 @@ public: return search->val; index++; index &= capacitymask; - if (index==oindex) + if (index == oindex) break; } while (true); return (_Val)0; @@ -244,9 +244,9 @@ public: if (!zero) { return (_Val)0; } else { - _Val v=zero->val; + _Val v = zero->val; ourfree(zero); - zero=NULL; + zero = NULL; size--; return v; } @@ -262,10 +262,10 @@ public: break; } else if (equals(search->key, key)) { - _Val v=search->val; + _Val v = search->val; //empty out this bin - search->val=(_Val) 1; - search->key=0; + search->val = (_Val) 1; + search->key = 0; size--; return v; } @@ -289,7 +289,7 @@ public: /* HashTable cannot handle 0 as a key */ if (!key) { - return zero!=NULL; + return zero != NULL; } unsigned int index = hash_function(key); @@ -329,7 +329,7 @@ public: struct hashlistnode<_Key, _Val> *bin = &oldtable[0]; struct hashlistnode<_Key, _Val> *lastbin = &oldtable[oldcapacity]; - for (;bin < lastbin;bin++) { + for (; bin < lastbin; bin++) { _Key key = bin->key; struct hashlistnode<_Key, _Val> *search; diff --git a/src/Collections/structs.cc b/src/Collections/structs.cc index a6e19f0..7239a7e 100644 --- a/src/Collections/structs.cc +++ b/src/Collections/structs.cc @@ -41,11 +41,11 @@ bool order_edge_equals(OrderEdge *key1, OrderEdge *key2) { return key1->sink == key2->sink && key1->source == key2->source; } -unsigned int order_element_hash_function(OrderElement* This) { +unsigned int order_element_hash_function(OrderElement *This) { return (uint)This->item; } -bool order_element_equals(OrderElement* key1, OrderElement* key2) { +bool order_element_equals(OrderElement *key1, OrderElement *key2) { return key1->item == key2->item; } diff --git a/src/Collections/structs.h b/src/Collections/structs.h index 4a882fb..28d290f 100644 --- a/src/Collections/structs.h +++ b/src/Collections/structs.h @@ -12,8 +12,8 @@ unsigned int order_node_hash_function(OrderNode *This); bool order_node_equals(OrderNode *key1, OrderNode *key2); unsigned int order_edge_hash_function(OrderEdge *This); bool order_edge_equals(OrderEdge *key1, OrderEdge *key2); -unsigned int order_element_hash_function(OrderElement* This); -bool order_element_equals(OrderElement* key1, OrderElement* key2); +unsigned int order_element_hash_function(OrderElement *This); +bool order_element_equals(OrderElement *key1, OrderElement *key2); unsigned int order_pair_hash_function(OrderPair *This); bool order_pair_equals(OrderPair *key1, OrderPair *key2); diff --git a/src/Encoders/elementencoding.h b/src/Encoders/elementencoding.h index 27ff248..1d41940 100644 --- a/src/Encoders/elementencoding.h +++ b/src/Encoders/elementencoding.h @@ -11,7 +11,7 @@ enum ElementEncodingType { typedef enum ElementEncodingType ElementEncodingType; class ElementEncoding { - public: +public: ElementEncoding(Element *element); ElementEncodingType getElementEncodingType() {return type;} ~ElementEncoding(); @@ -36,7 +36,7 @@ class ElementEncoding { return -1; } - + ElementEncodingType type; Element *element; Edge *variables;/* List Variables Used To Encode Element */ diff --git a/src/Encoders/functionencoding.h b/src/Encoders/functionencoding.h index 0919a9e..e4bd5aa 100644 --- a/src/Encoders/functionencoding.h +++ b/src/Encoders/functionencoding.h @@ -16,7 +16,7 @@ union ElementPredicate { typedef union ElementPredicate ElementPredicate; class FunctionEncoding { - public: +public: FunctionEncodingType type; bool isFunction;//true for function, false for predicate ElementPredicate op; diff --git a/src/Encoders/naiveencoder.cc b/src/Encoders/naiveencoder.cc index 35c62e8..efcb92f 100644 --- a/src/Encoders/naiveencoder.cc +++ b/src/Encoders/naiveencoder.cc @@ -14,8 +14,8 @@ #include void naiveEncodingDecision(CSolver *This) { - HSIteratorBoolean *iterator=This->getConstraints(); - while(iterator->hasNext()) { + HSIteratorBoolean *iterator = This->getConstraints(); + while (iterator->hasNext()) { Boolean *boolean = iterator->next(); naiveEncodingConstraint(boolean); } diff --git a/src/Encoders/orderencoding.h b/src/Encoders/orderencoding.h index 766245e..57409e7 100644 --- a/src/Encoders/orderencoding.h +++ b/src/Encoders/orderencoding.h @@ -9,7 +9,7 @@ enum OrderEncodingType { typedef enum OrderEncodingType OrderEncodingType; class OrderEncoding { - public: +public: OrderEncoding(Order *order); OrderEncodingType type; diff --git a/src/Test/logicopstest.cc b/src/Test/logicopstest.cc index df80fa7..7e1104d 100644 --- a/src/Test/logicopstest.cc +++ b/src/Test/logicopstest.cc @@ -13,16 +13,16 @@ int main(int numargs, char **argv) { Boolean *b3 = solver->getBooleanVar(0); Boolean *b4 = solver->getBooleanVar(0); //L_AND, L_OR, L_NOT, L_XOR, L_IMPLIES - Boolean * barray1[]={b1,b2}; + Boolean *barray1[] = {b1,b2}; Boolean *andb1b2 = solver->applyLogicalOperation(L_AND, barray1, 2); - Boolean * barray2[]={andb1b2, b3}; + Boolean *barray2[] = {andb1b2, b3}; Boolean *imply = solver->applyLogicalOperation(L_IMPLIES, barray2, 2); solver->addConstraint(imply); - Boolean * barray3[] ={b3}; + Boolean *barray3[] = {b3}; Boolean *notb3 = solver->applyLogicalOperation(L_NOT, barray3, 1); - Boolean * barray4[] ={notb3, b4}; + Boolean *barray4[] = {notb3, b4}; solver->addConstraint(solver->applyLogicalOperation(L_OR, barray4, 2)); - Boolean * barray5[] ={b1, b4}; + Boolean *barray5[] = {b1, b4}; solver->addConstraint(solver->applyLogicalOperation(L_XOR, barray5, 2)); if (solver->startEncoding() == 1) printf("b1=%d b2=%d b3=%d b4=%d\n", diff --git a/src/Test/ordergraphtest.cc b/src/Test/ordergraphtest.cc index f9f9c07..4562176 100644 --- a/src/Test/ordergraphtest.cc +++ b/src/Test/ordergraphtest.cc @@ -17,23 +17,23 @@ int main(int numargs, char **argv) { Boolean *o81 = solver->orderConstraint(order, 8, 1); /* Not Valid c++...Let Hamed fix... - addConstraint(solver, applyLogicalOperation(solver, L_OR,(Boolean *[]) {o12, o13, o24, o34}, 4) ); - Boolean *b1 = applyLogicalOperation(solver, L_XOR, (Boolean *[]) {o41, o57}, 2); - Boolean *o34n = applyLogicalOperation(solver, L_NOT, (Boolean *[]) {o34}, 1); - Boolean *o24n = applyLogicalOperation(solver, L_NOT, (Boolean *[]) {o24}, 1); - Boolean *b2 = applyLogicalOperation(solver, L_OR, (Boolean *[]) {o34n, o24n}, 2); - addConstraint(solver, applyLogicalOperation(solver, L_IMPLIES,(Boolean *[]) {b1, b2}, 2) ); - addConstraint(solver, applyLogicalOperation(solver, L_AND,(Boolean *[]) {o12, o13}, 2) ); - addConstraint(solver, applyLogicalOperation(solver, L_OR,(Boolean *[]) {o76, o65}, 2) ); - Boolean* b3= applyLogicalOperation(solver, L_AND,(Boolean *[]) {o76, o65}, 2) ; - Boolean* o57n= applyLogicalOperation(solver, L_NOT,(Boolean *[]) {o57}, 1); - addConstraint(solver, applyLogicalOperation(solver, L_IMPLIES,(Boolean *[]) {b3, o57n}, 2) ); - addConstraint(solver, applyLogicalOperation(solver, L_AND,(Boolean *[]) {o58, o81}, 2) ); - - if (solver->startEncoding() == 1) - printf("SAT\n"); - else - printf("UNSAT\n"); - */ + addConstraint(solver, applyLogicalOperation(solver, L_OR,(Boolean *[]) {o12, o13, o24, o34}, 4) ); + Boolean *b1 = applyLogicalOperation(solver, L_XOR, (Boolean *[]) {o41, o57}, 2); + Boolean *o34n = applyLogicalOperation(solver, L_NOT, (Boolean *[]) {o34}, 1); + Boolean *o24n = applyLogicalOperation(solver, L_NOT, (Boolean *[]) {o24}, 1); + Boolean *b2 = applyLogicalOperation(solver, L_OR, (Boolean *[]) {o34n, o24n}, 2); + addConstraint(solver, applyLogicalOperation(solver, L_IMPLIES,(Boolean *[]) {b1, b2}, 2) ); + addConstraint(solver, applyLogicalOperation(solver, L_AND,(Boolean *[]) {o12, o13}, 2) ); + addConstraint(solver, applyLogicalOperation(solver, L_OR,(Boolean *[]) {o76, o65}, 2) ); + Boolean* b3= applyLogicalOperation(solver, L_AND,(Boolean *[]) {o76, o65}, 2) ; + Boolean* o57n= applyLogicalOperation(solver, L_NOT,(Boolean *[]) {o57}, 1); + addConstraint(solver, applyLogicalOperation(solver, L_IMPLIES,(Boolean *[]) {b3, o57n}, 2) ); + addConstraint(solver, applyLogicalOperation(solver, L_AND,(Boolean *[]) {o58, o81}, 2) ); + + if (solver->startEncoding() == 1) + printf("SAT\n"); + else + printf("UNSAT\n"); + */ delete solver; } diff --git a/src/Test/tablefuncencodetest.cc b/src/Test/tablefuncencodetest.cc index 354b5ef..f0610e4 100644 --- a/src/Test/tablefuncencodetest.cc +++ b/src/Test/tablefuncencodetest.cc @@ -41,7 +41,7 @@ int main(int numargs, char **argv) { solver->addTableEntry(t1, row5, 2, 3); solver->addTableEntry(t1, row6, 2, 5); Function *f1 = solver->completeTable(t1, FLAGIFFUNDEFINED); - Element * tmparray[]={e1, e2}; + Element *tmparray[] = {e1, e2}; Element *e3 = solver->applyFunction(f1, tmparray, 2, overflow); Set *deq[] = {s3,s2}; diff --git a/src/Test/tablepredicencodetest.cc b/src/Test/tablepredicencodetest.cc index 77ae0af..d1e45de 100644 --- a/src/Test/tablepredicencodetest.cc +++ b/src/Test/tablepredicencodetest.cc @@ -42,7 +42,7 @@ int main(int numargs, char **argv) { solver->addTableEntry(t1, row6, 3, true); Predicate *p1 = solver->createPredicateTable(t1, FLAGIFFUNDEFINED); Boolean *undef = solver->getBooleanVar(2); - Element * tmparray[] = {e1, e2, e3}; + Element *tmparray[] = {e1, e2, e3}; Boolean *b1 = solver->applyPredicateTable(p1, tmparray, 3, undef); solver->addConstraint(b1); @@ -54,7 +54,7 @@ int main(int numargs, char **argv) { Set *d1[] = {s1, s2}; Predicate *eq = solver->createPredicateOperator(EQUALS, d1, 2); - Element * tmparray2[] = {e1, e2}; + Element *tmparray2[] = {e1, e2}; Boolean *pred2 = solver->applyPredicate(eq, tmparray2, 2); solver->addConstraint(pred2); diff --git a/src/Tuner/tunable.cc b/src/Tuner/tunable.cc index f994242..5c13a12 100644 --- a/src/Tuner/tunable.cc +++ b/src/Tuner/tunable.cc @@ -3,9 +3,9 @@ Tuner::Tuner() { } -int Tuner::getTunable(TunableParam param, TunableDesc * descriptor) { +int Tuner::getTunable(TunableParam param, TunableDesc *descriptor) { return descriptor->defaultValue; } -int Tuner::getVarTunable(VarType vartype, TunableParam param, TunableDesc * descriptor) { +int Tuner::getVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor) { return descriptor->defaultValue; } diff --git a/src/Tuner/tunable.h b/src/Tuner/tunable.h index 5816d7e..6077891 100644 --- a/src/Tuner/tunable.h +++ b/src/Tuner/tunable.h @@ -4,16 +4,16 @@ class Tuner { - public: +public: Tuner(); - int getTunable(TunableParam param, TunableDesc * descriptor); - int getVarTunable(VarType vartype, TunableParam param, TunableDesc * descriptor); + int getTunable(TunableParam param, TunableDesc *descriptor); + int getVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor); MEMALLOC; }; class TunableDesc { - public: - TunableDesc(int _lowValue, int _highValue, int _defaultValue) : lowValue(_lowValue), highValue(_highValue), defaultValue(_defaultValue) {} +public: + TunableDesc(int _lowValue, int _highValue, int _defaultValue) : lowValue(_lowValue), highValue(_highValue), defaultValue(_defaultValue) {} int lowValue; int highValue; int defaultValue; diff --git a/src/csolver.cc b/src/csolver.cc index d4d39c0..d825df5 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -161,7 +161,7 @@ Boolean *CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, ui } Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) { - Boolean * boolean=new BooleanLogic(this, op, array, asize); + Boolean *boolean = new BooleanLogic(this, op, array, asize); allBooleans.push(boolean); return boolean; } diff --git a/src/csolver.h b/src/csolver.h index aaf3b30..c1fd90b 100644 --- a/src/csolver.h +++ b/src/csolver.h @@ -5,19 +5,19 @@ #include "structs.h" class CSolver { - public: +public: CSolver(); ~CSolver(); - + /** This function creates a set containing the elements passed in the array. */ Set *createSet(VarType type, uint64_t *elements, uint num); /** This function creates a set from lowrange to highrange (inclusive). */ Set *createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange); - + /** This function creates a mutable set. */ - + MutableSet *createMutableSet(VarType type); /** This function adds a new item to a set. */ @@ -25,9 +25,9 @@ class CSolver { void addItem(MutableSet *set, uint64_t element); /** This function adds a new unique item to the set and returns it. - This function cannot be used in conjunction with manually adding - items to the set. */ - + This function cannot be used in conjunction with manually adding + items to the set. */ + uint64_t createUniqueItem(MutableSet *set); /** This function creates an element variable over a set. */ @@ -80,7 +80,7 @@ class CSolver { Boolean *applyLogicalOperation(LogicOp op, Boolean **array, uint asize); /** This function adds a boolean constraint to the set of constraints - to be satisfied */ + to be satisfied */ void addConstraint(Boolean *constraint); @@ -105,22 +105,22 @@ class CSolver { bool isUnSAT() { return unsat; } - Vector * getOrders() { return & allOrders;} + Vector *getOrders() { return &allOrders;} - Tuner * getTuner() { return tuner; } + Tuner *getTuner() { return tuner; } - HSIteratorBoolean * getConstraints() { return constraints.iterator(); } + HSIteratorBoolean *getConstraints() { return constraints.iterator(); } - SATEncoder * getSATEncoder() {return satEncoder;} + SATEncoder *getSATEncoder() {return satEncoder;} void replaceBooleanWithTrue(Boolean *bexpr); void replaceBooleanWithFalse(Boolean *bexpr); void replaceBooleanWithBoolean(Boolean *oldb, Boolean *newb); - + MEMALLOC; - private: +private: void handleXORFalse(BooleanLogic *bexpr, Boolean *child); void handleIMPLIESTrue(BooleanLogic *bexpr, Boolean *child); void handleIMPLIESFalse(BooleanLogic *bexpr, Boolean *child); diff --git a/src/mymemory.h b/src/mymemory.h index f5d54d9..294985d 100644 --- a/src/mymemory.h +++ b/src/mymemory.h @@ -31,21 +31,21 @@ static inline void ourfree(void *ptr) { free(ptr); } static inline void *ourcalloc(size_t count, size_t size) { return calloc(count, size); } static inline void *ourrealloc(void *ptr, size_t size) { return realloc(ptr, size); } -#define MEMALLOC \ - void * operator new(size_t size) { \ - return ourmalloc(size); \ - } \ - void operator delete(void *p, size_t size) { \ - ourfree(p); \ - } \ - void * operator new[](size_t size) { \ - return ourmalloc(size); \ - } \ - void operator delete[](void *p, size_t size) { \ - ourfree(p); \ - } \ - void * operator new(size_t size, void *p) { /* placement new */ \ - return p; \ +#define MEMALLOC \ + void *operator new(size_t size) { \ + return ourmalloc(size); \ + } \ + void operator delete(void *p, size_t size) { \ + ourfree(p); \ + } \ + void *operator new[](size_t size) { \ + return ourmalloc(size); \ + } \ + void operator delete[](void *p, size_t size) { \ + ourfree(p); \ + } \ + void *operator new(size_t size, void *p) { /* placement new */ \ + return p; \ } #endif/* _MY_MEMORY_H */ -- 2.34.1