heap.h

Go to the documentation of this file.

#ifndef _heap_h_INCLUDED
#define _heap_h_INCLUDED
 
#include "stack.h"
#include "utilities.h"
 
#include <assert.h>
#include <limits.h>
#include <stdbool.h>
 
#include "global.h"
ABC_NAMESPACE_HEADER_START
 
#define DISCONTAIN UINT_MAX
#define DISCONTAINED(IDX) ((int) (IDX) < 0)
 
typedef struct heap heap;
 
struct heap {
  bool tainted;
  unsigned vars;
  unsigned size;
  unsigneds stack;
  double *score;
  unsigned *pos;
};
 
struct kissat;
 
void kissat_resize_heap (struct kissat *, heap *, unsigned size);
void kissat_release_heap (struct kissat *, heap *);
 
static inline bool kissat_heap_contains (heap *heap, unsigned idx) {
  return idx < heap->vars && !DISCONTAINED (heap->pos[idx]);
}
 
static inline unsigned kissat_get_heap_pos (const heap *heap,
                                            unsigned idx) {
  return idx < heap->vars ? heap->pos[idx] : DISCONTAIN;
}
 
static inline double kissat_get_heap_score (const heap *heap,
                                            unsigned idx) {
  return idx < heap->vars ? heap->score[idx] : 0.0;
}
 
static inline bool kissat_empty_heap (heap *heap) {
  return EMPTY_STACK (heap->stack);
}
 
static inline size_t kissat_size_heap (heap *heap) {
  return SIZE_STACK (heap->stack);
}
 
static inline unsigned kissat_max_heap (heap *heap) {
  KISSAT_assert (!kissat_empty_heap (heap));
  return PEEK_STACK (heap->stack, 0);
}
 
void kissat_rescale_heap (struct kissat *, heap *heap, double factor);
 
void kissat_enlarge_heap (struct kissat *, heap *, unsigned new_vars);
 
static inline double kissat_max_score_on_heap (heap *heap) {
  if (!heap->tainted)
    return 0;
  KISSAT_assert (heap->vars);
  const double *const score = heap->score;
  const double *const end = score + heap->vars;
  double res = score[0];
  for (const double *p = score + 1; p != end; p++)
    res = MAX (res, *p);
  return res;
}
 
#ifndef KISSAT_NDEBUG
void kissat_dump_heap (heap *);
#endif
 
#ifndef KISSAT_NDEBUG
void kissat_check_heap (heap *);
#else
#define kissat_check_heap(...) \
  do { \
  } while (0)
#endif
 
ABC_NAMESPACE_HEADER_END
 
#endif