arena.h File Reference

#include "reference.h"
#include "stack.h"
#include "utilities.h"
#include "global.h"

Include dependency graph for arena.h:

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

Go to the source code of this file.

Macros
#define	LD_MAX_ARENA_32   (29 - (unsigned) sizeof (ward) / 4)
#define	LD_MAX_ARENA   ((sizeof (word) == 4) ? LD_MAX_ARENA_32 : LD_MAX_REF)
#define	MAX_ARENA   ((size_t) 1 << LD_MAX_ARENA)

Functions
typedef	STACK (ward) arena
reference	kissat_allocate_clause (struct kissat *, size_t size)
void	kissat_shrink_arena (struct kissat *)

Variables
ABC_NAMESPACE_HEADER_START typedef word	ward

Macro Definition Documentation

LD_MAX_ARENA

#define LD_MAX_ARENA   ((sizeof (word) == 4) ? LD_MAX_ARENA_32 : LD_MAX_REF)

Definition at line 19 of file arena.h.

LD_MAX_ARENA_32

#define LD_MAX_ARENA_32   (29 - (unsigned) sizeof (ward) / 4)

Definition at line 17 of file arena.h.

MAX_ARENA

#define MAX_ARENA   ((size_t) 1 << LD_MAX_ARENA)

Definition at line 21 of file arena.h.

Function Documentation

kissat_allocate_clause()

reference kissat_allocate_clause	(	struct 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

(

struct 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);
}

STACK()

typedef STACK

(

ward

)

Variable Documentation

ward

ABC_NAMESPACE_HEADER_START typedef word ward

Definition at line 12 of file arena.h.