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
       6                 :            : this software and associated documentation files (the "Software"), to deal in
       7                 :            : the Software without restriction, including without limitation the rights to
       8                 :            : use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
       9                 :            : the Software, and to permit persons to whom the Software is furnished to do so,
      10                 :            : subject to the following conditions:
      11                 :            : 
      12                 :            : The above copyright notice and this permission notice shall be included in all
      13                 :            : copies or substantial portions of the Software.
      14                 :            : 
      15                 :            : THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
      16                 :            : IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
      17                 :            : FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
      18                 :            : COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
      19                 :            : IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
      20                 :            : CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
      21                 :            : **************************************************************************************************/
      22                 :            : 
      23                 :            : #ifndef Minisat_Heap_h
      24                 :            : #define Minisat_Heap_h
      25                 :            : 
      26                 :            : #include "base/check.h"
      27                 :            : #include "prop/minisat/mtl/Vec.h"
      28                 :            : 
      29                 :            : namespace cvc5::internal {
      30                 :            : namespace Minisat {
      31                 :            : 
      32                 :            : //=================================================================================================
      33                 :            : // A heap implementation with support for decrease/increase key.
      34                 :            : 
      35                 :            : template <class Comp>
      36                 :            : class Heap
      37                 :            : {
      38                 :            :   Comp lt;        // The heap is a minimum-heap with respect to this comparator
      39                 :            :   vec<int> heap;  // Heap of integers
      40                 :            :   vec<int> indices;  // Each integers position (index) in the Heap
      41                 :            : 
      42                 :            :   // Index "traversal" functions
      43                 :    1422766 :   static inline int left(int i) { return i * 2 + 1; }
      44                 :    1080408 :   static inline int right(int i) { return (i + 1) * 2; }
      45                 :     771486 :   static inline int parent(int i) { return (i - 1) >> 1; }
      46                 :            : 
      47                 :     526635 :   void percolateUp(int i)
      48                 :            :   {
      49                 :     526635 :     int x = heap[i];
      50                 :     526635 :     int p = parent(i);
      51                 :            : 
      52 [ +  + ][ +  + ]:     771486 :     while (i != 0 && lt(x, heap[p]))
                 [ +  + ]
      53                 :            :     {
      54                 :     244851 :       heap[i] = heap[p];
      55                 :     244851 :       indices[heap[p]] = i;
      56                 :     244851 :       i = p;
      57                 :     244851 :       p = parent(p);
      58                 :            :     }
      59                 :     526635 :     heap[i] = x;
      60                 :     526635 :     indices[x] = i;
      61                 :     526635 :   }
      62                 :            : 
      63                 :     340095 :   void percolateDown(int i)
      64                 :            :   {
      65                 :     340095 :     int x = heap[i];
      66         [ +  + ]:     512850 :     while (left(i) < heap.size())
      67                 :            :     {
      68         [ +  + ]:     995162 :       int child = right(i) < heap.size() && lt(heap[right(i)], heap[left(i)])
      69         [ +  + ]:     585968 :                       ? right(i)
      70                 :     415476 :                       : left(i);
      71         [ +  + ]:     500722 :       if (!lt(heap[child], x)) break;
      72                 :     172755 :       heap[i] = heap[child];
      73                 :     172755 :       indices[heap[i]] = i;
      74                 :     172755 :       i = child;
      75                 :            :     }
      76                 :     340095 :     heap[i] = x;
      77                 :     340095 :     indices[x] = i;
      78                 :     340095 :   }
      79                 :            : 
      80                 :            :  public:
      81                 :       6272 :   Heap(const Comp& c) : lt(c) {}
      82                 :            : 
      83                 :         39 :   int size() const { return heap.size(); }
      84                 :     295306 :   bool empty() const { return heap.size() == 0; }
      85 [ +  + ][ +  + ]:    1801410 :   bool inHeap(int n) const { return n < indices.size() && indices[n] >= 0; }
      86                 :          0 :   int operator[](int index) const
      87                 :            :   {
      88                 :          0 :     Assert(index < heap.size());
      89                 :          0 :     return heap[index];
      90                 :            :   }
      91                 :            : 
      92                 :     133692 :   void decrease(int n)
      93                 :            :   {
      94 [ -  + ][ -  + ]:     133692 :     Assert(inHeap(n));
                 [ -  - ]
      95                 :     133692 :     percolateUp(indices[n]);
      96                 :     133692 :   }
      97                 :        830 :   void increase(int n)
      98                 :            :   {
      99 [ -  + ][ -  + ]:        830 :     Assert(inHeap(n));
                 [ -  - ]
     100                 :        830 :     percolateDown(indices[n]);
     101                 :        830 :   }
     102                 :            : 
     103                 :            :   // Safe variant of insert/decrease/increase:
     104                 :         54 :   void update(int n)
     105                 :            :   {
     106         [ -  + ]:         54 :     if (!inHeap(n))
     107                 :          0 :       insert(n);
     108                 :            :     else
     109                 :            :     {
     110                 :         54 :       percolateUp(indices[n]);
     111                 :         54 :       percolateDown(indices[n]);
     112                 :            :     }
     113                 :         54 :   }
     114                 :            : 
     115                 :     392889 :   void insert(int n)
     116                 :            :   {
     117                 :     392889 :     indices.growTo(n + 1, -1);
     118 [ -  + ][ -  + ]:     392889 :     Assert(!inHeap(n));
                 [ -  - ]
     119                 :            : 
     120                 :     392889 :     indices[n] = heap.size();
     121                 :     392889 :     heap.push(n);
     122                 :     392889 :     percolateUp(indices[n]);
     123                 :     392889 :   }
     124                 :            : 
     125                 :     283917 :   int removeMin()
     126                 :            :   {
     127                 :     283917 :     int x = heap[0];
     128                 :     283917 :     heap[0] = heap.last();
     129                 :     283917 :     indices[heap[0]] = 0;
     130                 :     283917 :     indices[x] = -1;
     131                 :     283917 :     heap.pop();
     132         [ +  + ]:     283917 :     if (heap.size() > 1) percolateDown(0);
     133                 :     283917 :     return x;
     134                 :            :   }
     135                 :            : 
     136                 :            :   // Rebuild the heap from scratch, using the elements in 'ns':
     137                 :       4225 :   void build(vec<int>& ns)
     138                 :            :   {
     139         [ +  + ]:     162356 :     for (int i = 0; i < heap.size(); i++) indices[heap[i]] = -1;
     140                 :       4225 :     heap.clear();
     141                 :            : 
     142         [ +  + ]:     129446 :     for (int i = 0; i < ns.size(); i++)
     143                 :            :     {
     144                 :     125221 :       indices[ns[i]] = i;
     145                 :     125221 :       heap.push(ns[i]);
     146                 :            :     }
     147                 :            : 
     148         [ +  + ]:      66141 :     for (int i = heap.size() / 2 - 1; i >= 0; i--) percolateDown(i);
     149                 :       4225 :   }
     150                 :            : 
     151                 :          0 :   void clear(bool dealloc = false)
     152                 :            :   {
     153         [ -  - ]:          0 :     for (int i = 0; i < heap.size(); i++) indices[heap[i]] = -1;
     154                 :          0 :     heap.clear(dealloc);
     155                 :          0 :   }
     156                 :            : };
     157                 :            : 
     158                 :            : //=================================================================================================
     159                 :            : }  // namespace Minisat
     160                 :            : }  // namespace cvc5::internal
     161                 :            : 
     162                 :            : #endif