heap.h File Reference

#include "stack.h"
#include "utilities.h"
#include <assert.h>
#include <limits.h>
#include <stdbool.h>
#include "global.h"

Include dependency graph for heap.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
struct	heap

Macros
#define	DISCONTAIN   UINT_MAX
#define	DISCONTAINED(IDX)
#define	kissat_check_heap(...)

Typedefs
typedef struct heap	heap

Functions
void	kissat_resize_heap (struct kissat *, heap *, unsigned size)
void	kissat_release_heap (struct kissat *, heap *)
void	kissat_rescale_heap (struct kissat *, heap *heap, double factor)
void	kissat_enlarge_heap (struct kissat *, heap *, unsigned new_vars)

Macro Definition Documentation

DISCONTAIN

#define DISCONTAIN   UINT_MAX

Definition at line 14 of file heap.h.

DISCONTAINED

#define DISCONTAINED

(

IDX

)

Value:

((int) (IDX) < 0)

Definition at line 15 of file heap.h.

kissat_check_heap

#define kissat_check_heap

(

...

)

Value:

  do { \
  } while (0)

Definition at line 83 of file heap.h.

#define kissat_check_heap(...) \
  do { \
  } while (0)

Typedef Documentation

heap

typedef struct heap heap

Definition at line 17 of file heap.h.

Function Documentation

kissat_enlarge_heap()

void kissat_enlarge_heap	(	struct kissat *	solver,
		heap *	heap,
		unsigned	new_vars )

Definition at line 82 of file heap.c.

                                                                         {
  const unsigned old_vars = heap->vars;
  KISSAT_assert (old_vars < new_vars);
  KISSAT_assert (new_vars <= heap->size);
  const size_t delta = new_vars - heap->vars;
  memset (heap->pos + old_vars, 0xff, delta * sizeof (unsigned));
  heap->vars = new_vars;
  if (heap->tainted)
    memset (heap->score + old_vars, 0, delta * sizeof (double));
  LOG ("enlarged heap from %u to %u", old_vars, new_vars);
#ifndef LOGGING
  (void) solver;
#endif
}

Here is the call graph for this function:

kissat_release_heap()

void kissat_release_heap	(	struct kissat *	solver,
		heap *	heap )

Definition at line 10 of file heap.c.

                                                      {
  RELEASE_STACK (heap->stack);
  DEALLOC (heap->pos, heap->size);
  DEALLOC (heap->score, heap->size);
  memset (heap, 0, sizeof *heap);
}

Here is the call graph for this function:

Here is the caller graph for this function:

kissat_rescale_heap()

void kissat_rescale_heap	(	struct kissat *	solver,
		heap *	heap,
		double	factor )

Definition at line 69 of file heap.c.

                                                                     {
  LOG ("rescaling scores on heap with factor %g", factor);
  double *score = heap->score;
  for (unsigned i = 0; i < heap->vars; i++)
    score[i] *= factor;
#ifndef KISSAT_NDEBUG
  kissat_check_heap (heap);
#endif
#ifndef LOGGING
  (void) solver;
#endif
}

Here is the caller graph for this function:

kissat_resize_heap()

void kissat_resize_heap	(	struct kissat *	solver,
		heap *	heap,
		unsigned	size )

Definition at line 46 of file heap.c.

                                                                        {
  const unsigned old_size = heap->size;
  if (old_size >= new_size)
    return;
  LOG ("resizing %s heap from %u to %u",
       (heap->tainted ? "tainted" : "untainted"), old_size, new_size);
 
  heap->pos = (unsigned*)kissat_nrealloc (solver, heap->pos, old_size, new_size,
                               sizeof (unsigned));
  if (heap->tainted) {
    heap->score = (double*)kissat_nrealloc (solver, heap->score, old_size, new_size,
                                   sizeof (double));
  } else {
    if (old_size)
      DEALLOC (heap->score, old_size);
    heap->score = (double*)kissat_calloc (solver, new_size, sizeof (double));
  }
  heap->size = new_size;
#ifdef CHECK_HEAP
  kissat_check_heap (heap);
#endif
}

Here is the call graph for this function:

Here is the caller graph for this function: