minisat_heap.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  *\file minisat_heap.h
00004  *\brief MiniSat internal heap implementation
00005  *
00006  * Author: Alexander Fuchs
00007  *
00008  * Created: Fri Sep 08 11:04:00 2006
00009  *
00010  * <hr>
00011  *
00012  * License to use, copy, modify, sell and/or distribute this software
00013  * and its documentation for any purpose is hereby granted without
00014  * royalty, subject to the terms and conditions defined in the \ref
00015  * LICENSE file provided with this distribution.
00016  * 
00017  * <hr>
00018  */
00019 /*****************************************************************************/
00020 
00021 /******************************************************************************************[Heap.h]
00022 MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson
00023 
00024 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
00025 associated documentation files (the "Software"), to deal in the Software without restriction,
00026 including without limitation the rights to use, copy, modify, merge, publish, distribute,
00027 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
00028 furnished to do so, subject to the following conditions:
00029 
00030 The above copyright notice and this permission notice shall be included in all copies or
00031 substantial portions of the Software.
00032 
00033 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
00034 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
00035 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
00036 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
00037 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
00038 **************************************************************************************************/
00039 
00040 #ifndef _cvc3__minisat__heap_h_
00041 #define _cvc3__minisat__heap_h_
00042 
00043 //=================================================================================================
00044 
00045 #include "debug.h"
00046 #include <iostream>
00047 
00048 // provides a heap over ints
00049 
00050 namespace MiniSat {
00051 
00052 
00053 static inline int left  (int i) { return i+i; }
00054 static inline int right (int i) { return i+i + 1; }
00055 static inline int parent(int i) { return i >> 1; }
00056 
00057 template<class C>
00058 class Heap {
00059 public:
00060   C        comp;
00061   vec<int> heap;     // heap of ints
00062   vec<int> indices;  // int -> index in heap
00063   
00064   inline void percolateUp(int i)
00065   {
00066     int x = heap[i];
00067     while (parent(i) != 0 && comp(x,heap[parent(i)])){
00068       heap[i]          = heap[parent(i)];
00069       indices[heap[i]] = i;
00070       i                = parent(i);
00071     }
00072     heap   [i] = x;
00073     indices[x] = i;
00074   }
00075   
00076   inline void percolateDown(int i)
00077   {
00078     int x = heap[i];
00079     while (left(i) < heap.size()){
00080       int child = right(i) < heap.size() && comp(heap[right(i)],heap[left(i)]) ? right(i) : left(i);
00081       if (!comp(heap[child],x)) break;
00082       heap[i]          = heap[child];
00083       indices[heap[i]] = i;
00084       i                = child;
00085     }
00086     heap   [i] = x;
00087     indices[x] = i;
00088     }
00089   
00090   bool ok(int n) { return n >= 0 && n < (int)indices.size(); }
00091 
00092 public:
00093   Heap(C c) : comp(c) { heap.push(-1); }
00094   
00095   void setBounds (int size) { DebugAssert(size >= 0, "MiniSat::Heap::setBounds"); indices.growTo(size,0); }
00096   bool inHeap    (int n)    { DebugAssert(ok(n), "MiniSat::Heap::inHeap"); return indices[n] != 0; }
00097 
00098   void increase  (int n){
00099     DebugAssert(ok(n), "MiniSat::Heap::increase: ok");
00100     DebugAssert(inHeap(n), "MiniSat::Heap::increase: inHeap");
00101     percolateUp(indices[n]);
00102   }
00103 
00104   bool empty     ()         { return heap.size() == 1; }
00105   
00106   void insert(int n) {
00107     DebugAssert(n > 0, "MiniSat::Heap::insert: inserting invalid var id");
00108     if (!inHeap(n)) {
00109       DebugAssert(ok(n), "MiniSat::Heap::insert: ok");
00110       indices[n] = heap.size();
00111       heap.push(n);
00112       percolateUp(indices[n]);
00113     }
00114   }
00115   
00116   int getMin() {
00117     int r            = heap[1];
00118     DebugAssert(r > 0, "MiniSatHeap:getmin: invalid var id");
00119     heap[1]          = heap.last();
00120     indices[heap[1]] = 1;
00121     indices[r]       = 0;
00122     heap.pop();
00123     if (heap.size() > 1)
00124       percolateDown(1);
00125     return r; }
00126   
00127   bool heapProperty() {
00128     return heapProperty(1); }
00129   
00130   bool heapProperty(int i) {
00131     return (size_t)i >= heap.size()
00132       || ((parent(i) == 0 || !comp(heap[i],heap[parent(i)])) && heapProperty(left(i)) && heapProperty(right(i))); }
00133 };
00134 
00135 }
00136 
00137 //=================================================================================================
00138 #endif

Generated on Wed Nov 18 16:13:30 2009 for CVC3 by  doxygen 1.5.2