resize.h File Reference

#include "global.h"

Include dependency graph for resize.h:

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

Go to the source code of this file.

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

Function Documentation

kissat_decrease_size()

void kissat_decrease_size

(

struct 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	(	struct 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	(	struct 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: