glucose-syrup/parallel/SharedCompanion.h

   1 /***************************************************************************************[SharedCompanion.h]
   2  Glucose -- Copyright (c) 2009-2014, Gilles Audemard, Laurent Simon
   3                                 CRIL - Univ. Artois, France
   4                                 LRI  - Univ. Paris Sud, France (2009-2013)
   5                                 Labri - Univ. Bordeaux, France
   6
   7  Syrup (Glucose Parallel) -- Copyright (c) 2013-2014, Gilles Audemard, Laurent Simon
   8                                 CRIL - Univ. Artois, France
   9                                 Labri - Univ. Bordeaux, France
  10
  11 Glucose sources are based on MiniSat (see below MiniSat copyrights). Permissions and copyrights of
  12 Glucose (sources until 2013, Glucose 3.0, single core) are exactly the same as Minisat on which it
  13 is based on. (see below).
  14
  15 Glucose-Syrup sources are based on another copyright. Permissions and copyrights for the parallel
  16 version of Glucose-Syrup (the "Software") are granted, free of charge, to deal with the Software
  17 without restriction, including the rights to use, copy, modify, merge, publish, distribute,
  18 sublicence, and/or sell copies of the Software, and to permit persons to whom the Software is
  19 furnished to do so, subject to the following conditions:
  20
  21 - The above and below copyrights notices and this permission notice shall be included in all
  22 copies or substantial portions of the Software;
  23 - The parallel version of Glucose (all files modified since Glucose 3.0 releases, 2013) cannot
  24 be used in any competitive event (sat competitions/evaluations) without the express permission of
  25 the authors (Gilles Audemard / Laurent Simon). This is also the case for any competitive event
  26 using Glucose Parallel as an embedded SAT engine (single core or not).
  27
  28
  29 --------------- Original Minisat Copyrights
  30
  31 Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
  32 Copyright (c) 2007-2010, Niklas Sorensson
  33
  34 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
  35 associated documentation files (the "Software"), to deal in the Software without restriction,
  36 including without limitation the rights to use, copy, modify, merge, publish, distribute,
  37 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
  38 furnished to do so, subject to the following conditions:
  39
  40 The above copyright notice and this permission notice shall be included in all copies or
  41 substantial portions of the Software.
  42
  43 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
  44 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
  45 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
  46 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
  47 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
  48  **************************************************************************************************/
  49
  50 /* This class is responsible for protecting (by mutex) information exchange between threads.
  51  * It also allows each solver to send / receive clause / unary clauses.
  52  *
  53  * Only one sharedCompanion is created for all the solvers
  54  */
  55
  56
  57 #ifndef SharedCompanion_h
  58 #define SharedCompanion_h
  59 #include "core/SolverTypes.h"
  60 #include "parallel/ParallelSolver.h"
  61 #include "parallel/SolverCompanion.h"
  62 #include "parallel/ClausesBuffer.h"
  63
  64 namespace Glucose {
  65
  66
  67 class SharedCompanion : public SolverCompanion {
  68     friend class MultiSolvers;
  69     friend class ParallelSolver;
  70 public:
  71         SharedCompanion(int nbThreads=0);
  72         void setNbThreads(int _nbThreads); // Sets the number of threads (cannot by changed once the solver is running)
  73         void newVar(bool sign);            // Adds a var (used to keep track of unary variables)
  74         void printStats();                 // Printing statistics of all solvers
  75
  76         bool jobFinished();                // True if the job is over
  77         bool IFinished(ParallelSolver *s); // returns true if you are the first solver to finish
  78         bool addSolver(ParallelSolver*);   // attach a solver to accompany
  79         void addLearnt(ParallelSolver *s,Lit unary);   // Add a unary clause to share
  80         bool addLearnt(ParallelSolver *s, Clause & c); // Add a clause to the shared companion, as a database manager
  81
  82         bool getNewClause(ParallelSolver *s, int &th, vec<Lit> & nc); // gets a new interesting clause for solver s
  83         Lit getUnary(ParallelSolver *s);                              // Gets a new unary literal
  84         inline ParallelSolver* winner(){return jobFinishedBy;}        // Gets the first solver that called IFinished()
  85
  86  protected:
  87
  88         ClausesBuffer clausesBuffer; // A big blackboard for all threads sharing non unary clauses
  89         int nbThreads;               // Number of threads
  90
  91         // A set of mutex variables
  92         pthread_mutex_t mutexSharedCompanion; // mutex for any high level sync between all threads (like reportf)
  93         pthread_mutex_t mutexSharedClauseCompanion; // mutex for reading/writing clauses on the blackboard
  94         pthread_mutex_t mutexSharedUnitCompanion; // mutex for reading/writing unit clauses on the blackboard
  95         pthread_mutex_t mutexJobFinished;
  96
  97         bool bjobFinished;
  98         ParallelSolver *jobFinishedBy;
  99         bool panicMode;                        // panicMode means no more increasing space needed
 100         lbool jobStatus;                       // globale status of the job
 101
 102         // Shared clauses are a queue of lits...
 103         //      friend class wholearnt;
 104         vec<int> nextUnit; // indice of next unit clause to retrieve for solver number i
 105         vec<Lit> unitLit;  // Set of unit literals found so far
 106         vec<lbool> isUnary; // sign of the unary var (if proved, or l_Undef if not)
 107         double    random_seed;
 108
 109         // Returns a random float 0 <= x < 1. Seed must never be 0.
 110         static inline double drand(double& seed) {
 111             seed *= 1389796;
 112             int q = (int)(seed / 2147483647);
 113             seed -= (double)q * 2147483647;
 114             return seed / 2147483647; }
 115
 116         // Returns a random integer 0 <= x < size. Seed must never be 0.
 117         static inline int irand(double& seed, int size) {
 118             return (int)(drand(seed) * size); }
 119
 120 };
 121 }
 122 #endif