vector.h File Reference

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

Include dependency graph for vector.h:

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

Go to the source code of this file.

Classes
struct	vectors
struct	vector

Macros
#define	LD_MAX_VECTORS   (sizeof (word) == 8 ? 32u : 28u)
#define	MAX_VECTORS   (((uint64_t) 1) << LD_MAX_VECTORS)
#define	INVALID_VECTOR_ELEMENT   UINT_MAX
#define	MAX_SECTOR   MAX_SIZE_T
#define	kissat_check_vectors(...)

Typedefs
typedef struct vector	vector
typedef struct vectors	vectors

Functions
unsigned *	kissat_enlarge_vector (struct kissat *, vector *)
void	kissat_defrag_vectors (struct kissat *, size_t, vector *)
void	kissat_remove_from_vector (struct kissat *, vector *, unsigned)
void	kissat_resize_vector (struct kissat *, vector *, size_t)
void	kissat_release_vectors (struct kissat *)

Macro Definition Documentation

INVALID_VECTOR_ELEMENT

#define INVALID_VECTOR_ELEMENT   UINT_MAX

Definition at line 20 of file vector.h.

kissat_check_vectors

#define kissat_check_vectors

(

...

)

Value:

  do { \
  } while (0)

Definition at line 47 of file vector.h.

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

LD_MAX_VECTORS

#define LD_MAX_VECTORS   (sizeof (word) == 8 ? 32u : 28u)

Definition at line 13 of file vector.h.

MAX_SECTOR

#define MAX_SECTOR   MAX_SIZE_T

Definition at line 22 of file vector.h.

MAX_VECTORS

#define MAX_VECTORS   (((uint64_t) 1) << LD_MAX_VECTORS)

Definition at line 18 of file vector.h.

Typedef Documentation

vector

typedef struct vector vector

Definition at line 24 of file vector.h.

vectors

typedef struct vectors vectors

Definition at line 25 of file vector.h.

Function Documentation

kissat_defrag_vectors()

void kissat_defrag_vectors	(	struct kissat *	solver,
		size_t	size_unsorted,
		vector *	unsorted )

Definition at line 161 of file vector.c.

                                              {
  unsigneds *stack = &solver->vectors.stack;
  const size_t size_vectors = SIZE_STACK (*stack);
  if (size_vectors < 2)
    return;
  START (defrag);
  INC (defragmentations);
  LOG ("defragmenting vectors size %zu capacity %zu usable %zu",
       size_vectors, CAPACITY_STACK (*stack), solver->vectors.usable);
  size_t bytes = size_unsorted * sizeof (unsigned);
  unsigned *sorted = (unsigned*)kissat_malloc (solver, bytes);
  unsigned size_sorted = 0;
  for (unsigned i = 0; i < size_unsorted; i++) {
    vector *vector = unsorted + i;
    if (kissat_empty_vector (vector))
#ifdef KISSAT_COMPACT
      vector->offset = 0;
#else
      vector->begin = vector->end = 0;
#endif
    else
      sorted[size_sorted++] = i;
  }
  RADIX_SORT (unsigned, rank, size_sorted, sorted, RANK_OFFSET);
  unsigned *old_begin_stack = BEGIN_STACK (*stack);
  unsigned *p = old_begin_stack + 1;
  for (unsigned i = 0; i < size_sorted; i++) {
    unsigned j = sorted[i];
    vector *vector = unsorted + j;
    const size_t size = kissat_size_vector (vector);
    unsigned *new_end_of_vector = p + size;
#ifdef KISSAT_COMPACT
    const unsigned old_offset = vector->offset;
    const unsigned new_offset = p - old_begin_stack;
    KISSAT_assert (new_offset <= old_offset);
    vector->offset = new_offset;
    const unsigned *const q = old_begin_stack + old_offset;
#else
    if (!size) {
      vector->begin = vector->end = 0;
      continue;
    }
    const unsigned *const q = vector->begin;
    vector->begin = p;
    vector->end = new_end_of_vector;
#endif
    KISSAT_assert (MAX_SIZE_T / sizeof (unsigned) >= size);
    memmove (p, q, size * sizeof (unsigned));
    p = new_end_of_vector;
  }
  kissat_free (solver, sorted, bytes);
#ifndef KISSAT_QUIET
  const size_t freed = END_STACK (*stack) - p;
  double freed_fraction = kissat_percent (freed, size_vectors);
  kissat_phase (solver, "defrag", GET (defragmentations),
                "freed %zu usable entries %.0f%% thus %s", freed,
                freed_fraction, FORMAT_BYTES (freed * sizeof (unsigned)));
  KISSAT_assert (freed == solver->vectors.usable);
#endif
  SET_END_OF_STACK (*stack, p);
#ifndef KISSAT_COMPACT
  KISSAT_assert (old_begin_stack == BEGIN_STACK (*stack));
#endif
  SHRINK_STACK (*stack);
#ifndef KISSAT_COMPACT
  unsigned *new_begin_stack = BEGIN_STACK (*stack);
  const ptrdiff_t moved =
      (char *) new_begin_stack - (char *) old_begin_stack;
  if (moved)
    fix_vector_pointers_after_moving_stack (solver, moved);
#endif
  solver->vectors.usable = 0;
  kissat_check_vectors (solver);
  STOP (defrag);
}

