63 lines
2.1 KiB
C++
63 lines
2.1 KiB
C++
|
|
/*
|
|
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
|
|
Author: Lev Nachmanson
|
|
*/
|
|
#pragma once
|
|
#include <vector>
|
|
#include "util/debug.h"
|
|
#include "util/lp/lp_utils.h"
|
|
namespace lean {
|
|
// the elements with the smallest priority are dequeued first
|
|
template <typename T>
|
|
class binary_heap_priority_queue {
|
|
std::vector<T> m_priorities;
|
|
|
|
// indexing for A starts from 1
|
|
std::vector<unsigned> m_heap; // keeps the elements of the queue
|
|
std::vector<int> m_heap_inverse; // o = m_heap[m_heap_inverse[o]]
|
|
unsigned m_heap_size = 0;
|
|
|
|
// is is the child place in heap
|
|
void swap_with_parent(unsigned i);
|
|
void put_at(unsigned i, unsigned h);
|
|
void decrease_priority(unsigned o, T newPriority);
|
|
public:
|
|
#ifdef LEAN_DEBUG
|
|
bool is_consistent() const;
|
|
#endif
|
|
public:
|
|
void remove(unsigned o);
|
|
unsigned size() const { return m_heap_size; }
|
|
binary_heap_priority_queue(): m_heap(1) {} // the empty constructror
|
|
// n is the initial queue capacity.
|
|
// The capacity will be enlarged two times automatically if needed
|
|
binary_heap_priority_queue(unsigned n);
|
|
|
|
void clear() { m_heap_size = 0; }
|
|
|
|
void resize(unsigned n);
|
|
void put_to_heap(unsigned i, unsigned o);
|
|
|
|
void enqueue_new(unsigned o, const T& priority);
|
|
|
|
// This method can work with an element that is already in the queue.
|
|
// In this case the priority will be changed and the queue adjusted.
|
|
void enqueue(unsigned o, const T & priority);
|
|
void change_priority_for_existing(unsigned o, const T & priority);
|
|
T get_priority(unsigned o) const { return m_priorities[o]; }
|
|
bool is_empty() const { return m_heap_size == 0; }
|
|
|
|
/// return the first element of the queue and removes it from the queue
|
|
unsigned dequeue_and_get_priority(T & priority);
|
|
void fix_heap_under(unsigned i);
|
|
void put_the_last_at_the_top_and_fix_the_heap();
|
|
/// return the first element of the queue and removes it from the queue
|
|
unsigned dequeue();
|
|
#ifdef LEAN_DEBUG
|
|
void print(std::ostream & out);
|
|
#endif
|
|
};
|
|
}
|