#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]; } } void GSATThread::useAverageMethod() { cb.setMethod(MT_AVG); } void GSATThread::useEpsilonMethod(double epsilon) { cb.setMethod(MT_EPS); cb.setEpsilon(epsilon); } bool GSATThread::solve() { return this->solve(true); } bool GSATThread::solve(bool verbose) { 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(!this->isEnd()) { //Lance les bandit avec la méthode choisit printf("--- Search ------------------------------------------------------------------------------\n"); this->runBandit(verbose); } //Resultat if(verbose) { printf("--- Result ------------------------------------------------------------------------------\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); } 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::initBandit(bool verbose) { threads.clear(); //Lance thread for(int i = 0; i < nbThread; i++) { time[i] = gsat[i]->realTime(); threads[i] = std::thread(&GSATThread::initThread, this, i, verbose); } //Attend resultat for(int i = 0; i < nbThread; i++){ threads[i].join(); } } void GSATThread::runBandit(bool verbose) { threads.clear(); //Lance thread for(int i = 0; i < nbThread; i++) { threads[i] = std::thread(&GSATThread::runThread, this, i, verbose); } //Attend resultat for(int i = 0; i < nbThread; i++){ threads[i].join(); } } void GSATThread::initThread(int id, bool verbose) { //Les threads vont jouer les bandits pour etablir les moyennes bool solve = false; while(!this->isEnd() && !solve && !cb.queueIsEmpty()){ solve = this->calc(id, verbose); } //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(); } } void GSATThread::runThread(int id, bool verbose) { //Les threads vont jouer les bandits avec la méthode choisit bool solve = false; while(!this->isEnd() && !solve){ solve = this->calc(id, verbose); } //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(); } } bool GSATThread::calc(int id, bool verbose) { //Recup le prochaine fill et heuristic à tester fillAndHeuristic fah = cb.next(); //Calcul bool solve = gsat[id]->start(fah.fill, fah.heuristic); //Affiche 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); } } //Ajoute le resultat aux moyenne cb.addFill(fah.fill, gsat[id]->getNbSatisfiedClausesFill()); cb.addHeuristic(fah.heuristic, gsat[id]->getNbSatisfiedClausesSolve()); return solve; }