Run tabbing pass
authorbdemsky <bdemsky@uci.edu>
Sun, 27 Aug 2017 01:11:20 +0000 (18:11 -0700)
committerbdemsky <bdemsky@uci.edu>
Sun, 27 Aug 2017 01:11:20 +0000 (18:11 -0700)
52 files changed:
src/AST/astnode.h
src/AST/boolean.h
src/AST/element.cc
src/AST/element.h
src/AST/function.h
src/AST/mutableset.h
src/AST/order.h
src/AST/predicate.cc
src/AST/predicate.h
src/AST/rewriter.cc
src/AST/set.h
src/AST/table.cc
src/AST/table.h
src/ASTAnalyses/orderedge.h
src/ASTAnalyses/orderencoder.cc
src/ASTAnalyses/orderencoder.h
src/ASTAnalyses/ordergraph.h
src/ASTAnalyses/ordernode.h
src/ASTAnalyses/polarityassignment.cc
src/ASTTransform/integerencoding.cc
src/ASTTransform/integerencoding.h
src/ASTTransform/orderdecompose.cc
src/ASTTransform/orderdecompose.h
src/Backend/constraint.cc
src/Backend/orderelement.cc
src/Backend/orderelement.h
src/Backend/orderpair.h
src/Backend/satencoder.cc
src/Backend/satfuncopencoder.cc
src/Backend/satfunctableencoder.cc
src/Backend/satorderencoder.cc
src/Backend/satorderencoder.h
src/Backend/sattranslator.h
src/Collections/array.h
src/Collections/cppvector.h
src/Collections/hashset.h
src/Collections/hashtable.h
src/Collections/structs.cc
src/Collections/structs.h
src/Encoders/elementencoding.h
src/Encoders/functionencoding.h
src/Encoders/naiveencoder.cc
src/Encoders/orderencoding.h
src/Test/logicopstest.cc
src/Test/ordergraphtest.cc
src/Test/tablefuncencodetest.cc
src/Test/tablepredicencodetest.cc
src/Tuner/tunable.cc
src/Tuner/tunable.h
src/csolver.cc
src/csolver.h
src/mymemory.h

index 8cc126a..749bf8e 100644 (file)
@@ -4,8 +4,8 @@
 #include "ops.h"
 
 class ASTNode {
- public:
-  ASTNode(ASTNodeType _type) : type(_type) {}
+public:
+       ASTNode(ASTNodeType _type) : type(_type) {}
        ASTNodeType type;
        MEMALLOC;
 };
index 4bab811..c9722a9 100644 (file)
@@ -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<Element *> 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<Boolean *> inputs;
index be4f77b..32b372a 100644 (file)
@@ -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);
 }
 
index 6a8ea95..f563586 100644 (file)
@@ -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<ASTNode *> 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;
index 9b6f254..2cd5cca 100644 (file)
@@ -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<Set *> 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);
index b0359d3..3c2f937 100644 (file)
@@ -3,7 +3,7 @@
 #include "set.h"
 
 class MutableSet : public Set {
- public:
+public:
        MutableSet(VarType t);
        void addElementMSet(uint64_t element);
        MEMALLOC;
index 1645786..8d21240 100644 (file)
@@ -9,13 +9,13 @@
 #include "orderpair.h"
 
 class Order {
- public:
+public:
        Order(OrderType type, Set *set);
        ~Order();
        OrderType type;
        Set *set;
        HashTableOrderPair *orderPairTable;
-       HashSetOrderElementelementTable;
+       HashSetOrderElement *elementTable;
        OrderGraph *graph;
        Vector<BooleanOrder *> constraints;
        OrderEncoding order;
index feff67a..0e04668 100644 (file)
@@ -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) {
index 96f462d..46bc5af 100644 (file)
@@ -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;
index e8e9c84..f32fc91 100644 (file)
@@ -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);
index 9303fa8..bb246b6 100644 (file)
@@ -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
index 016b3cc..d54aefb 100644 (file)
@@ -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);
index f232615..28b13e4 100644 (file)
@@ -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);
index 7063f34..9b1af29 100644 (file)
@@ -11,7 +11,7 @@
 #include "mymemory.h"
 
 class OrderEdge {
- public:
+public:
        OrderEdge(OrderNode *begin, OrderNode *end);
 
        OrderNode *source;
index 10adc81..5d94206 100644 (file)
@@ -46,8 +46,8 @@ void DFSNodeVisit(OrderNode *node, Vector<OrderNode *> *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){
-       HSIteratorOrderEdgeiterator = node->inEdges.iterator();
-       while(iterator->hasNext()){
-               OrderEdgeedge = 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()){
-               OrderEdgeedge = 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){
-       HSIteratorOrderEdgeiterin = node->inEdges.iterator();
-       while(iterin->hasNext()){
-               OrderEdgeinEdge = iterin->next();
-               OrderNodesrcNode = 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);
-               HSIteratorOrderEdgeiterout = node->outEdges.iterator();
-               while(iterout->hasNext()){
-                       OrderEdgeoutEdge = iterout->next();
-                       OrderNodesinkNode = 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) {
-       HSIteratorOrderNodeiterator = graph->getNodes();
-       while(iterator->hasNext()) {
-               OrderNodenode = 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<OrderNode *> finishNodes;
@@ -146,14 +146,14 @@ void completePartialOrderGraph(OrderGraph *graph) {
        HashTableNodeToNodeSet *table = new HashTableNodeToNodeSet(128, 0.25);
 
        Vector<OrderNode *> 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, Vector<OrderNode
                }
                {
                        //Use source sets to compute mustPos edges
-                       HSIteratorOrderEdge *iterator =node->inEdges.iterator();
+                       HSIteratorOrderEdge *iterator = node->inEdges.iterator();
                        while (iterator->hasNext()) {
                                OrderEdge *edge = iterator->next();
                                OrderNode *parent = edge->source;
@@ -303,7 +303,7 @@ void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode
    must be true because of transitivity from other must be true
    edges. */
 
-void reachMustAnalysis(CSolver * solver, OrderGraph *graph, bool computeTransitiveClosure) {
+void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure) {
        Vector<OrderNode *> finishNodes;
        //Topologically sort the mustPos edge graph
        DFSMust(graph, &finishNodes);
index 19240cf..57a6e5c 100644 (file)
@@ -18,8 +18,8 @@ void DFS(OrderGraph *graph, Vector<OrderNode *> *finishNodes);
 void DFSReverse(OrderGraph *graph, Vector<OrderNode *> *finishNodes);
 void completePartialOrderGraph(OrderGraph *graph);
 void resetNodeInfoStatusSCC(OrderGraph *graph);
-bool isMustBeTrueNode(OrderNodenode);
-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<OrderNode *> *finishNodes);
index 8dd2e65..eb756a8 100644 (file)
@@ -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;
index a63dd7f..36bb3df 100644 (file)
@@ -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);
index 947f28e..705f5d9 100644 (file)
@@ -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);
index 4fe381a..0a415b9 100644 (file)
@@ -9,29 +9,29 @@
 #include "set.h"
 
 
-void orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder){
-       Orderorder = 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) {
-       HashSetOrderElementeset = order->elementTable;
+Element *getOrderIntegerElement(SATEncoder *This,Order *order, uint64_t item) {
+       HashSetOrderElement *eset = order->elementTable;
        OrderElement oelement(item, NULL);
-       if( !eset->contains(&oelement)){
-               Setset = This->solver->createRangeSet(order->set->type, 1, (uint64_t) order->set->getSize());
-               Elementelem = 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
index 9b5a808..15fbdd7 100644 (file)
@@ -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 */
 
index 4962046..18602cc 100644 (file)
 #include "integerencoding.h"
 
 void orderAnalysis(CSolver *This) {
-       Vector<Order *> * orders=This->getOrders();
+       Vector<Order *> *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; i<size; i++){
-                       orderIntegerEncodingSATEncoder(This->satEncoder, 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; i<size; i++){
+                  orderIntegerEncodingSATEncoder(This->satEncoder, 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;i<pcvsize;i++) {
-               Order * neworder=partialcandidatevec.get(i);
-               if (neworder != NULL){
+       uint pcvsize = partialcandidatevec.getSize();
+       for (uint i = 0; i < pcvsize; i++) {
+               Order *neworder = partialcandidatevec.get(i);
+               if (neworder != NULL) {
                        neworder->type = TOTAL;
                        model_print("i=%u\t", i);
                }
index b88fded..85a5481 100644 (file)
@@ -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 */
 
index df812df..1c36cd1 100644 (file)
@@ -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;
 }
index 01d0ada..679a656 100644 (file)
@@ -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;
 }
index 7199405..a5f08a3 100644 (file)
 #include "constraint.h"
 
 class OrderElement {
- public:
-       OrderElement(uint64_t item, Elementelem);
+public:
+       OrderElement(uint64_t item, Element *elem);
        uint64_t item;
-       Elementelem;
+       Element *elem;
        MEMALLOC;
 };
 
index b34ea1a..6fc5df1 100644 (file)
 #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;
index 91e323d..3dd9933 100644 (file)
@@ -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;
index 7f7341a..695493b 100644 (file)
@@ -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);
 }
index 0efe02c..27cf8c7 100644 (file)
@@ -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<Element*> * inputs = &constraint->inputs;
+       Array<Element *> *inputs = &constraint->inputs;
        uint inputNum = inputs->getSize();
        uint size = table->entries->getSize();
        bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
index 640ac1a..5744736 100644 (file)
 
 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);
index 9b143d9..ca6b4d4 100644 (file)
@@ -2,7 +2,7 @@
 #define SATORDERENCODER_H
 
 Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint);
-Edge inferOrderConstraintFromGraph(Orderorder, 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);
index be5c8c0..1d9964f 100644 (file)
@@ -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);
index 6197de7..496bdc6 100644 (file)
@@ -3,49 +3,49 @@
 
 template<typename type>
 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;
 };
 
 
index a10403e..377ffe4 100644 (file)
@@ -6,80 +6,80 @@
 
 template<typename type>
 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;
index b0b987a..6a823f5 100644 (file)
@@ -24,14 +24,14 @@ class HashSet;
 template<typename _Key, typename _KeyInt, int _Shift, unsigned int (*hash_function)(_Key) = default_hash_function<_Key, _Shift, _KeyInt>, 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<typename _Key, typename _KeyInt, int _Shift = 0, unsigned int (*hash_function)(_Key) = default_hash_function<_Key, _Shift, _KeyInt>, 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;
 };
index c33fe60..528f5f2 100644 (file)
@@ -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<capacity;i++) {
+               for (unsigned int i = 0; i < capacity; i++) {
                        struct hashlistnode<_Key, _Val> *bin = &table[i];
                        if (bin->key != NULL) {
                                bin->key = NULL;
@@ -136,7 +136,7 @@ public:
        }
 
        void resetandfree() {
-               for(unsigned int i=0;i<capacity;i++) {
+               for (unsigned int i = 0; i < capacity; i++) {
                        struct hashlistnode<_Key, _Val> *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;
index a6e19f0..7239a7e 100644 (file)
@@ -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(OrderElementThis) {
+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;
 }
 
index 4a882fb..28d290f 100644 (file)
@@ -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(OrderElementThis);
-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);
 
index 27ff248..1d41940 100644 (file)
@@ -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 */
index 0919a9e..e4bd5aa 100644 (file)
@@ -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;
index 35c62e8..efcb92f 100644 (file)
@@ -14,8 +14,8 @@
 #include <strings.h>
 
 void naiveEncodingDecision(CSolver *This) {
-       HSIteratorBoolean *iterator=This->getConstraints();
-       while(iterator->hasNext()) {
+       HSIteratorBoolean *iterator = This->getConstraints();
+       while (iterator->hasNext()) {
                Boolean *boolean = iterator->next();
                naiveEncodingConstraint(boolean);
        }
index 766245e..57409e7 100644 (file)
@@ -9,7 +9,7 @@ enum OrderEncodingType {
 typedef enum OrderEncodingType OrderEncodingType;
 
 class OrderEncoding {
- public:
+public:
        OrderEncoding(Order *order);
 
        OrderEncodingType type;
index df80fa7..7e1104d 100644 (file)
@@ -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",
index f9f9c07..4562176 100644 (file)
@@ -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;
 }
index 354b5ef..f0610e4 100644 (file)
@@ -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};
index 77ae0af..d1e45de 100644 (file)
@@ -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);
 
index f994242..5c13a12 100644 (file)
@@ -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;
 }
index 5816d7e..6077891 100644 (file)
@@ -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;
index d4d39c0..d825df5 100644 (file)
@@ -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;
 }
index aaf3b30..c1fd90b 100644 (file)
@@ -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<Order *> * getOrders() { return & allOrders;}
+       Vector<Order *> *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);
index f5d54d9..294985d 100644 (file)
@@ -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 */