From: bdemsky Date: Fri, 12 Oct 2018 18:43:55 +0000 (-0700) Subject: tabbing X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=1038eba14663554fb228406db8f33a8ead28b89b;p=satune.git tabbing --- diff --git a/src/ASTAnalyses/Encoding/encodinggraph.cc b/src/ASTAnalyses/Encoding/encodinggraph.cc index 957fea3..d2791d3 100644 --- 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 ae330b8..96c163e 100644 --- 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 de76e4d..577ed5f 100644 --- 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 1392dba..0ceb306 100644 --- 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 c1bebb8..2d6b8a4 100644 --- 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 4692cfe..3562a42 100644 --- 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 8f06eec..2f93d21 100644 --- 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 548619f..c9a708c 100644 --- 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 14551a6..29afbd9 100644 --- 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 9f374cc..5a914e8 100644 --- 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 60e7c68..fd6487a 100644 --- 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; };