|
@@ -39,13 +39,13 @@ bool GSATThread::solve() {
|
|
|
}
|
|
|
|
|
|
bool GSATThread::solve(bool verbose) {
|
|
|
- end = false;
|
|
|
+ this->end(false);
|
|
|
calcTime = 0;
|
|
|
//Lance Initialise
|
|
|
printf("--- Initialize --------------------------------------------------------------------------\n");
|
|
|
this->initBandit(verbose);
|
|
|
//Si la reponse n'a pas été trouvé durant l'initialisation
|
|
|
- if(!end) {
|
|
|
+ if(!this->isEnd()) {
|
|
|
//Lance les bandit avec la méthode choisit
|
|
|
printf("--- Search ------------------------------------------------------------------------------\n");
|
|
|
this->runBandit(verbose);
|
|
@@ -55,22 +55,35 @@ bool GSATThread::solve(bool verbose) {
|
|
|
printf("--- Result ------------------------------------------------------------------------------\n");
|
|
|
this->printResult();
|
|
|
}
|
|
|
- return end;
|
|
|
+ return this->isEnd();
|
|
|
+}
|
|
|
+
|
|
|
+void GSATThread::end() {
|
|
|
+ this->end(true);
|
|
|
+}
|
|
|
+
|
|
|
+void GSATThread::end(bool endOrNot) {
|
|
|
+ std::lock_guard<std::mutex> guard(mEnd);
|
|
|
+ bEnd = endOrNot;
|
|
|
+}
|
|
|
+
|
|
|
+bool GSATThread::isEnd() {
|
|
|
+ std::lock_guard<std::mutex> guard(mEnd);
|
|
|
+ return bEnd;
|
|
|
}
|
|
|
|
|
|
void GSATThread::printResult() {
|
|
|
- if(end) {
|
|
|
+ if(this->isEnd()) {
|
|
|
printf(GREEN "s SATISFIABLE\n" RESET);
|
|
|
} else {
|
|
|
printf(RED "NOT FOUND\n" RESET);
|
|
|
}
|
|
|
- //printf("s %s\n",end?"SATISFIABLE":"NOT FOUND");
|
|
|
- if(!end && calcTime == 0) {
|
|
|
+ if(!this->isEnd() && calcTime == 0) {
|
|
|
//Si on à pas trouver
|
|
|
calcTime = gsat[0]->realTime() - time[0];
|
|
|
}
|
|
|
printf(YELLOW);
|
|
|
- if(end) {
|
|
|
+ if(this->isEnd()) {
|
|
|
printf("c [thread:%2d][iteration:%4d][fill:%d][heuristic:%d]Satisfied clauses (begin: %d)(end:%d)\n",
|
|
|
result.threadId,
|
|
|
result.nbIteration,
|
|
@@ -113,12 +126,12 @@ void GSATThread::runBandit(bool verbose) {
|
|
|
void GSATThread::initThread(int id, bool verbose) {
|
|
|
//Les threads vont jouer les bandits pour etablir les moyennes
|
|
|
bool solve = false;
|
|
|
- while(!end && !solve && !cb.queueIsEmpty()){
|
|
|
+ while(!this->isEnd() && !solve && !cb.queueIsEmpty()){
|
|
|
solve = this->calc(id, verbose);
|
|
|
}
|
|
|
//Si 1er arreter
|
|
|
- if(!end && solve) {
|
|
|
- end = true;
|
|
|
+ if(!this->isEnd() && solve) {
|
|
|
+ this->end();
|
|
|
calcTime = gsat[id]->realTime() - time[id];
|
|
|
result.threadId = id;
|
|
|
result.nbIteration = gsat[id]->getNbIterations();
|
|
@@ -132,12 +145,12 @@ void GSATThread::initThread(int id, bool verbose) {
|
|
|
void GSATThread::runThread(int id, bool verbose) {
|
|
|
//Les threads vont jouer les bandits avec la méthode choisit
|
|
|
bool solve = false;
|
|
|
- while(!end && !solve){
|
|
|
+ while(!this->isEnd() && !solve){
|
|
|
solve = this->calc(id, verbose);
|
|
|
}
|
|
|
//Si 1er arreter
|
|
|
- if(!end && solve) {
|
|
|
- end = true;
|
|
|
+ if(!this->isEnd() && solve) {
|
|
|
+ this->end();
|
|
|
calcTime = gsat[id]->realTime() - time[id];
|
|
|
result.threadId = id;
|
|
|
result.nbIteration = gsat[id]->getNbIterations();
|