From: bdemsky Date: Tue, 2 Oct 2018 18:04:12 +0000 (-0700) Subject: Fix tabbing X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=3ea7df0292dcc11b7a60a186d375bda980d771e5 Fix tabbing --- diff --git a/src/AST/element.cc b/src/AST/element.cc index d807231..f182cd2 100644 --- 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 a7217b5..91d677f 100644 --- 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 8029049..2ac69c1 100644 --- 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; iencArraySize; 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 f3d58a2..d284d21 100644 --- 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 919d7f4..98036a7 100644 --- 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 18164f5..8d2666c 100644 --- 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 ac6e6bf..ff069ec 100644 --- 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 f5aa44b..0de7043 100644 --- 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 29c3289..d31a72f 100644 --- 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 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 3486a9c..e9de49f 100644 --- 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 0aabb64..26fd8df 100644 --- 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 a06d0f1..966cb00 100644 --- 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 5cdca73..e72b363 100644 --- 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);