arena.c File Reference

#include "error.h"
#include "internal.h"
#include "logging.h"
#include "print.h"

Include dependency graph for arena.c:

Go to the source code of this file.

Functions
reference	kissat_allocate_clause (kissat *solver, size_t size)
void	kissat_shrink_arena (kissat *solver)

Function Documentation

kissat_allocate_clause()

reference kissat_allocate_clause	(	kissat *	solver,
		size_t	size )

Definition at line 27 of file arena.c.

                                                               {
  KISSAT_assert (size <= UINT_MAX);
  const size_t res = SIZE_STACK (solver->arena);
  KISSAT_assert (res <= MAX_REF);
  const size_t bytes = kissat_bytes_of_clause (size);
  KISSAT_assert (kissat_aligned_word (bytes));
  const size_t needed = bytes / sizeof (ward);
  KISSAT_assert (needed <= UINT_MAX);
  size_t capacity = CAPACITY_STACK (solver->arena);
  KISSAT_assert (kissat_is_power_of_two (MAX_ARENA));
  KISSAT_assert (capacity <= MAX_ARENA);
  size_t available = capacity - res;
  if (needed > available) {
    const arena before = solver->arena;
    do {
      KISSAT_assert (kissat_is_zero_or_power_of_two (capacity));
      if (capacity == MAX_ARENA)
        kissat_fatal ("maximum arena capacity "
                      "of 2^%u %zu-byte-words %s exhausted"
#ifdef KISSAT_COMPACT
                      " (consider a configuration without '--compact')"
#endif
                      ,
                      LD_MAX_ARENA, sizeof (ward),
                      FORMAT_BYTES (MAX_ARENA * sizeof (ward)));
      kissat_stack_enlarge (solver, (chars *) &solver->arena,
                            sizeof (ward));
      capacity = CAPACITY_STACK (solver->arena);
      available = capacity - res;
    } while (needed > available);
    INC (arena_resized);
    INC (arena_enlarged);
    report_resized (solver, "enlarged", before);
    KISSAT_assert (capacity <= MAX_ARENA);
  }
  solver->arena.end += needed;
  LOG ("allocated clause[%zu] of size %zu bytes %s", res, size,
       FORMAT_BYTES (bytes));
  return (reference) res;
}

Here is the call graph for this function:

kissat_shrink_arena()

void kissat_shrink_arena

(

kissat *

solver

)

Definition at line 68 of file arena.c.

                                          {
  const arena before = solver->arena;
  const size_t capacity = CAPACITY_STACK (before);
  const size_t size = SIZE_STACK (before);
#ifndef KISSAT_QUIET
  const size_t capacity_bytes = capacity * sizeof (ward);
  kissat_phase (solver, "arena", GET (arena_resized),
                "capacity of %s %d-byte-words %s", FORMAT_COUNT (capacity),
                (int) sizeof (ward), FORMAT_BYTES (capacity_bytes));
  const size_t size_bytes = size * sizeof (ward);
  kissat_phase (solver, "arena", GET (arena_resized),
                "filled %.0f%% with %s %d-byte-words %s",
                kissat_percent (size, capacity), FORMAT_COUNT (size),
                (int) sizeof (ward), FORMAT_BYTES (size_bytes));
#endif
  if (size > capacity / 4) {
    kissat_phase (solver, "arena", GET (arena_resized),
                  "not shrinking since more than 25%% filled");
    return;
  }
  INC (arena_resized);
  INC (arena_shrunken);
  SHRINK_STACK (solver->arena);
  report_resized (solver, "shrunken", before);
}