#include #include #include #include "GSATThread.hpp" #include "color.h" /* --- Public --- */ GSATThread::GSATThread(int _nbThread, int argc, char** argv) { nbThread = _nbThread; gsat = std::vector(_nbThread); time = std::vector(_nbThread); threads = std::vector(_nbThread); for(int i = 0; i < _nbThread; i++) { gsat[i] = new GSAT(); gsat[i]->setParameters(argc,argv); gsat[i]->initialize(); time[i] = 0; } } GSATThread::~GSATThread() { for(int i = 0; i < nbThread; i++) { delete gsat[i]; } } bool GSATThread::solve() { return this->solve(0, true); } bool GSATThread::solve(int maxIteration) { return this->solve(maxIteration, true); } bool GSATThread::solve(bool verbose) { return this->solve(0, verbose); } bool GSATThread::solve(int _maxIteration, bool verbose) { threads.clear(); this->end(false); calcTime = 0; maxIteration = _maxIteration; //Lance thread for(int i = 0; i < nbThread; i++) { time[i] = gsat[i]->realTime(); threads[i] = std::thread(&GSATThread::solverThread, this, i, verbose); } //Attend resultat for(int i = 0; i < nbThread; i++){ threads[i].join(); } //Resultat if(verbose) { printf("-----------------------------------------------------------------------------------------\n"); this->printResult(); } return this->isEnd(); } void GSATThread::end() { this->end(true); } void GSATThread::end(bool endOrNot) { std::lock_guard guard(mEnd); bEnd = endOrNot; } bool GSATThread::isEnd() { std::lock_guard guard(mEnd); return bEnd; } void GSATThread::printResult() { 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(!this->isEnd() && calcTime == 0) { //Si on à pas trouver calcTime = gsat[0]->realTime() - time[0]; } printf(YELLOW); printf("c real time : %.4f seconds\n", calcTime); if(this->isEnd()) { printf("c [thread:%2d][iteration:%4d][fill:%d][heuristic:%d]Satisfied clauses (begin: %d)(end:%d)\n", result.threadId, result.nbIteration, result.heuristicFill, result.heuristicSolve, result.nbSatisfiedClausesFill, result.nbSatisfiedClausesSolve); } printf(RESET); } /* --- Private --- */ void GSATThread::solverThread(int id, bool verbose) { //Resolution bool solve = false; int cpt = 0; while(!this->isEnd() && !solve && (maxIteration == 0 || cpt < maxIteration)){ solve = gsat[id]->start(); if(verbose) { if(solve) { printf(CYAN); } printf("c [thread:%2d][iteration:%4d][fill:%d][heuristic:%d]Satisfied clauses (begin: %d)(end:%d)\n", id, gsat[id]->getNbIterations(), gsat[id]->getHeuristicFill(), gsat[id]->getHeuristicSolve(), gsat[id]->getNbSatisfiedClausesFill(), gsat[id]->getNbSatisfiedClausesSolve()); if(solve) { printf(RESET); } } cpt++; } //Si 1er arreter if(!this->isEnd() && solve) { this->end(); calcTime = gsat[id]->realTime() - time[id]; result.threadId = id; result.nbIteration = gsat[id]->getNbIterations(); result.heuristicFill = gsat[id]->getHeuristicFill(); result.heuristicSolve = gsat[id]->getHeuristicSolve(); result.nbSatisfiedClausesFill = gsat[id]->getNbSatisfiedClausesFill(); result.nbSatisfiedClausesSolve = gsat[id]->getNbSatisfiedClausesSolve(); } }