resize.c File Reference

#include "resize.h"
#include "allocate.h"
#include "inline.h"
#include "require.h"
#include <limits.h>
#include <string.h>

Include dependency graph for resize.c:

Go to the source code of this file.

Macros
#define	NREALLOC_GENERIC(TYPE, NAME, ELEMENTS_PER_BLOCK)
#define	CREALLOC_GENERIC(TYPE, NAME, ELEMENTS_PER_BLOCK)
#define	NREALLOC_VARIABLE_INDEXED(TYPE, NAME)
#define	NREALLOC_LITERAL_INDEXED(TYPE, NAME)
#define	CREALLOC_VARIABLE_INDEXED(TYPE, NAME)
#define	CREALLOC_LITERAL_INDEXED(TYPE, NAME)

Functions
void	kissat_increase_size (kissat *solver, unsigned new_size)
void	kissat_decrease_size (kissat *solver)
void	kissat_enlarge_variables (kissat *solver, unsigned new_vars)

Macro Definition Documentation

CREALLOC_GENERIC

#define CREALLOC_GENERIC	(		TYPE,
			NAME,
			ELEMENTS_PER_BLOCK )

Value:

  do { \
    const size_t block_size = sizeof (TYPE); \
    TYPE *NAME = \
      (TYPE*) kissat_calloc (solver, ELEMENTS_PER_BLOCK * new_size, block_size); \
    if (old_size) { \
      const size_t bytes = ELEMENTS_PER_BLOCK * old_size * block_size; \
      memcpy (NAME, solver->NAME, bytes); \
    } \
    kissat_dealloc (solver, solver->NAME, ELEMENTS_PER_BLOCK *old_size, \
                    block_size); \
    solver->NAME = NAME; \
  } while (0)

Definition at line 19 of file resize.c.

#define CREALLOC_GENERIC(TYPE, NAME, ELEMENTS_PER_BLOCK) \
  do { \
    const size_t block_size = sizeof (TYPE); \
    TYPE *NAME = \
      (TYPE*) kissat_calloc (solver, ELEMENTS_PER_BLOCK * new_size, block_size); \
    if (old_size) { \
      const size_t bytes = ELEMENTS_PER_BLOCK * old_size * block_size; \
      memcpy (NAME, solver->NAME, bytes); \
    } \
    kissat_dealloc (solver, solver->NAME, ELEMENTS_PER_BLOCK *old_size, \
                    block_size); \
    solver->NAME = NAME; \
  } while (0)

CREALLOC_LITERAL_INDEXED

#define CREALLOC_LITERAL_INDEXED	(		TYPE,
			NAME )

Value:

  CREALLOC_GENERIC (TYPE, NAME, 2)

Definition at line 42 of file resize.c.

#define CREALLOC_LITERAL_INDEXED(TYPE, NAME) \
  CREALLOC_GENERIC (TYPE, NAME, 2)

CREALLOC_VARIABLE_INDEXED

#define CREALLOC_VARIABLE_INDEXED	(		TYPE,
			NAME )

Value:

  CREALLOC_GENERIC (TYPE, NAME, 1)

Definition at line 39 of file resize.c.

#define CREALLOC_VARIABLE_INDEXED(TYPE, NAME) \
  CREALLOC_GENERIC (TYPE, NAME, 1)

NREALLOC_GENERIC

#define NREALLOC_GENERIC	(		TYPE,
			NAME,
			ELEMENTS_PER_BLOCK )

Value:

  do { \
    const size_t block_size = sizeof (TYPE); \
    solver->NAME = \
      (TYPE*) kissat_nrealloc (solver, solver->NAME, old_size, new_size,      \
                         ELEMENTS_PER_BLOCK * block_size); \
  } while (0)

Definition at line 11 of file resize.c.

#define NREALLOC_GENERIC(TYPE, NAME, ELEMENTS_PER_BLOCK) \
  do { \
    const size_t block_size = sizeof (TYPE); \
    solver->NAME = \
      (TYPE*) kissat_nrealloc (solver, solver->NAME, old_size, new_size,      \
                         ELEMENTS_PER_BLOCK * block_size); \
  } while (0)

NREALLOC_LITERAL_INDEXED

#define NREALLOC_LITERAL_INDEXED	(		TYPE,
			NAME )

Value:

  NREALLOC_GENERIC (TYPE, NAME, 2)

Definition at line 36 of file resize.c.

#define NREALLOC_LITERAL_INDEXED(TYPE, NAME) \
  NREALLOC_GENERIC (TYPE, NAME, 2)

NREALLOC_VARIABLE_INDEXED

#define NREALLOC_VARIABLE_INDEXED	(		TYPE,
			NAME )

Value:

  NREALLOC_GENERIC (TYPE, NAME, 1)

Definition at line 33 of file resize.c.

#define NREALLOC_VARIABLE_INDEXED(TYPE, NAME) \
  NREALLOC_GENERIC (TYPE, NAME, 1)

Function Documentation

kissat_decrease_size()

void kissat_decrease_size

(

kissat *

solver

)

Definition at line 82 of file resize.c.

                                           {
  const unsigned old_size = solver->size;
  const unsigned new_size = solver->vars;
 
#ifdef METRICS
  LOG ("%s before decreasing size from %u to %u",
       FORMAT_BYTES (kissat_allocated (solver)), old_size, new_size);
#endif
 
  NREALLOC_VARIABLE_INDEXED (assigned, assigned);
  NREALLOC_VARIABLE_INDEXED (flags, flags);
  NREALLOC_VARIABLE_INDEXED (links, links);
 
  NREALLOC_LITERAL_INDEXED (mark, marks);
  NREALLOC_LITERAL_INDEXED (value, values);
  NREALLOC_LITERAL_INDEXED (watches, watches);
 
  reallocate_trail (solver, old_size, new_size);
  kissat_resize_heap (solver, SCORES, new_size);
  kissat_decrease_phases (solver, new_size);
 
  solver->size = new_size;
 
#ifdef METRICS
  LOG ("%s after decreasing size from %u to %u",
       FORMAT_BYTES (kissat_allocated (solver)), old_size, new_size);
#endif
}

Here is the call graph for this function:

Here is the caller graph for this function:

kissat_enlarge_variables()

void kissat_enlarge_variables	(	kissat *	solver,
		unsigned	new_vars )

Definition at line 111 of file resize.c.

                                                                  {
  if (solver->vars >= new_vars)
    return;
  KISSAT_assert (new_vars <= INTERNAL_MAX_VAR + 1);
  LOG ("enlarging variables from %u to %u", solver->vars, new_vars);
  const size_t old_size = solver->size;
  if (old_size < new_vars) {
    LOG ("old size %zu below requested new number of variables %u",
         old_size, new_vars);
    size_t new_size;
    if (!old_size)
      new_size = new_vars;
    else {
      if (kissat_is_power_of_two (old_size)) {
        KISSAT_assert (old_size <= UINT_MAX / 2);
        new_size = 2 * old_size;
      } else {
        KISSAT_assert (1 < old_size);
        new_size = 2;
      }
      while (new_size < new_vars) {
        KISSAT_assert (new_size <= UINT_MAX / 2);
        new_size *= 2;
      }
    }
    kissat_increase_size (solver, new_size);
  }
  solver->vars = new_vars;
}

Here is the call graph for this function:

kissat_increase_size()

void kissat_increase_size	(	kissat *	solver,
		unsigned	new_size )

Definition at line 52 of file resize.c.

                                                              {
  KISSAT_assert (solver->vars <= new_size);
  const unsigned old_size = solver->size;
  if (old_size >= new_size)
    return;
 
#ifdef METRICS
  LOG ("%s before increasing size from %u to %u",
       FORMAT_BYTES (kissat_allocated (solver)), old_size, new_size);
#endif
  CREALLOC_VARIABLE_INDEXED (struct assigned, assigned);
  CREALLOC_VARIABLE_INDEXED (struct flags, flags);
  NREALLOC_VARIABLE_INDEXED (struct links, links);
 
  CREALLOC_LITERAL_INDEXED (mark, marks);
  CREALLOC_LITERAL_INDEXED (value, values);
  CREALLOC_LITERAL_INDEXED (struct vector, watches);
 
  reallocate_trail (solver, old_size, new_size);
  kissat_resize_heap (solver, SCORES, new_size);
  kissat_increase_phases (solver, new_size);
 
  solver->size = new_size;
 
#ifdef METRICS
  LOG ("%s after increasing size from %u to %u",
       FORMAT_BYTES (kissat_allocated (solver)), old_size, new_size);
#endif
}

Here is the call graph for this function:

Here is the caller graph for this function: