tabbing

diff --git a/src/ASTAnalyses/Encoding/encodinggraph.cc b/src/ASTAnalyses/Encoding/encodinggraph.cc
index 957fea33ba4818cd67e98a88e66f839c8293a98e..d2791d3a02e994da2584ec4da731de57d1c909a0 100644 (file)
--- a/src/ASTAnalyses/Encoding/encodinggraph.cc
+++ b/src/ASTAnalyses/Encoding/encodinggraph.cc
@@ -333,8 +333,8 @@ void EncodingGraph::decideEdges() {
                        EncodingNode *tmp = left; left = right; right = tmp;
                        EncodingSubGraph *tmpsg = leftGraph; leftGraph = rightGraph; rightGraph = tmpsg;
                }
-               
-               uint leftSize = 0, rightSize = 0, newSize = 0, max=0;
+
+               uint leftSize = 0, rightSize = 0, newSize = 0, max = 0;
                bool merge = false;
                if (leftGraph == NULL && rightGraph == NULL) {
                        leftSize = convertSize(left->getSize());
@@ -348,7 +348,7 @@ void EncodingGraph::decideEdges() {
                        newSize = convertSize(leftGraph->estimateNewSize(right));
                        newSize = (leftSize > newSize) ? leftSize : newSize;
                        newSize = (rightSize > newSize) ? rightSize : newSize;
-                       max = rightSize > leftSize? rightSize : leftSize;
+                       max = rightSize > leftSize ? rightSize : leftSize;
 //                     model_print("Merge=%s\tsimilarity=%f\n", max==newSize?"TRUE":"FALSE", left->measureSimilarity(right));
                        merge = left->measureSimilarity(right) > 1.5 || max == newSize;
                } else {
@@ -359,7 +359,7 @@ void EncodingGraph::decideEdges() {
 //                     model_print("MergingSubGraphs: left=%u\tright=%u\tnewSize=%u\n", leftSize, rightSize, newSize);
                        newSize = (leftSize > newSize) ? leftSize : newSize;
                        newSize = (rightSize > newSize) ? rightSize : newSize;
-                       max = rightSize > leftSize? rightSize : leftSize;
+                       max = rightSize > leftSize ? rightSize : leftSize;
 //                     model_print("Merge=%s\tsimilarity=%f\n", max==newSize?"TRUE":"FALSE", leftGraph->measureSimilarity(right));
                        merge = leftGraph->measureSimilarity(right) > 1.5 || max == newSize;
                }
@@ -419,7 +419,7 @@ uint EncodingNode::getSize() const {
        return s->getSize();
 }
 
-uint64_t EncodingNode::getIndex(uint index){
+uint64_t EncodingNode::getIndex(uint index) {
        return s->getElement(index);
 }
 
@@ -427,24 +427,24 @@ VarType EncodingNode::getType() const {
        return s->getType();
 }
 
-bool EncodingNode::itemExists(uint64_t item){
-       for(uint i=0; i< s->getSize(); i++){
-               if(item == s->getElement(i))
+bool EncodingNode::itemExists(uint64_t item) {
+       for (uint i = 0; i < s->getSize(); i++) {
+               if (item == s->getElement(i))
                        return true;
        }
        return false;
 }
 
-double EncodingNode::measureSimilarity(EncodingNode *node){
+double EncodingNode::measureSimilarity(EncodingNode *node) {
        uint common = 0;
-       for(uint i=0; i < s->getSize(); i++){
+       for (uint i = 0; i < s->getSize(); i++) {
                uint64_t item = s->getElement(i);
-               if(node->itemExists(item)){
+               if (node->itemExists(item)) {
                        common++;
                }
        }
 //     model_print("common=%u\tsize1=%u\tsize2=%u\tsim1=%f\tsim2=%f\n", common, s->getSize(), node->getSize(), 1.0*common/s->getSize(), 1.0*common/node->getSize());
-       return common*1.0/s->getSize() + common*1.0/node->getSize();
+       return common * 1.0 / s->getSize() + common * 1.0 / node->getSize();
 }
 
 EncodingNode *EncodingGraph::createNode(Element *e) {

diff --git a/src/ASTAnalyses/Encoding/encodinggraph.h b/src/ASTAnalyses/Encoding/encodinggraph.h
index ae330b853dcedca2cbeafa0f804c513a56de258a..96c163efd03f1c0b7befbcf5baeaf54d41437104 100644 (file)
--- a/src/ASTAnalyses/Encoding/encodinggraph.h
+++ b/src/ASTAnalyses/Encoding/encodinggraph.h
@@ -44,10 +44,10 @@ public:
        uint getSize() const;
        uint64_t getIndex(uint index);
        VarType getType() const;
-        double measureSimilarity(EncodingNode *node);
+       double measureSimilarity(EncodingNode *node);
        void setEncoding(ElementEncodingType e) {encoding = e;}
        ElementEncodingType getEncoding() {return encoding;}
-        bool itemExists(uint64_t item);
+       bool itemExists(uint64_t item);
        bool couldBeBinaryIndex() {return encoding == BINARYINDEX || encoding == ELEM_UNASSIGNED;}
        CMEMALLOC;
 private:

diff --git a/src/ASTAnalyses/Encoding/subgraph.cc b/src/ASTAnalyses/Encoding/subgraph.cc
index de76e4d0e6890d149fd703795f3713dc455ad3be..577ed5f1b9a249e24cbd790f7fa5cf404820066d 100644 (file)
--- a/src/ASTAnalyses/Encoding/subgraph.cc
+++ b/src/ASTAnalyses/Encoding/subgraph.cc
@@ -127,18 +127,18 @@ double EncodingSubGraph::measureSimilarity(EncodingNode *node) {
        SetIteratorEncodingNode *nit = nodes.iterator();
        while (nit->hasNext()) {
                EncodingNode *en = nit->next();
-               for(uint i=0; i < en->getSize(); i++){
+               for (uint i = 0; i < en->getSize(); i++) {
                        intSet.add(en->getIndex(i));
                }
        }
-       for(uint i=0; i < node->getSize(); i++){
-               if(intSet.contains( node->getIndex(i) )){
+       for (uint i = 0; i < node->getSize(); i++) {
+               if (intSet.contains( node->getIndex(i) )) {
                        common++;
                }
        }
 //     model_print("measureSimilarity:139: common=%u\t GraphSize=%u\tnodeSize=%u\tGraphSim=%f\tnodeSim=%f\n", common, intSet.getSize(), node->getSize(), 1.0*common/intSet.getSize(), 1.0*common/node->getSize());
        delete nit;
-       return common*1.0/intSet.getSize() + common*1.0/node->getSize();
+       return common * 1.0 / intSet.getSize() + common * 1.0 / node->getSize();
 }
 
 double EncodingSubGraph::measureSimilarity(EncodingSubGraph *sg) {
@@ -148,7 +148,7 @@ double EncodingSubGraph::measureSimilarity(EncodingSubGraph *sg) {
        SetIteratorEncodingNode *nit = nodes.iterator();
        while (nit->hasNext()) {
                EncodingNode *en = nit->next();
-               for(uint i=0; i < en->getSize(); i++){
+               for (uint i = 0; i < en->getSize(); i++) {
                        set1.add(en->getIndex(i));
                }
        }
@@ -156,21 +156,21 @@ double EncodingSubGraph::measureSimilarity(EncodingSubGraph *sg) {
        nit = sg->nodes.iterator();
        while (nit->hasNext()) {
                EncodingNode *en = nit->next();
-               for(uint i=0; i < en->getSize(); i++){
+               for (uint i = 0; i < en->getSize(); i++) {
                        set2.add(en->getIndex(i));
                }
        }
        delete nit;
        SetIterator64Int *setIter1 = set1.iterator();
-       while(setIter1->hasNext()){
+       while (setIter1->hasNext()) {
                uint64_t item1 = setIter1->next();
-               if( set2.contains(item1)){
+               if ( set2.contains(item1)) {
                        common++;
                }
        }
        delete setIter1;
 //     model_print("measureSimilarity:139: common=%u\tGraphSize1=%u\tGraphSize2=%u\tGraphSize1=%f\tGraphSize2=%f\n", common, set1.getSize(), set2.getSize(), 1.0*common/set1.getSize(), 1.0*common/set2.getSize());
-       return common*1.0/set1.getSize() + common*1.0/set2.getSize();
+       return common * 1.0 / set1.getSize() + common * 1.0 / set2.getSize();
 }
 
 uint EncodingSubGraph::estimateNewSize(EncodingNode *n) {

diff --git a/src/ASTAnalyses/Encoding/subgraph.h b/src/ASTAnalyses/Encoding/subgraph.h
index 1392dba72b70ee98df814d55102c73eecce9eab2..0ceb306933152ef9f1232cd620209874b8027214 100644 (file)
--- a/src/ASTAnalyses/Encoding/subgraph.h
+++ b/src/ASTAnalyses/Encoding/subgraph.h
@@ -45,8 +45,8 @@ public:
        void encode();
        uint getEncoding(EncodingNode *n, uint64_t val);
        uint getEncodingMaxVal(EncodingNode *n) { return maxEncodingVal;}
-        double measureSimilarity(EncodingNode *n);
-        double measureSimilarity(EncodingSubGraph *sg);
+       double measureSimilarity(EncodingNode *n);
+       double measureSimilarity(EncodingSubGraph *sg);
        CMEMALLOC;
 private:
        uint estimateNewSize(EncodingNode *n);

diff --git a/src/Backend/inc_solver.cc b/src/Backend/inc_solver.cc
index c1bebb806ad0e453ebd1e5a7e087ca34ac697551..2d6b8a48d993aa6ad9164e2060b413c50533e0b6 100644 (file)
--- a/src/Backend/inc_solver.cc
+++ b/src/Backend/inc_solver.cc
@@ -117,23 +117,23 @@ int readStatus(IncrementalSolver *This) {
        fd_set rfds;
        FD_ZERO(&rfds);
        FD_SET(This->from_solver_fd, &rfds);
-       fd_set * temp;
-       if(This->timeout == NOTIMEOUT){
-               retval = select(This->from_solver_fd+1, &rfds, NULL, NULL, NULL);
-       }else {
+       fd_set *temp;
+       if (This->timeout == NOTIMEOUT) {
+               retval = select(This->from_solver_fd + 1, &rfds, NULL, NULL, NULL);
+       } else {
                struct timeval tv;
                tv.tv_sec = This->timeout;
                tv.tv_usec = 0;
-               retval = select(This->from_solver_fd+1, &rfds, NULL, NULL, &tv);
+               retval = select(This->from_solver_fd + 1, &rfds, NULL, NULL, &tv);
        }
-       if(retval == -1){
+       if (retval == -1) {
                perror("Error in select()");
                exit(EXIT_FAILURE);
        }
-       else if (retval){
+       else if (retval) {
                printf("Data is available now.\n");
                return readIntSolver(This);
-       }else{
+       } else {
                printf("Timeout for the solver\n");
                return IS_INDETER;
        }

diff --git a/src/Backend/inc_solver.h b/src/Backend/inc_solver.h
index 4692cfe626f0e6fd3add84adaf4a615bcfe4ddd1..3562a4270b76b6dfb2a8a0c3515e188eac632165 100644 (file)
--- a/src/Backend/inc_solver.h
+++ b/src/Backend/inc_solver.h
@@ -28,7 +28,7 @@ struct IncrementalSolver {
        pid_t solver_pid;
        int to_solver_fd;
        int from_solver_fd;
-        long timeout;
+       long timeout;
 };
 
 IncrementalSolver *allocIncrementalSolver();

diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc
index 8f06eecad991e3d68d9b83e5d5b47f3bba3a4f6b..2f93d21ea1dac6edbb7533b5a3819ffe1fe57a68 100644 (file)
--- a/src/Backend/satelemencoder.cc
+++ b/src/Backend/satelemencoder.cc
@@ -223,10 +223,10 @@ void SATEncoder::generateBinaryIndexEncodingVars(ElementEncoding *encoding) {
        ASSERT(encoding->type == BINARYINDEX);
        allocElementConstraintVariables(encoding, NUMBITS(encoding->encArraySize - 1));
        getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
-       if (encoding->element->anyValue){
+       if (encoding->element->anyValue) {
                uint setSize = encoding->element->getRange()->getSize();
                uint encArraySize = encoding->encArraySize;
-               if(setSize < encArraySize * (uint)solver->getTuner()->getTunable(MUSTVALUE, &mustValueBinaryIndex)/10){
+               if (setSize < encArraySize * (uint)solver->getTuner()->getTunable(MUSTVALUE, &mustValueBinaryIndex) / 10) {
                        generateAnyValueBinaryIndexEncodingPositive(encoding);
                } else {
                        generateAnyValueBinaryIndexEncoding(encoding);

diff --git a/src/Serialize/deserializer.cc b/src/Serialize/deserializer.cc
index 548619fe221d45a380bb35933b08e08f552dafe1..c9a708ce4e625311d905da22bb1b37781327b74f 100644 (file)
--- a/src/Serialize/deserializer.cc
+++ b/src/Serialize/deserializer.cc
@@ -153,8 +153,8 @@ void Deserializer::deserializeBooleanConst() {
        myread(&b, sizeof(BooleanVar *));
        bool istrue;
        myread(&istrue, sizeof(bool));
-       map.put(b, istrue?solver->getBooleanTrue().getBoolean():
-                       solver->getBooleanFalse().getBoolean());
+       map.put(b, istrue ? solver->getBooleanTrue().getBoolean() :
+                                       solver->getBooleanFalse().getBoolean());
 }
 
 void Deserializer::deserializeBooleanOrder() {

diff --git a/src/Test/deserializerun.cc b/src/Test/deserializerun.cc
index 14551a624f1a068eb07b7cedcd248c57343eb013..29afbd9a22bcdf97aa27834f3c7e0be2aefb5568 100644 (file)
--- a/src/Test/deserializerun.cc
+++ b/src/Test/deserializerun.cc
@@ -14,6 +14,7 @@ int main(int argc, char **argv) {
        sscanf(argv[2], "%u", &timeout);
        SearchTuner *tuner = new SearchTuner(argv[3]);
        solver->setTuner(tuner);
+       solver->setSatSolverTimeout(timeout);
        int sat = solver->solve();
        long long metric = solver->getElapsedTime();
        ofstream myfile;

diff --git a/src/csolver.cc b/src/csolver.cc
index 9f374cc00df78fc08ac6c7097f0e78aaa4b12b2d..5a914e8af15d4c7b1dcf53b56329feccf4b2f9a9 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -632,7 +632,7 @@ int CSolver::solve() {
 
        model_print("Is problem UNSAT after encoding: %d\n", unsat);
        int result = unsat ? IS_UNSAT : satEncoder->solve(satsolverTimeout);
-       model_print("Result Computed in SAT solver:\t%s\n", result == IS_SAT? "SAT" : result == IS_INDETER? "INDETERMINATE" : " UNSAT");
+       model_print("Result Computed in SAT solver:\t%s\n", result == IS_SAT ? "SAT" : result == IS_INDETER ? "INDETERMINATE" : " UNSAT");
        time2 = getTimeNano();
        elapsedTime = time2 - startTime;
        model_print("CSOLVER solve time: %f\n", elapsedTime / NANOSEC);

diff --git a/src/csolver.h b/src/csolver.h
index 60e7c6861033e70216aa782238d80c7b8f6c0c43..fd6487afb092c688a293f6e40e2d3e193befced5 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -139,7 +139,7 @@ public:
        bool isFalse(BooleanEdge b);
 
        void setUnSAT() { model_print("Setting UNSAT %%%%%%\n"); unsat = true; }
-        void setSatSolverTimeout(long seconds){ satsolverTimeout = seconds;}
+       void setSatSolverTimeout(long seconds) { satsolverTimeout = seconds;}
        bool isUnSAT() { return unsat; }
 
        void printConstraint(BooleanEdge boolean);
@@ -220,7 +220,7 @@ private:
        bool unsat;
        Tuner *tuner;
        long long elapsedTime;
-        long satsolverTimeout;
+       long satsolverTimeout;
        friend class ElementOpt;
 };