glucose-syrup/parallel/ClausesBuffer.cc

   1 /**********************************************************************************[ClausesBuffer.cc]
   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 /* ClausesBuffer
  51  *
  52  * This class is responsible for exchanging clauses between threads.
  53  * It is based on a fixed-length FIFO array of literals.
  54  * If the FIFO is full, then old clauses are removed (even if it was not yet sent to all threads)
  55  *
  56  * a clause " l1 l2 l3" is pushed in the FIFO with the following 6 unsigned integers
  57  * 3 nseen origin l1 l2 l3
  58  * + 3 is the size of the pushed clause
  59  * + nseen is the number of thread which imported this clause (initialized with nthreads-1)
  60  *       (when set to 0, the clause is removed from the fifo)
  61  * + origin is the thread id of the thread which added this clause to the fifo
  62  * + l1 l2 l3 are the literals of the clause
  63  *
  64  * **********************************************************************************************
  65  * **CAREFUL** This class is not thread-safe. In glucose-syrup, the SharedCompanion is
  66  * responsible for ensuring atomicity of main functions
  67  * **********************************************************************************************
  68  *
  69  * */
  70
  71 #include "parallel/ClausesBuffer.h"
  72
  73 //=================================================================================================
  74
  75 using namespace Glucose;
  76
  77 extern BoolOption opt_whenFullRemoveOlder;
  78 extern IntOption  opt_fifoSizeByCore;
  79
  80 // index : size clause
  81 // index + 1 : nbSeen
  82 // index + 2 : threadId
  83 // index + 3 : .. index + 3 + size : Lit of clause
  84 ClausesBuffer::ClausesBuffer(int _nbThreads, unsigned int _maxsize) : first(0), last(_maxsize-1),
  85     maxsize(_maxsize), queuesize(0),
  86     removedClauses(0),
  87     forcedRemovedClauses(0), nbThreads(_nbThreads),
  88     whenFullRemoveOlder(opt_whenFullRemoveOlder), fifoSizeByCore(opt_fifoSizeByCore) {
  89         lastOfThread.growTo(_nbThreads);
  90         for(int i=0;i<nbThreads;i++) lastOfThread[i] = _maxsize-1;
  91         elems.growTo(maxsize);
  92 }
  93
  94 ClausesBuffer::ClausesBuffer() : first(0), last(0), maxsize(0), queuesize(0), removedClauses(0), forcedRemovedClauses(0), nbThreads(0),
  95                                  whenFullRemoveOlder(opt_whenFullRemoveOlder), fifoSizeByCore(opt_fifoSizeByCore) {}
  96
  97 void ClausesBuffer::setNbThreads(int _nbThreads) {
  98     unsigned int _maxsize = fifoSizeByCore*_nbThreads;
  99     last = _maxsize -1;
 100     maxsize = _maxsize;
 101     nbThreads = _nbThreads;
 102     lastOfThread.growTo(_nbThreads);
 103     for(int i=0;i<nbThreads;i++) lastOfThread[i] = _maxsize-1;
 104     elems.growTo(maxsize);
 105 }
 106
 107 uint32_t ClausesBuffer::getCap() {
 108     return elems.capacity();
 109 }
 110 inline unsigned int ClausesBuffer::nextIndex(unsigned int i) {
 111     i++;
 112     if (i == maxsize)
 113         return 0;
 114     return i;
 115 }
 116
 117 inline unsigned int ClausesBuffer::addIndex(unsigned int i, unsigned int a) {
 118     i += a;
 119     if (i >= maxsize)
 120         return i - maxsize;
 121     return i;
 122 }
 123
 124 void ClausesBuffer::removeLastClause() {
 125     assert(queuesize > 0);
 126     do {
 127         unsigned int size = (unsigned int) elems[nextIndex(last)];
 128         unsigned int nextlast = addIndex(last, size+headerSize);
 129
 130         for(int i=0;i<nbThreads;i++) {
 131             if (lastOfThread[i] == last)
 132                 lastOfThread[i] = nextlast;
 133         }
 134
 135         // printf("Removing clause starting at %d of size %d.\n",nextIndex(last), size);
 136         for(unsigned int i=0;i<size+headerSize;i++) {
 137             last = nextIndex(last);
 138             assert(queuesize > 0);
 139             queuesize --;
 140         }
 141         removedClauses ++;
 142         assert(last >= 0);
 143         assert(last < maxsize);
 144         assert(last == nextlast);
 145     } while (queuesize > 0 && (elems[addIndex(last,2)] == 0));
 146
 147 }
 148
 149
 150 // Pushes a single uint to the fifo
 151 inline void ClausesBuffer::noCheckPush(uint32_t x) {
 152     elems[first] = x;
 153     first = nextIndex(first);
 154 }
 155
 156 // Pops a single uint from the fifo
 157 inline uint32_t ClausesBuffer::noCheckPop(uint32_t & index) {
 158     index = nextIndex(index);
 159     uint32_t ret = elems[index];
 160     return ret;
 161 }
 162
 163
 164
 165 // Return true if the clause was succesfully added
 166 bool ClausesBuffer::pushClause(int threadId, Clause & c) {
 167     if (!whenFullRemoveOlder && (queuesize + c.size() + headerSize >= maxsize))
 168         return false; // We need to remove some old clauses
 169     while (queuesize + c.size() + headerSize >= maxsize) { // We need to remove some old clauses
 170         forcedRemovedClauses ++;
 171         removeLastClause();
 172         assert(queuesize > 0);
 173     }
 174     noCheckPush(c.size());
 175     noCheckPush(nbThreads>1?nbThreads-1:1);
 176     noCheckPush(threadId);
 177     for(int i=0;i<c.size();i++)
 178         noCheckPush(toInt(c[i]));
 179     queuesize += c.size()+headerSize;
 180     return true;
 181     //  printf(" -> (%d, %d)\n", first, last);
 182 }
 183
 184 bool ClausesBuffer::getClause(int threadId, int & threadOrigin, vec<Lit> & resultClause,  bool firstFound) {
 185     assert(lastOfThread.size() > threadId);
 186     unsigned int thislast = lastOfThread[threadId];
 187     assert(!firstFound || thislast == last); // FIXME: Gilles has this assertion on his cluster
 188
 189     // Early exiting
 190     if (nextIndex(thislast) == first) return false;
 191
 192     if ( ( thislast < last && last < first) ||
 193             ( first < thislast && thislast < last ) ||
 194             ( last < first && first < thislast) ) {
 195         // Special case where last has moved and lastOfThread[threadId] is no more valid (is behind)
 196         thislast = last;
 197     }
 198     assert(!firstFound);
 199     // Go to next clause for this thread id
 200     if (!firstFound) {
 201         while (nextIndex(thislast) != first && elems[addIndex(thislast,3)] == ((unsigned int)threadId)) { // 3 = 2 + 1
 202             thislast = addIndex(thislast, elems[nextIndex(thislast)] + headerSize); //
 203             assert(thislast >= 0);
 204             assert(thislast < maxsize);
 205         }
 206         assert(nextIndex(thislast)==first || elems[addIndex(thislast,3)] != (unsigned int)threadId);
 207     }
 208
 209     if (nextIndex(thislast) == first) {
 210         lastOfThread[threadId] = thislast;
 211         return false;
 212     }
 213     assert(elems[addIndex(thislast,3)] != ((unsigned int) threadId));
 214     unsigned int previouslast = thislast;
 215     bool removeAfter = false;
 216     int csize = noCheckPop(thislast);
 217     removeAfter = (--elems[addIndex(thislast,1)] == 0); // We are sure this is not one of our own clause
 218     thislast = nextIndex(thislast); // Skips the removeAfter fieldr
 219     threadOrigin = noCheckPop(thislast);
 220     assert(threadOrigin != threadId);
 221     resultClause.clear();
 222     for(int i=0;i<csize;i++) {
 223         resultClause.push(toLit(noCheckPop(thislast)));
 224     }
 225     if (last == previouslast && removeAfter) {
 226         removeLastClause();
 227         thislast = last;
 228     }
 229     lastOfThread[threadId] = thislast;
 230     return true;
 231 }
 232
 233
 234 //=================================================================================================
 235