glucose-syrup/core/BoundedQueue.h

   1 /***************************************************************************************[BoundedQueue.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
  51 #ifndef BoundedQueue_h
  52 #define BoundedQueue_h
  53
  54 #include "mtl/Vec.h"
  55
  56 //=================================================================================================
  57
  58 namespace Glucose {
  59
  60 template <class T>
  61 class bqueue {
  62     vec<T>  elems;
  63     int     first;
  64         int             last;
  65         unsigned long long sumofqueue;
  66         int     maxsize;
  67         int     queuesize; // Number of current elements (must be < maxsize !)
  68         bool expComputed;
  69         double exp,value;
  70 public:
  71  bqueue(void) : first(0), last(0), sumofqueue(0), maxsize(0), queuesize(0),expComputed(false) { }
  72
  73         void initSize(int size) {growTo(size);exp = 2.0/(size+1);} // Init size of bounded size queue
  74
  75         void push(T x) {
  76           expComputed = false;
  77                 if (queuesize==maxsize) {
  78                         assert(last==first); // The queue is full, next value to enter will replace oldest one
  79                         sumofqueue -= elems[last];
  80                         if ((++last) == maxsize) last = 0;
  81                 } else
  82                         queuesize++;
  83                 sumofqueue += x;
  84                 elems[first] = x;
  85                 if ((++first) == maxsize) {first = 0;last = 0;}
  86         }
  87
  88         T peek() { assert(queuesize>0); return elems[last]; }
  89         void pop() {sumofqueue-=elems[last]; queuesize--; if ((++last) == maxsize) last = 0;}
  90
  91         unsigned long long getsum() const {return sumofqueue;}
  92         unsigned int getavg() const {return (unsigned int)(sumofqueue/((unsigned long long)queuesize));}
  93         int maxSize() const {return maxsize;}
  94         double getavgDouble() const {
  95           double tmp = 0;
  96           for(int i=0;i<elems.size();i++) {
  97             tmp+=elems[i];
  98           }
  99           return tmp/elems.size();
 100         }
 101         int isvalid() const {return (queuesize==maxsize);}
 102
 103         void growTo(int size) {
 104                 elems.growTo(size);
 105                 first=0; maxsize=size; queuesize = 0;last = 0;
 106                 for(int i=0;i<size;i++) elems[i]=0;
 107         }
 108
 109         double getAvgExp() {
 110           if(expComputed) return value;
 111           double a=exp;
 112           value = elems[first];
 113           for(int i  = first;i<maxsize;i++) {
 114             value+=a*((double)elems[i]);
 115             a=a*exp;
 116           }
 117           for(int i  = 0;i<last;i++) {
 118             value+=a*((double)elems[i]);
 119             a=a*exp;
 120           }
 121           value = value*(1-exp)/(1-a);
 122           expComputed = true;
 123           return value;
 124
 125
 126         }
 127         void fastclear() {first = 0; last = 0; queuesize=0; sumofqueue=0;} // to be called after restarts... Discard the queue
 128
 129     int  size(void)    { return queuesize; }
 130
 131     void clear(bool dealloc = false)   { elems.clear(dealloc); first = 0; maxsize=0; queuesize=0;sumofqueue=0;}
 132
 133     void copyTo(bqueue &dest) const {
 134         dest.last = last;
 135         dest.sumofqueue = sumofqueue;
 136         dest.maxsize = maxsize;
 137         dest.queuesize = queuesize;
 138         dest.expComputed = expComputed;
 139         dest.exp = exp;
 140         dest.value = value;
 141         dest.first = first;
 142         elems.copyTo(dest.elems);
 143     }
 144 };
 145 }
 146 //=================================================================================================
 147
 148 #endif