Branch data     Line data    Source code

       1                 :            : /*****************************************************************************************[Queue.h]
       2                 :            : Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
       3                 :            : Copyright (c) 2007-2010, Niklas Sorensson
       4                 :            : 
       5                 :            : Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
       6                 :            : associated documentation files (the "Software"), to deal in the Software without restriction,
       7                 :            : including without limitation the rights to use, copy, modify, merge, publish, distribute,
       8                 :            : sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
       9                 :            : furnished to do so, subject to the following conditions:
      10                 :            : 
      11                 :            : The above copyright notice and this permission notice shall be included in all copies or
      12                 :            : substantial portions of the Software.
      13                 :            : 
      14                 :            : THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
      15                 :            : NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
      16                 :            : NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
      17                 :            : DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
      18                 :            : OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
      19                 :            : **************************************************************************************************/
      20                 :            : 
      21                 :            : #ifndef Minisat_Queue_h
      22                 :            : #define Minisat_Queue_h
      23                 :            : 
      24                 :            : #include "base/check.h"
      25                 :            : #include "prop/minisat/mtl/Vec.h"
      26                 :            : 
      27                 :            : namespace cvc5::internal {
      28                 :            : namespace Minisat {
      29                 :            : 
      30                 :            : //=================================================================================================
      31                 :            : 
      32                 :            : template<class T>
      33                 :            : class Queue {
      34                 :            :     vec<T>  buf;
      35                 :            :     int     first;
      36                 :            :     int     end;
      37                 :            : 
      38                 :            : public:
      39                 :            :     typedef T Key;
      40                 :            : 
      41                 :      51931 :     Queue() : buf(1), first(0), end(0) {}
      42                 :            : 
      43                 :          0 :     void clear (bool dealloc = false) { buf.clear(dealloc); buf.growTo(1); first = end = 0; }
      44         [ +  + ]:    1528550 :     int  size  () const { return (end >= first) ? end - first : end - first + buf.size(); }
      45                 :            : 
      46                 :            :     const T& operator[](int index) const
      47                 :            :     {
      48                 :            :       Assert(index >= 0);
      49                 :            :       Assert(index < size());
      50                 :            :       return buf[(first + index) % buf.size()];
      51                 :            :     }
      52                 :     661280 :     T& operator[](int index)
      53                 :            :     {
      54 [ -  + ][ -  + ]:     661280 :       Assert(index >= 0);
                 [ -  - ]
      55 [ -  + ][ -  + ]:     661280 :       Assert(index < size());
                 [ -  - ]
      56                 :     661280 :       return buf[(first + index) % buf.size()];
      57                 :            :     }
      58                 :            : 
      59                 :     256959 :     T peek() const
      60                 :            :     {
      61 [ -  + ][ -  + ]:     256959 :       Assert(first != end);
                 [ -  - ]
      62                 :     256959 :       return buf[first];
      63                 :            :     }
      64                 :     256959 :     void pop()
      65                 :            :     {
      66 [ -  + ][ -  + ]:     256959 :       Assert(first != end);
                 [ -  - ]
      67                 :     256959 :       first++;
      68         [ +  + ]:     256959 :       if (first == buf.size()) first = 0;
      69                 :     256959 :     }
      70                 :     257149 :     void insert(T elem) {   // INVARIANT: buf[end] is always unused
      71                 :     257149 :         buf[end++] = elem;
      72         [ +  + ]:     257149 :         if (end == buf.size()) end = 0;
      73         [ +  + ]:     257149 :         if (first == end){  // Resize:
      74                 :      21586 :             vec<T>  tmp((buf.size()*3 + 1) >> 1);
      75                 :            :             //**/printf("queue alloc: %d elems (%.1f MB)\n", tmp.size(), tmp.size() * sizeof(T) / 1000000.0);
      76                 :      10793 :             int     i = 0;
      77         [ +  + ]:     371149 :             for (int j = first; j < buf.size(); j++) tmp[i++] = buf[j];
      78         [ +  + ]:      10795 :             for (int j = 0    ; j < end       ; j++) tmp[i++] = buf[j];
      79                 :      10793 :             first = 0;
      80                 :      10793 :             end   = buf.size();
      81                 :      10793 :             tmp.moveTo(buf);
      82                 :            :         }
      83                 :     257149 :     }
      84                 :            : };
      85                 :            : 
      86                 :            : 
      87                 :            : //=================================================================================================
      88                 :            : }
      89                 :            : }  // namespace cvc5::internal
      90                 :            : 
      91                 :            : #endif