Here is the call graph for this function:

kissat_enlarge_vector()

unsigned * kissat_enlarge_vector	(	struct kissat *	solver,
		vector *	vector )

Definition at line 45 of file vector.c.

                                                                 {
  unsigneds *stack = &solver->vectors.stack;
  const size_t old_vector_size = kissat_size_vector (vector);
#ifdef LOGGING
  const size_t old_offset = kissat_offset_vector (solver, vector);
  LOG2 ("enlarging vector %zu[%zu] at %p", old_offset, old_vector_size,
        (void *) vector);
#endif
  KISSAT_assert (old_vector_size < MAX_VECTORS / 2);
  const size_t new_vector_size = old_vector_size ? 2 * old_vector_size : 1;
  size_t old_stack_size = SIZE_STACK (*stack);
  size_t capacity = CAPACITY_STACK (*stack);
  KISSAT_assert (kissat_is_power_of_two (MAX_VECTORS));
  KISSAT_assert (capacity <= MAX_VECTORS);
  size_t available = capacity - old_stack_size;
  if (new_vector_size > available) {
#if !defined(KISSAT_QUIET) || !defined(KISSAT_COMPACT)
    unsigned *old_begin_stack = BEGIN_STACK (*stack);
#endif
    unsigned enlarged = 0;
    do {
      KISSAT_assert (kissat_is_zero_or_power_of_two (capacity));
 
      if (capacity == MAX_VECTORS)
        kissat_fatal ("maximum vector stack size "
                      "of 2^%u entries %s exhausted",
                      LD_MAX_VECTORS,
                      FORMAT_BYTES (MAX_VECTORS * sizeof (unsigned)));
      enlarged++;
      kissat_stack_enlarge (solver, (chars *) stack, sizeof (unsigned));
 
      capacity = CAPACITY_STACK (*stack);
      available = capacity - old_stack_size;
    } while (new_vector_size > available);
 
    if (enlarged) {
      INC (vectors_enlarged);
#if !defined(KISSAT_QUIET) || !defined(KISSAT_COMPACT)
      unsigned *new_begin_stack = BEGIN_STACK (*stack);
      const ptrdiff_t moved =
          (char *) new_begin_stack - (char *) old_begin_stack;
#endif
#ifndef KISSAT_QUIET
      kissat_phase (solver, "vectors", GET (vectors_enlarged),
                    "enlarged to %s entries %s (%s)",
                    FORMAT_COUNT (capacity),
                    FORMAT_BYTES (capacity * sizeof (unsigned)),
                    (moved ? "moved" : "in place"));
#endif
#ifndef KISSAT_COMPACT
      if (moved)
        fix_vector_pointers_after_moving_stack (solver, moved);
#endif
    }
    KISSAT_assert (capacity <= MAX_VECTORS);
    KISSAT_assert (new_vector_size <= available);
  }
  unsigned *begin_old_vector = kissat_begin_vector (solver, vector);
  unsigned *begin_new_vector = END_STACK (*stack);
  unsigned *middle_new_vector = begin_new_vector + old_vector_size;
  unsigned *end_new_vector = begin_new_vector + new_vector_size;
  KISSAT_assert (end_new_vector <= stack->allocated);
  const size_t old_bytes = old_vector_size * sizeof (unsigned);
  const size_t delta_size = new_vector_size - old_vector_size;
  KISSAT_assert (MAX_SIZE_T / sizeof (unsigned) >= delta_size);
  const size_t delta_bytes = delta_size * sizeof (unsigned);
  if (old_bytes) {
    memcpy (begin_new_vector, begin_old_vector, old_bytes);
    memset (begin_old_vector, 0xff, old_bytes);
  }
  solver->vectors.usable += old_vector_size;
  kissat_add_usable (solver, delta_size);
  if (delta_bytes)
    memset (middle_new_vector, 0xff, delta_bytes);
#ifdef KISSAT_COMPACT
  const uint64_t offset = SIZE_STACK (*stack);
  KISSAT_assert (offset <= MAX_VECTORS);
  vector->offset = offset;
  LOG2 ("enlarged vector at %p to %u[%u]", (void *) vector, vector->offset,
        vector->size);
#else
  vector->begin = begin_new_vector;
  vector->end = middle_new_vector;
#ifdef LOGGING
  const size_t new_offset = vector->begin - stack->begin;
  LOG2 ("enlarged vector at %p to %zu[%zu]", (void *) vector, new_offset,
        old_vector_size);
#endif
#endif
  stack->end = end_new_vector;
  KISSAT_assert (begin_new_vector < end_new_vector);
  KISSAT_assert (kissat_size_vector (vector) == old_vector_size);
  return middle_new_vector;
}

