Fix tabbing

diff --git a/src/AST/element.cc b/src/AST/element.cc
index d8072315ca3a04e8f44a7fe0ee78ddc6aa852716..f182cd2c471def656f480f29c04361f1dde0a001 100644 (file)
--- a/src/AST/element.cc
+++ b/src/AST/element.cc
@@ -9,7 +9,7 @@
 Element::Element(ASTNodeType _type) :
        ASTNode(_type),
        encoding(this),
-       anyValue(false){
+       anyValue(false) {
 }
 
 ElementSet::ElementSet(Set *s) :
@@ -36,7 +36,7 @@ ElementConst::ElementConst(uint64_t _value, Set *_set) :
 }
 
 Element *ElementConst::clone(CSolver *solver, CloneMap *map) {
-       Element* e= solver->getElementConst(type, value);
+       Element *e = solver->getElementConst(type, value);
        e->anyValue = anyValue;
        return e;
 }

diff --git a/src/AST/element.h b/src/AST/element.h
index a7217b5a44052999119debc7cb2c0b3c3dae0e06..91d677fc2b8726ff67aedcbda69338ac2b35c6ad 100644 (file)
--- a/src/AST/element.h
+++ b/src/AST/element.h
@@ -21,7 +21,7 @@ public:
        virtual void updateParents() {}
        virtual Set *getRange() = 0;
        CMEMALLOC;
-        bool anyValue;
+       bool anyValue;
 };
 
 class ElementSet : public Element {

diff --git a/src/ASTAnalyses/Encoding/encodinggraph.cc b/src/ASTAnalyses/Encoding/encodinggraph.cc
index 8029049c5a165710238b2083d96b65dd7c699546..2ac69c1de22ddbedb684e04eb44cc51cc76e61f4 100644 (file)
--- a/src/ASTAnalyses/Encoding/encodinggraph.cc
+++ b/src/ASTAnalyses/Encoding/encodinggraph.cc
@@ -54,32 +54,32 @@ void EncodingGraph::buildGraph() {
 
 
 void EncodingGraph::validate() {
-       SetIteratorBooleanEdge* it= solver->getConstraints();
-       while(it->hasNext()){
+       SetIteratorBooleanEdge *it = solver->getConstraints();
+       while (it->hasNext()) {
                BooleanEdge be = it->next();
-               if(be->type == PREDICATEOP){
+               if (be->type == PREDICATEOP) {
                        BooleanPredicate *b = (BooleanPredicate *)be.getBoolean();
-                       if(b->predicate->type == OPERATORPRED){
-                               PredicateOperator* predicate = (PredicateOperator*) b->predicate;
-                               if(predicate->getOp() == SATC_EQUALS){
+                       if (b->predicate->type == OPERATORPRED) {
+                               PredicateOperator *predicate = (PredicateOperator *) b->predicate;
+                               if (predicate->getOp() == SATC_EQUALS) {
                                        ASSERT(b->inputs.getSize() == 2);
-                                       Element* e1= b->inputs.get(0);
-                                       Element* e2= b->inputs.get(1);
-                                       if(e1->type == ELEMCONST || e1->type == ELEMCONST)
+                                       Element *e1 = b->inputs.get(0);
+                                       Element *e2 = b->inputs.get(1);
+                                       if (e1->type == ELEMCONST || e1->type == ELEMCONST)
                                                continue;
                                        ElementEncoding *enc1 = e1->getElementEncoding();
                                        ElementEncoding *enc2 = e2->getElementEncoding();
                                        ASSERT(enc1->getElementEncodingType() != ELEM_UNASSIGNED);
                                        ASSERT(enc2->getElementEncodingType() != ELEM_UNASSIGNED);
-                                       if(enc1->getElementEncodingType() == enc2->getElementEncodingType() && enc1->getElementEncodingType() == BINARYINDEX && b->getFunctionEncoding()->type == CIRCUIT){
-                                               for(uint i=0; i<enc1->encArraySize; i++){
-                                                       if(enc1->isinUseElement(i)){
+                                       if (enc1->getElementEncodingType() == enc2->getElementEncodingType() && enc1->getElementEncodingType() == BINARYINDEX && b->getFunctionEncoding()->type == CIRCUIT) {
+                                               for (uint i = 0; i < enc1->encArraySize; i++) {
+                                                       if (enc1->isinUseElement(i)) {
                                                                uint64_t val1 = enc1->encodingArray[i];
-                                                               if(enc2->isinUseElement(i)){
+                                                               if (enc2->isinUseElement(i)) {
                                                                        ASSERT(val1 == enc2->encodingArray[i]);
-                                                               }else{
-                                                                       for(uint j=0; j< enc2->encArraySize; j++){
-                                                                               if(enc2->isinUseElement(j)){
+                                                               } else {
+                                                                       for (uint j = 0; j < enc2->encArraySize; j++) {
+                                                                               if (enc2->isinUseElement(j)) {
                                                                                        ASSERT(val1 != enc2->encodingArray[j]);
                                                                                }
                                                                        }
@@ -88,15 +88,15 @@ void EncodingGraph::validate() {
                                                }
                                        }
                                        //Now make sure that all the elements in the set are appeared in the encoding array!
-                                       for(uint k=0; k< b->inputs.getSize(); k++){
+                                       for (uint k = 0; k < b->inputs.getSize(); k++) {
                                                Element *e = b->inputs.get(k);
                                                ElementEncoding *enc = e->getElementEncoding();
                                                Set *s = e->getRange();
                                                for (uint i = 0; i < s->getSize(); i++) {
                                                        uint64_t value = s->getElement(i);
-                                                       bool exist=false;
-                                                       for(uint j=0; j< enc->encArraySize; j++){
-                                                               if(enc->isinUseElement(j) && enc->encodingArray[j] == value){
+                                                       bool exist = false;
+                                                       for (uint j = 0; j < enc->encArraySize; j++) {
+                                                               if (enc->isinUseElement(j) && enc->encodingArray[j] == value) {
                                                                        exist = true;
                                                                        break;
                                                                }
@@ -155,7 +155,7 @@ void EncodingGraph::encode() {
                                                ASSERT(encoding->isinUseElement(encodingIndex));
                                                encoding->encodingArray[encodingIndex] = value;
                                        }
-                               } else{
+                               } else {
                                        model_print("DAMN in encode()\n");
                                        e->print();
                                }
@@ -207,7 +207,7 @@ void EncodingGraph::mergeNodes(EncodingNode *first, EncodingNode *second) {
                first->setEncoding(BINARYINDEX);
        if (graph2 == NULL)
                second->setEncoding(BINARYINDEX);
-       
+
        if (graph1 == NULL && graph2 == NULL) {
                graph1 = new EncodingSubGraph();
                subgraphs.add(graph1);
@@ -334,14 +334,14 @@ void EncodingGraph::decideEdges() {
                        EncodingSubGraph *tmpsg = leftGraph; leftGraph = rightGraph; rightGraph = tmpsg;
                }
                //model_print("Right=%p RGraph=%p\tLeft=%p LGraph=%p\n", right, rightGraph, left, leftGraph);
-               uint leftSize = 0, rightSize = 0, newSize = 0, max=0;
+               uint leftSize = 0, rightSize = 0, newSize = 0, max = 0;
                uint64_t totalCost = 0;
                bool merge = false;
 //             model_print("**************decideEdge*************\n");
 //             model_print("LeftNode Size = %u\n", left->getSize());
 //             model_print("rightNode Size = %u\n", right->getSize());
 //             model_print("UnionSize = %u\n", left->s->getUnionSize(right->s));
-                       
+
                if (leftGraph == NULL && rightGraph == NULL) {
                        leftSize = convertSize(left->getSize());
                        rightSize = convertSize(right->getSize());
@@ -351,8 +351,8 @@ void EncodingGraph::decideEdges() {
                        totalCost = (newSize - leftSize) * left->elements.getSize() +
                                                                        (newSize - rightSize) * right->elements.getSize();
                        //model_print("leftSize=%u\trighSize=%u\tnewSize=%u\n", leftSize, rightSize, newSize);
-                       max = rightSize > leftSize? rightSize : leftSize;
-                       if(newSize == max){
+                       max = rightSize > leftSize ? rightSize : leftSize;
+                       if (newSize == max) {
                                merge = true;
                        }
                } else if (leftGraph != NULL && rightGraph == NULL) {
@@ -364,8 +364,8 @@ void EncodingGraph::decideEdges() {
                        totalCost = (newSize - leftSize) * leftGraph->numElements +
                                                                        (newSize - rightSize) * right->elements.getSize();
                        //model_print("leftSize=%u\trighSize=%u\tnewSize=%u\n", leftSize, rightSize, newSize);
-                       max = rightSize > leftSize? rightSize : leftSize;
-                       if(newSize == max){
+                       max = rightSize > leftSize ? rightSize : leftSize;
+                       if (newSize == max) {
                                merge = true;
                        }
                } else {
@@ -380,7 +380,7 @@ void EncodingGraph::decideEdges() {
 //                     model_print("LeftGraph size=%u\n", leftGraph->encodingSize);
 //                     model_print("RightGraph size=%u\n", rightGraph->encodingSize);
 //                     model_print("UnionGraph size = %u\n", leftGraph->estimateNewSize(rightGraph));
-                       if(rightSize < 64 && leftSize < 64){
+                       if (rightSize < 64 && leftSize < 64) {
                                merge = true;
                        }
                }

diff --git a/src/ASTAnalyses/Encoding/encodinggraph.h b/src/ASTAnalyses/Encoding/encodinggraph.h
index f3d58a220155d2153ea01b0d927e6d7eea7c31ba..d284d2149bf3b53e914587d956a64e20c3f1806e 100644 (file)
--- a/src/ASTAnalyses/Encoding/encodinggraph.h
+++ b/src/ASTAnalyses/Encoding/encodinggraph.h
@@ -4,7 +4,7 @@
 #include "structs.h"
 #include "graphstructs.h"
 
-#define FUDGEFACTOR 1.2 
+#define FUDGEFACTOR 1.2
 #define CONVERSIONFACTOR  0.5
 
 class EncodingGraph {

diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc
index 919d7f4e7165b3a9b6a1a6a2e18cdd4def1838da..98036a7997049100fb7a4eea058a413caab66384 100644 (file)
--- a/src/Backend/constraint.cc
+++ b/src/Backend/constraint.cc
@@ -573,7 +573,7 @@ Edge simplifyCNF(CNF *cnf, Edge input) {
        }
 }
 
-void addClause(CNF *cnf, uint numliterals, int *literals){
+void addClause(CNF *cnf, uint numliterals, int *literals) {
        cnf->clausecount++;
        addArrayClauseLiteral(cnf->solver, numliterals, literals);
 }

diff --git a/src/Backend/constraint.h b/src/Backend/constraint.h
index 18164f535afd4e659f52758d3dc9be98de5eba11..8d2666ca2e17464c8023fccbc3a5ac5c6e594228 100644 (file)
--- a/src/Backend/constraint.h
+++ b/src/Backend/constraint.h
@@ -46,7 +46,7 @@ typedef struct Node Node;
 
 struct CNF {
        uint varcount;
-        uint clausecount;
+       uint clausecount;
        uint asize;
        IncrementalSolver *solver;
        int *array;

diff --git a/src/Encoders/elementencoding.h b/src/Encoders/elementencoding.h
index ac6e6bf5a4626903e3a12fd3e43a82214ec0779f..ff069ecffccb4dcac3587469f6fc70a3fa5b0974 100644 (file)
--- a/src/Encoders/elementencoding.h
+++ b/src/Encoders/elementencoding.h
@@ -54,7 +54,7 @@ public:
                };
        };
        uint numVars;   /* Number of variables */
-        CMEMALLOC;
+       CMEMALLOC;
 };
 
 

diff --git a/src/Encoders/naiveencoder.cc b/src/Encoders/naiveencoder.cc
index f5aa44b955e0c67837f089d4d82d40d4b62a6445..0de7043b2d51472cc58089b1e5fa9bbe44015bfe 100644 (file)
--- a/src/Encoders/naiveencoder.cc
+++ b/src/Encoders/naiveencoder.cc
@@ -65,7 +65,7 @@ void naiveEncodingPredicate(BooleanPredicate *This) {
 void naiveEncodingElement(Element *This) {
        ElementEncoding *encoding = This->getElementEncoding();
        if (encoding->getElementEncodingType() == ELEM_UNASSIGNED) {
-               if(This->type != ELEMCONST){
+               if (This->type != ELEMCONST) {
                        model_print("INFO: naive encoder is making the decision about element %p....\n", This);
                }
                encoding->setElementEncodingType(UNARY);

diff --git a/src/Tuner/autotuner.cc b/src/Tuner/autotuner.cc
index 29c3289ec2d371f71f9e47f0ea2745e8ee71e023..d31a72f1e024733dc03d801ba221a59cc0fd46c2 100644 (file)
--- a/src/Tuner/autotuner.cc
+++ b/src/Tuner/autotuner.cc
@@ -21,7 +21,7 @@ int solve(CSolver *solver)
        try{
                return solver->solve();
        }
-       catch(std::runtime_error& e) {
+       catch (std::runtime_error &e) {
                return UNSETVALUE;
        }
 }
@@ -33,16 +33,16 @@ int solveWrapper(CSolver *solver)
        int retValue;
 
        std::thread t([&cv, &retValue, solver]()
-       {
-               retValue = solve(solver);
-               cv.notify_one();
-       });
+               {
+                                                               retValue = solve(solver);
+                                                               cv.notify_one();
+               });
 
        t.detach();
 
        {
                std::unique_lock<std::mutex> l(m);
-               if(cv.wait_for(l, TIMEOUT) == std::cv_status::timeout)
+               if (cv.wait_for(l, TIMEOUT) == std::cv_status::timeout)
                        throw std::runtime_error("Timeout");
        }
 
@@ -73,11 +73,11 @@ long long AutoTuner::evaluate(CSolver *problem, SearchTuner *tuner) {
                }
                metric = copy->getElapsedTime();
        }
-       catch(std::runtime_error& e) {
+       catch (std::runtime_error &e) {
                metric = POSINFINITY;
                model_print("TimeOut has hit\n");
        }
-       
+
        delete copy;
        return metric;
 }

diff --git a/src/Tuner/searchtuner.cc b/src/Tuner/searchtuner.cc
index 3486a9c737eab26ca7b120df730d389857fa8b64..e9de49f4a8c799f99cd819b7f939486e4b83a14f 100644 (file)
--- a/src/Tuner/searchtuner.cc
+++ b/src/Tuner/searchtuner.cc
@@ -62,18 +62,18 @@ bool tunableSettingEquals(TunableSetting *setting1, TunableSetting *setting2) {
                                 setting1->param == setting2->param;
 }
 
-ostream& operator<<(ostream& os, const TunableSetting& ts)  
-{  
-    os << ts.hasVar <<" " << ts.type1 <<" " << ts.type2 << " " << ts.param << " " << ts.lowValue <<" " 
-            << ts.highValue << " " << ts.defaultValue << " " << ts.selectedValue;  
-    return os;  
-}  
+ostream &operator<<(ostream &os, const TunableSetting &ts)
+{
+       os << ts.hasVar << " " << ts.type1 << " " << ts.type2 << " " << ts.param << " " << ts.lowValue << " "
+                << ts.highValue << " " << ts.defaultValue << " " << ts.selectedValue;
+       return os;
+}
 
 
 SearchTuner::SearchTuner() {
        ifstream myfile;
        myfile.open (TUNEFILE, ios::in);
-       if(myfile.is_open()){
+       if (myfile.is_open()) {
                bool hasVar;
                VarType type1;
                VarType type2;
@@ -82,12 +82,12 @@ SearchTuner::SearchTuner() {
                int highValue;
                int defaultValue;
                int selectedValue;
-               while(myfile >> hasVar >> type1 >> type2 >> param >> lowValue >> highValue >> defaultValue >> selectedValue){
+               while (myfile >> hasVar >> type1 >> type2 >> param >> lowValue >> highValue >> defaultValue >> selectedValue) {
                        TunableSetting *setting;
-                       
-                       if(hasVar){
+
+                       if (hasVar) {
                                setting = new TunableSetting(type1, type2, param);
-                       }else{
+                       } else {
                                setting = new TunableSetting(param);
                        }
                        setting->setDecision(lowValue, highValue, defaultValue, selectedValue);

diff --git a/src/Tuner/searchtuner.h b/src/Tuner/searchtuner.h
index 0aabb6465affbc8b116b6271ef562efc7663f21e..26fd8df51a66004fa23c1fda5462902811320cd9 100644 (file)
--- a/src/Tuner/searchtuner.h
+++ b/src/Tuner/searchtuner.h
@@ -15,7 +15,7 @@ public:
        TunableSetting(TunableSetting *ts);
        void setDecision(int _low, int _high, int _default, int _selection);
        void print();
-        friend std::ostream& operator<< (std::ostream& stream, const TunableSetting& matrix);
+       friend std ::ostream &operator<< (std::ostream &stream, const TunableSetting &matrix);
        CMEMALLOC;
 private:
        bool hasVar;
@@ -49,8 +49,8 @@ public:
        uint getSize() { return usedSettings.getSize();}
        void print();
        void printUsed();
-        void serialize();
-        
+       void serialize();
+
        CMEMALLOC;
 private:
        /** Used Settings keeps track of settings that were actually used by

diff --git a/src/Tuner/tunable.cc b/src/Tuner/tunable.cc
index a06d0f1290b888bcb0a167b86a2961a2c7ec1f21..966cb0014226c9e009d6abb1aac1a68fcc07c28d 100644 (file)
--- a/src/Tuner/tunable.cc
+++ b/src/Tuner/tunable.cc
@@ -15,35 +15,35 @@ int DefaultTuner::getVarTunable(VarType vartype1, VarType vartype2, TunableParam
        return descriptor->defaultValue;
 }
 
-const char* tunableParameterToString(Tunables tunable){
-        switch(tunable){
-                case DECOMPOSEORDER:
-                        return "DECOMPOSEORDER";
-                case MUSTREACHGLOBAL:
-                        return "MUSTREACHGLOBAL";
-                case MUSTREACHLOCAL:
-                        return "MUSTREACHLOCAL";
-                case MUSTREACHPRUNE:
-                        return "MUSTREACHPRUNE";
-                case OPTIMIZEORDERSTRUCTURE:
-                        return "OPTIMIZEORDERSTRUCTURE";
-                case ORDERINTEGERENCODING:
-                        return "ORDERINTEGERENCODING";
-                case PREPROCESS:
-                        return "PREPROCESS";
-                case NODEENCODING:
-                        return "NODEENCODING";
-                case EDGEENCODING:
-                        return "EDGEENCODING";
-                case MUSTEDGEPRUNE:
-                        return "MUSTEDGEPRUNE";
-               case ELEMENTOPT: 
-                       return "ELEMENTOPT";
-               case ELEMENTOPTSETS:
-                       return "ELEMENTOPTSETS";
-               case PROXYVARIABLE:
-                       return "PROXYVARIABLE";
-                default:
-                        ASSERT(0);
-        }
+const char *tunableParameterToString(Tunables tunable) {
+       switch (tunable) {
+       case DECOMPOSEORDER:
+               return "DECOMPOSEORDER";
+       case MUSTREACHGLOBAL:
+               return "MUSTREACHGLOBAL";
+       case MUSTREACHLOCAL:
+               return "MUSTREACHLOCAL";
+       case MUSTREACHPRUNE:
+               return "MUSTREACHPRUNE";
+       case OPTIMIZEORDERSTRUCTURE:
+               return "OPTIMIZEORDERSTRUCTURE";
+       case ORDERINTEGERENCODING:
+               return "ORDERINTEGERENCODING";
+       case PREPROCESS:
+               return "PREPROCESS";
+       case NODEENCODING:
+               return "NODEENCODING";
+       case EDGEENCODING:
+               return "EDGEENCODING";
+       case MUSTEDGEPRUNE:
+               return "MUSTEDGEPRUNE";
+       case ELEMENTOPT:
+               return "ELEMENTOPT";
+       case ELEMENTOPTSETS:
+               return "ELEMENTOPTSETS";
+       case PROXYVARIABLE:
+               return "PROXYVARIABLE";
+       default:
+               ASSERT(0);
+       }
 }

diff --git a/src/csolver.cc b/src/csolver.cc
index 5cdca73eb0ce7c91ce3a3feb4ca405290d3fcfbd..e72b3631de5385a23442b6f663d4f1731725198e 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -621,18 +621,18 @@ int CSolver::solve() {
 
        naiveEncodingDecision(this);
 //     eg.validate();
-       
+
        time2 = getTimeNano();
        model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC);
 
        satEncoder->encodeAllSATEncoder(this);
        time1 = getTimeNano();
 
-       model_print("Elapse Encode time: %f\n", (time1- startTime) / NANOSEC);
-       
+       model_print("Elapse Encode time: %f\n", (time1 - startTime) / NANOSEC);
+
        model_print("Is problem UNSAT after encoding: %d\n", unsat);
        int result = unsat ? IS_UNSAT : satEncoder->solve();
-       model_print("Result Computed in SAT solver:\t%s\n", result == IS_SAT? "SAT" : " UNSAT");
+       model_print("Result Computed in SAT solver:\t%s\n", result == IS_SAT ? "SAT" : " UNSAT");
        time2 = getTimeNano();
        elapsedTime = time2 - startTime;
        model_print("CSOLVER solve time: %f\n", elapsedTime / NANOSEC);