Branch data     Line data    Source code

       1                 :            : /******************************************************************************************[Heap.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_Heap_h
      22                 :            : #define Minisat_Heap_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                 :            : // A heap implementation with support for decrease/increase key.
      32                 :            : 
      33                 :            : 
      34                 :            : template<class Comp>
      35                 :            : class Heap {
      36                 :            :     Comp     lt;       // The heap is a minimum-heap with respect to this comparator
      37                 :            :     vec<int> heap;     // Heap of integers
      38                 :            :     vec<int> indices;  // Each integers position (index) in the Heap
      39                 :            : 
      40                 :            :     // Index "traversal" functions
      41                 :  260900411 :     static inline int left  (int i) { return i*2+1; }
      42                 :  244718472 :     static inline int right (int i) { return (i+1)*2; }
      43                 :  122849113 :     static inline int parent(int i) { return (i-1) >> 1; }
      44                 :            : 
      45                 :            : 
      46                 :   48106103 :     void percolateUp(int i)
      47                 :            :     {
      48                 :   48106103 :         int x  = heap[i];
      49                 :   48106103 :         int p  = parent(i);
      50                 :            :         
      51 [ +  + ][ +  + ]:  122849113 :         while (i != 0 && lt(x, heap[p])){
                 [ +  + ]
      52                 :   74743010 :             heap[i]          = heap[p];
      53                 :   74743010 :             indices[heap[p]] = i;
      54                 :   74743010 :             i                = p;
      55                 :   74743010 :             p                = parent(p);
      56                 :            :         }
      57                 :   48106103 :         heap   [i] = x;
      58                 :   48106103 :         indices[x] = i;
      59                 :   48106103 :     }
      60                 :            : 
      61                 :            : 
      62                 :   19280370 :     void percolateDown(int i)
      63                 :            :     {
      64                 :   19280370 :         int x = heap[i];
      65         [ +  + ]:  105274073 :         while (left(i) < heap.size()){
      66 [ +  + ][ +  + ]:  100397860 :             int child = right(i) < heap.size() && lt(heap[right(i)], heap[left(i)]) ? right(i) : left(i);
      67         [ +  + ]:  100397860 :             if (!lt(heap[child], x)) break;
      68                 :   85993703 :             heap[i]          = heap[child];
      69                 :   85993703 :             indices[heap[i]] = i;
      70                 :   85993703 :             i                = child;
      71                 :            :         }
      72                 :   19280370 :         heap   [i] = x;
      73                 :   19280370 :         indices[x] = i;
      74                 :   19280370 :     }
      75                 :            : 
      76                 :            : 
      77                 :            :   public:
      78                 :     101212 :     Heap(const Comp& c) : lt(c) { }
      79                 :            : 
      80                 :       3080 :     int  size      ()          const { return heap.size(); }
      81                 :   16437985 :     bool empty     ()          const { return heap.size() == 0; }
      82 [ +  + ][ +  + ]:  267179739 :     bool inHeap    (int n)     const { return n < indices.size() && indices[n] >= 0; }
      83                 :          0 :     int operator[](int index) const
      84                 :            :     {
      85                 :          0 :       Assert(index < heap.size());
      86                 :          0 :       return heap[index];
      87                 :            :     }
      88                 :            : 
      89                 :   29637468 :     void decrease(int n)
      90                 :            :     {
      91 [ -  + ][ -  + ]:   29637468 :       Assert(inHeap(n));
                 [ -  - ]
      92                 :   29637468 :       percolateUp(indices[n]);
      93                 :   29637468 :     }
      94                 :     443637 :     void increase(int n)
      95                 :            :     {
      96 [ -  + ][ -  + ]:     443637 :       Assert(inHeap(n));
                 [ -  - ]
      97                 :     443637 :       percolateDown(indices[n]);
      98                 :     443637 :     }
      99                 :            : 
     100                 :            :     // Safe variant of insert/decrease/increase:
     101                 :     124579 :     void update(int n)
     102                 :            :     {
     103         [ +  + ]:     124579 :         if (!inHeap(n))
     104                 :       2009 :             insert(n);
     105                 :            :         else {
     106                 :     122570 :             percolateUp(indices[n]);
     107                 :     122570 :             percolateDown(indices[n]); }
     108                 :     124579 :     }
     109                 :            : 
     110                 :            : 
     111                 :   18346065 :     void insert(int n)
     112                 :            :     {
     113                 :   18346065 :         indices.growTo(n+1, -1);
     114 [ -  + ][ -  + ]:   18346065 :         Assert(!inHeap(n));
                 [ -  - ]
     115                 :            : 
     116                 :   18346065 :         indices[n] = heap.size();
     117                 :   18346065 :         heap.push(n);
     118                 :   18346065 :         percolateUp(indices[n]); 
     119                 :   18346065 :     }
     120                 :            : 
     121                 :            : 
     122                 :   16261030 :     int  removeMin()
     123                 :            :     {
     124                 :   16261030 :         int x            = heap[0];
     125                 :   16261030 :         heap[0]          = heap.last();
     126                 :   16261030 :         indices[heap[0]] = 0;
     127                 :   16261030 :         indices[x]       = -1;
     128                 :   16261030 :         heap.pop();
     129         [ +  + ]:   16261030 :         if (heap.size() > 1) percolateDown(0);
     130                 :   16261030 :         return x; 
     131                 :            :     }
     132                 :            : 
     133                 :            : 
     134                 :            :     // Rebuild the heap from scratch, using the elements in 'ns':
     135                 :      54820 :     void build(vec<int>& ns) {
     136         [ +  + ]:    5656013 :         for (int i = 0; i < heap.size(); i++)
     137                 :    5601193 :             indices[heap[i]] = -1;
     138                 :      54820 :         heap.clear();
     139                 :            : 
     140         [ +  + ]:    5157066 :         for (int i = 0; i < ns.size(); i++){
     141                 :    5102246 :             indices[ns[i]] = i;
     142                 :    5102246 :             heap.push(ns[i]); }
     143                 :            : 
     144         [ +  + ]:    2597879 :         for (int i = heap.size() / 2 - 1; i >= 0; i--)
     145                 :    2543059 :             percolateDown(i);
     146                 :      54820 :     }
     147                 :            : 
     148                 :          0 :     void clear(bool dealloc = false) 
     149                 :            :     { 
     150         [ -  - ]:          0 :         for (int i = 0; i < heap.size(); i++)
     151                 :          0 :             indices[heap[i]] = -1;
     152                 :          0 :         heap.clear(dealloc); 
     153                 :          0 :     }
     154                 :            : };
     155                 :            : 
     156                 :            : 
     157                 :            : //=================================================================================================
     158                 :            : }
     159                 :            : }  // namespace cvc5::internal
     160                 :            : 
     161                 :            : #endif