inlineheap.h

Go to the documentation of this file.

#ifndef _inlineheap_h_INCLUDED
#define _inlineheap_h_INCLUDED
 
#include "allocate.h"
#include "internal.h"
#include "logging.h"
 
#include "global.h"
ABC_NAMESPACE_HEADER_START
 
#define HEAP_CHILD(POS) (KISSAT_assert ((POS) < (1u << 31)), (2 * (POS) + 1))
 
#define HEAP_PARENT(POS) (KISSAT_assert ((POS) > 0), (((POS) - 1) / 2))
 
static inline void kissat_bubble_up (kissat *solver, heap *heap,
                                     unsigned idx) {
  unsigned *stack = BEGIN_STACK (heap->stack);
  unsigned *pos = heap->pos;
  unsigned idx_pos = pos[idx];
  const double *const score = heap->score;
  const double idx_score = score[idx];
  while (idx_pos) {
    const unsigned parent_pos = HEAP_PARENT (idx_pos);
    const unsigned parent = stack[parent_pos];
    if (score[parent] >= idx_score)
      break;
    LOG ("heap bubble up: %u@%u = %g swapped with %u@%u = %g", parent,
         parent_pos, score[parent], idx, idx_pos, idx_score);
    stack[idx_pos] = parent;
    pos[parent] = idx_pos;
    idx_pos = parent_pos;
  }
  stack[idx_pos] = idx;
  pos[idx] = idx_pos;
#ifndef LOGGING
  (void) solver;
#endif
}
 
static inline void kissat_bubble_down (kissat *solver, heap *heap,
                                       unsigned idx) {
  unsigned *stack = BEGIN_STACK (heap->stack);
  const unsigned end = SIZE_STACK (heap->stack);
  unsigned *pos = heap->pos;
  unsigned idx_pos = pos[idx];
  const double *const score = heap->score;
  const double idx_score = score[idx];
  for (;;) {
    unsigned child_pos = HEAP_CHILD (idx_pos);
    if (child_pos >= end)
      break;
    unsigned child = stack[child_pos];
    double child_score = score[child];
    const unsigned sibling_pos = child_pos + 1;
    if (sibling_pos < end) {
      const unsigned sibling = stack[sibling_pos];
      const double sibling_score = score[sibling];
      if (sibling_score > child_score) {
        child = sibling;
        child_pos = sibling_pos;
        child_score = sibling_score;
      }
    }
    if (child_score <= idx_score)
      break;
    LOG ("heap bubble down: %u@%u = %g swapped with %u@%u = %g", child,
         child_pos, score[child], idx, idx_pos, idx_score);
    stack[idx_pos] = child;
    pos[child] = idx_pos;
    idx_pos = child_pos;
  }
  stack[idx_pos] = idx;
  pos[idx] = idx_pos;
#ifndef LOGGING
  (void) solver;
#endif
}
 
#define HEAP_IMPORT(IDX) \
  do { \
    KISSAT_assert ((IDX) < UINT_MAX - 1); \
    if (heap->vars <= (IDX)) \
      kissat_enlarge_heap (solver, heap, (IDX) + 1); \
  } while (0)
 
#define CHECK_HEAP_IMPORTED(IDX)
 
static inline void kissat_push_heap (kissat *solver, heap *heap,
                                     unsigned idx) {
  LOG ("push heap %u", idx);
  KISSAT_assert (!kissat_heap_contains (heap, idx));
  HEAP_IMPORT (idx);
  heap->pos[idx] = SIZE_STACK (heap->stack);
  PUSH_STACK (heap->stack, idx);
  kissat_bubble_up (solver, heap, idx);
}
 
static inline void kissat_pop_heap (kissat *solver, heap *heap,
                                    unsigned idx) {
  LOG ("pop heap %u", idx);
  KISSAT_assert (kissat_heap_contains (heap, idx));
  const unsigned last = POP_STACK (heap->stack);
  heap->pos[last] = DISCONTAIN;
  if (last == idx)
    return;
  const unsigned idx_pos = heap->pos[idx];
  heap->pos[idx] = DISCONTAIN;
  POKE_STACK (heap->stack, idx_pos, last);
  heap->pos[last] = idx_pos;
  kissat_bubble_up (solver, heap, last);
  kissat_bubble_down (solver, heap, last);
#ifdef CHECK_HEAP
  kissat_check_heap (heap);
#endif
}
 
static inline unsigned kissat_pop_max_heap (kissat *solver, heap *heap) {
  KISSAT_assert (!EMPTY_STACK (heap->stack));
  unsigneds *stack = &heap->stack;
  unsigned *const begin = BEGIN_STACK (*stack);
  const unsigned idx = *begin;
  KISSAT_assert (!heap->pos[idx]);
  LOG ("pop max heap %u", idx);
  const unsigned last = POP_STACK (*stack);
  unsigned *const pos = heap->pos;
  pos[last] = DISCONTAIN;
  if (last == idx)
    return idx;
  pos[idx] = DISCONTAIN;
  *begin = last;
  pos[last] = 0;
  kissat_bubble_down (solver, heap, last);
#ifdef CHECK_HEAP
  kissat_check_heap (heap);
#endif
  return idx;
}
 
static inline void kissat_adjust_heap (kissat *solver, heap *heap,
                                       unsigned idx) {
  const unsigned new_vars = idx + 1;
  const unsigned old_vars = heap->vars;
  if (new_vars <= old_vars)
    return;
  const unsigned old_size = heap->size;
  if (idx >= old_size) {
    size_t new_size = old_size ? 2 * old_size : 1;
    while (idx >= new_size)
      new_size *= 2;
    KISSAT_assert (new_size < DISCONTAIN);
    kissat_resize_heap (solver, heap, new_size);
  }
  kissat_enlarge_heap (solver, heap, idx + 1);
}
 
static inline void kissat_update_heap (kissat *solver, heap *heap,
                                       unsigned idx, double new_score) {
  const double old_score = kissat_get_heap_score (heap, idx);
  if (old_score == new_score)
    return;
  HEAP_IMPORT (idx);
  LOG ("update heap %u score from %g to %g", idx, old_score, new_score);
  heap->score[idx] = new_score;
  if (!heap->tainted) {
    heap->tainted = true;
    LOG ("tainted heap");
  }
  if (!kissat_heap_contains (heap, idx))
    return;
  if (new_score > old_score)
    kissat_bubble_up (solver, heap, idx);
  else
    kissat_bubble_down (solver, heap, idx);
#ifdef CHECK_HEAP
  kissat_check_heap (heap);
#endif
}
 
ABC_NAMESPACE_HEADER_END
 
#endif