Here is the call graph for this function:

kissat_release_vectors()

void kissat_release_vectors

(

struct kissat *

solver

)

Definition at line 284 of file vector.c.

                                             {
  RELEASE_STACK (solver->vectors.stack);
  solver->vectors.usable = 0;
}

Here is the caller graph for this function:

kissat_remove_from_vector()

void kissat_remove_from_vector	(	struct kissat *	solver,
		vector *	vector,
		unsigned	remove )

Definition at line 238 of file vector.c.

                                                 {
  unsigned *begin = kissat_begin_vector (solver, vector), *p = begin;
  const unsigned *const end = kissat_end_vector (solver, vector);
  KISSAT_assert (p != end);
  while (*p != remove)
    p++, KISSAT_assert (p != end);
  while (++p != end)
    p[-1] = *p;
  p[-1] = INVALID_VECTOR_ELEMENT;
#ifdef KISSAT_COMPACT
  vector->size--;
#else
  KISSAT_assert (vector->begin < vector->end);
  vector->end--;
#endif
  kissat_inc_usable (solver);
  kissat_check_vectors (solver);
#ifndef CHECK_VECTORS
  (void) solver;
#endif
}

kissat_resize_vector()

void kissat_resize_vector	(	struct kissat *	solver,
		vector *	vector,
		size_t	new_size )

Definition at line 261 of file vector.c.

                                            {
  const size_t old_size = kissat_size_vector (vector);
  KISSAT_assert (new_size <= old_size);
  if (new_size == old_size)
    return;
#ifdef KISSAT_COMPACT
  vector->size = new_size;
#else
  vector->end = vector->begin + new_size;
#endif
  unsigned *begin = kissat_begin_vector (solver, vector);
  unsigned *end = begin + new_size;
  size_t delta = old_size - new_size;
  kissat_add_usable (solver, delta);
  size_t bytes = delta * sizeof (unsigned);
  memset (end, 0xff, bytes);
  kissat_check_vectors (solver);
#ifndef CHECK_VECTORS
  (void) solver;
#endif
}

Here is the call graph for this function: