1/******************************************************************************************[Heap.h]2Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson3Copyright (c) 2007-2010, Niklas Sorensson45Permission is hereby granted, free of charge, to any person obtaining a copy of this software and6associated documentation files (the "Software"), to deal in the Software without restriction,7including without limitation the rights to use, copy, modify, merge, publish, distribute,8sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is9furnished to do so, subject to the following conditions:1011The above copyright notice and this permission notice shall be included in all copies or12substantial portions of the Software.1314THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT15NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND16NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,17DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT18OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.19**************************************************************************************************/2021package solver2223// A heap implementation with support for decrease/increase key. This is24// strongly inspired from Minisat's mtl/Heap.h.2526type queue struct {27 activity []float64 // Activity of each variable. This should be the solver's slice, not a copy.28 content []int // Actual content.29 indices []int // Reverse queue, i.e position of each item in content; -1 means absence.30}3132func newQueue(activity []float64) queue {33 q := queue{34 activity: activity,35 }36 for i := range q.activity {37 q.insert(i)38 }39 return q40}4142func (q *queue) lt(i, j int) bool {43 return q.activity[i] > q.activity[j]44}4546// Traversal functions.47func left(i int) int { return i*2 + 1 }48func right(i int) int { return (i + 1) * 2 }49func parent(i int) int { return (i - 1) >> 1 }5051func (q *queue) percolateUp(i int) {52 x := q.content[i]53 p := parent(i)54 for i != 0 && q.lt(x, q.content[p]) {55 q.content[i] = q.content[p]56 q.indices[q.content[p]] = i57 i = p58 p = parent(p)59 }60 q.content[i] = x61 q.indices[x] = i62}6364func (q *queue) percolateDown(i int) {65 x := q.content[i]66 for left(i) < len(q.content) {67 var child int68 if right(i) < len(q.content) && q.lt(q.content[right(i)], q.content[left(i)]) {69 child = right(i)70 } else {71 child = left(i)72 }73 if !q.lt(q.content[child], x) {74 break75 }76 q.content[i] = q.content[child]77 q.indices[q.content[i]] = i78 i = child79 }80 q.content[i] = x81 q.indices[x] = i82}8384func (q *queue) empty() bool { return len(q.content) == 0 }8586func (q *queue) contains(n int) bool {87 return n < len(q.indices) && q.indices[n] >= 088}8990func (q *queue) decrease(n int) {91 q.percolateUp(q.indices[n])92}9394func (q *queue) insert(n int) {95 for i := len(q.indices); i <= n; i++ {96 q.indices = append(q.indices, -1)97 }98 q.indices[n] = len(q.content)99 q.content = append(q.content, n)100 q.percolateUp(q.indices[n])101}102103func (q *queue) removeMin() int {104 x := q.content[0]105 q.content[0] = q.content[len(q.content)-1]106 q.indices[q.content[0]] = 0107 q.indices[x] = -1108 q.content = q.content[:len(q.content)-1]109 if len(q.content) > 1 {110 q.percolateDown(0)111 }112 return x113}114115// Rebuild the heap from scratch, using the elements in 'ns':116func (q *queue) build(ns []int) {117 for i := range q.content {118 q.indices[q.content[i]] = -1119 }120 q.content = q.content[:0]121 for i, val := range ns {122 q.indices[val] = i123 q.content = append(q.content, val)124 }125 for i := len(q.content)/2 - 1; i >= 0; i-- {126 q.percolateDown(i)127 }128}