#include <stdbool.h>
#include <stdint.h>
#include "global.h"
#include <inttypes.h>

Include dependency graph for kimits.h:

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

Classes
struct	bounds

struct	limits

struct	limited

struct	enabled

struct	delay

struct	delays

struct	remember

Macros
#define	LOGN(COUNT)

#define	LINEAR(COUNT)

#define	NLOGN(COUNT)

#define	NLOG2N(COUNT)

#define	NLOG3N(COUNT)

#define	SQRT(COUNT)

#define	UPDATE_CONFLICT_LIMIT(NAME, COUNT, SCALE_COUNT_FUNCTION, SCALE_DELTA)

#define	SET_EFFORT_LIMIT(LIMIT, NAME, START)

#define	DELAYING(NAME)

#define	BUMP_DELAY(NAME)

#define	REDUCE_DELAY(NAME)

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct bounds	bounds

typedef struct changes	changes

typedef struct delays	delays

typedef struct delay	delay

typedef struct remember	remember

typedef struct enabled	enabled

typedef struct limited	limited

typedef struct limits	limits

Functions
changes	kissat_changes (struct kissat *)

bool	kissat_changed (changes before, changes after)

void	kissat_init_limits (struct kissat *)

uint64_t	kissat_scale_delta (struct kissat , const char , uint64_t)

double	kissat_nlogpown (uint64_t, unsigned)

double	kissat_sqrt (uint64_t)

double	kissat_logn (uint64_t)

bool	kissat_delaying (struct kissat , delay )

void	kissat_bump_delay (struct kissat , delay )

void	kissat_reduce_delay (struct kissat , delay )

Macro Definition Documentation

◆ BUMP_DELAY

#define BUMP_DELAY ( NAME )

Value:

kissat_bump_delay (solver, &solver->delays.NAME)

kissat_bump_delay

void kissat_bump_delay(kissat *solver, delay *delay)

Definition kimits.c:170

solver

#define solver

Definition kitten.c:211

Definition at line 183 of file kimits.h.

◆ DELAYING

#define DELAYING ( NAME )

Value:

kissat_delaying (solver, &solver->delays.NAME)

kissat_delaying

bool kissat_delaying(kissat *solver, delay *delay)

Definition kimits.c:181

Definition at line 181 of file kimits.h.

◆ LINEAR

#define LINEAR ( COUNT )

Value:

(COUNT)

Definition at line 108 of file kimits.h.

◆ LOGN

#define LOGN ( COUNT )

Value:

kissat_logn (COUNT)

kissat_logn

ABC_NAMESPACE_IMPL_START double kissat_logn(uint64_t count)

Definition kimits.c:15

Definition at line 107 of file kimits.h.

◆ NLOG2N

#define NLOG2N ( COUNT )

Value:

kissat_nlogpown (COUNT, 2)

kissat_nlogpown

double kissat_nlogpown(uint64_t count, unsigned exponent)

Definition kimits.c:29

Definition at line 110 of file kimits.h.

◆ NLOG3N

#define NLOG3N ( COUNT )

Value:

kissat_nlogpown (COUNT, 3)

Definition at line 111 of file kimits.h.

◆ NLOGN

#define NLOGN ( COUNT )

Value:

kissat_nlogpown (COUNT, 1)

Definition at line 109 of file kimits.h.

◆ REDUCE_DELAY

#define REDUCE_DELAY ( NAME )

Value:

kissat_reduce_delay (solver, &solver->delays.NAME)

kissat_reduce_delay

void kissat_reduce_delay(kissat *solver, delay *delay)

Definition kimits.c:157

Definition at line 185 of file kimits.h.

185#define REDUCE_DELAY(NAME) \

186 kissat_reduce_delay (solver, &solver->delays.NAME)

◆ SET_EFFORT_LIMIT

#define SET_EFFORT_LIMIT	(	LIMIT,
		NAME,
		START )

Definition at line 138 of file kimits.h.

#define SET_EFFORT_LIMIT(LIMIT, NAME, START) \
  uint64_t LIMIT; \
  do { \
    const uint64_t OLD_LIMIT = solver->statistics_.START; \
    const uint64_t TICKS = solver->statistics_.search_ticks; \
    const uint64_t LAST = solver->probing ? solver->last.ticks.probe \
                                          : solver->last.ticks.eliminate; \
    uint64_t REFERENCE = TICKS - LAST; \
    const uint64_t MINEFFORT = 1e6 * GET_OPTION (mineffort); \
    if (REFERENCE < MINEFFORT) { \
      REFERENCE = MINEFFORT; \
      kissat_extremely_verbose ( \
          solver, #NAME " effort reference %s set to 'mineffort'", \
          FORMAT_COUNT (REFERENCE)); \
    } else { \
      kissat_extremely_verbose ( \
          solver, #NAME " effort reference %s = %s - %s 'search_ticks'", \
          FORMAT_COUNT (REFERENCE), FORMAT_COUNT (TICKS), \
          FORMAT_COUNT (LAST)); \
    } \
    const double EFFORT = (double) GET_OPTION (NAME##effort) * 1e-3; \
    const uint64_t DELTA = EFFORT * REFERENCE; \
\
    kissat_extremely_verbose ( \
        solver, #NAME " effort delta %s = %g * %s '" #START "'", \
        FORMAT_COUNT (DELTA), EFFORT, FORMAT_COUNT (REFERENCE)); \
\
    const uint64_t NEW_LIMIT = OLD_LIMIT + DELTA; \
    kissat_very_verbose (solver, \
                         #NAME " effort limit %s = %s + %s '" #START "'", \
                         FORMAT_COUNT (NEW_LIMIT), \
                         FORMAT_COUNT (OLD_LIMIT), FORMAT_COUNT (DELTA)); \
\
    LIMIT = NEW_LIMIT; \
\
  } while (0)

◆ SQRT

#define SQRT ( COUNT )

Value:

kissat_sqrt (COUNT)

kissat_sqrt

double kissat_sqrt(uint64_t count)

Definition kimits.c:22

Definition at line 113 of file kimits.h.

◆ UPDATE_CONFLICT_LIMIT

#define UPDATE_CONFLICT_LIMIT	(	NAME,
		COUNT,
		SCALE_COUNT_FUNCTION,
		SCALE_DELTA )

Value:

  do { \
    if (solver->inconsistent) \
      break; \
    const struct statistics *statistics = &solver->statistics_; \
    KISSAT_assert (statistics->COUNT > 0); \
    struct limits *limits = &solver->limits; \
    uint64_t DELTA = GET_OPTION (NAME##int); \
    const double SCALING = SCALE_COUNT_FUNCTION (statistics->COUNT); \
    KISSAT_assert (SCALING >= 1); \
    DELTA *= SCALING; \
    const uint64_t SCALED = \
        !(SCALE_DELTA) ? DELTA \
                       : kissat_scale_delta (solver, #NAME, DELTA); \
    limits->NAME.conflicts = CONFLICTS + SCALED; \
    kissat_phase ( \
        solver, #NAME, GET (COUNT), "new limit of %s after %s conflicts", \
        FORMAT_COUNT (limits->NAME.conflicts), FORMAT_COUNT (SCALED)); \
  } while (0)

Definition at line 115 of file kimits.h.

Typedef Documentation

◆ bounds

typedef typedefABC_NAMESPACE_HEADER_START struct bounds bounds

Definition at line 10 of file kimits.h.

◆ changes

typedef struct changes changes

Definition at line 11 of file kimits.h.

◆ delay

typedef struct delay delay

Definition at line 13 of file kimits.h.

◆ delays

typedef struct delays delays

Definition at line 12 of file kimits.h.

◆ enabled

typedef struct enabled enabled

Definition at line 15 of file kimits.h.

◆ limited

typedef struct limited limited

Definition at line 16 of file kimits.h.

◆ limits

typedef struct limits limits

Definition at line 17 of file kimits.h.

◆ remember

typedef struct remember remember

Definition at line 14 of file kimits.h.

Function Documentation

◆ kissat_bump_delay()

void kissat_bump_delay	(	struct kissat *	solver,
		delay *	delay )

Definition at line 170 of file kimits.c.

                                                      {
  delay->current += delay->current < UINT_MAX;
  VERY_VERBOSE_IF_NOT_BUMPREASONS (
      solver, "%s delay interval increased to %u",
      delay_description (solver, delay), delay->current);
  delay->count = delay->current;
#ifdef KISSAT_QUIET
  (void) solver;
#endif
}

◆ kissat_changed()

bool kissat_changed	(	changes	before,
		changes	after )

◆ kissat_changes()

changes kissat_changes ( struct kissat * )

◆ kissat_delaying()

bool kissat_delaying	(	struct kissat *	solver,
		delay *	delay )

Definition at line 181 of file kimits.c.

                                                    {
  if (delay->count) {
    delay->count--;
    VERY_VERBOSE_IF_NOT_BUMPREASONS (
        solver, "%s still delayed (%u more times)",
        delay_description (solver, delay), delay->current);
    return true;
  } else {
    VERY_VERBOSE_IF_NOT_BUMPREASONS (solver, "%s not delayed",
                                     delay_description (solver, delay));
    return false;
  }
#ifdef KISSAT_QUIET
  (void) solver;
#endif
}

◆ kissat_init_limits()

void kissat_init_limits ( struct kissat * solver )

Definition at line 101 of file kimits.c.

                                         {
  KISSAT_assert (solver->statistics_.searches == 1);
 
  init_enabled (solver);
 
  limits *limits = &solver->limits;
 
  if (GET_OPTION (randec))
    INIT_CONFLICT_LIMIT (randec, false);
 
  if (GET_OPTION (reduce))
    INIT_CONFLICT_LIMIT (reduce, false);
 
  if (GET_OPTION (reorder))
    INIT_CONFLICT_LIMIT (reorder, false);
 
  if (GET_OPTION (rephase))
    INIT_CONFLICT_LIMIT (rephase, false);
 
  if (!solver->stable)
    kissat_update_focused_restart_limit (solver);
 
  kissat_init_mode_limit (solver);
 
  if (solver->enabled.eliminate) {
    INIT_CONFLICT_LIMIT (eliminate, true);
    solver->bounds.eliminate.max_bound_completed = 0;
    solver->bounds.eliminate.additional_clauses = 0;
    kissat_very_verbose (solver, "reset elimination bound to zero");
  }
 
  if (solver->enabled.probe)
    INIT_CONFLICT_LIMIT (probe, true);
}

Here is the call graph for this function:

◆ kissat_logn()

double kissat_logn ( uint64_t count )

Definition at line 15 of file kimits.c.

                                    {
  KISSAT_assert (count > 0);
  const double res = log10 (count + 9);
  KISSAT_assert (res >= 1);
  return res;
}

Here is the caller graph for this function:

◆ kissat_nlogpown()

double kissat_nlogpown	(	uint64_t	count,
		unsigned	exponent )

Definition at line 29 of file kimits.c.

                                                           {
  KISSAT_assert (count > 0);
  const double tmp = log10 (count + 9);
  double factor = 1;
  while (exponent--)
    factor *= tmp;
  KISSAT_assert (factor >= 1);
  const double res = count * factor;
  KISSAT_assert (res >= 1);
  return res;
}

◆ kissat_reduce_delay()

void kissat_reduce_delay	(	struct kissat *	solver,
		delay *	delay )

Definition at line 157 of file kimits.c.

                                                        {
  if (!delay->current)
    return;
  delay->current /= 2;
  VERY_VERBOSE_IF_NOT_BUMPREASONS (
      solver, "%s delay interval decreased to %u",
      delay_description (solver, delay), delay->current);
  delay->count = delay->current;
#ifdef KISSAT_QUIET
  (void) solver;
#endif
}

◆ kissat_scale_delta()

uint64_t kissat_scale_delta	(	struct kissat *	solver,
		const char *	pretty,
		uint64_t	delta )

Definition at line 41 of file kimits.c.

                                             {
  const uint64_t C = BINIRR_CLAUSES;
  double f = kissat_logn (C + 1) - 5;
  const double ff = f * f;
  KISSAT_assert (ff >= 0);
  const double fff = 4.5 * ff + 25;
  uint64_t scaled = fff * delta;
  KISSAT_assert (delta <= scaled);
  // clang-format off
  kissat_very_verbose (solver,
    "scaled %s delta %" PRIu64
    " = %g * %" PRIu64
    " = (4.5 (log10(%" PRIu64 ") - 5)^2 + 25) * %" PRIu64,
    pretty, scaled, fff, delta, C, delta);
  // clang-format on
  (void) pretty;
  return scaled;
}

Here is the call graph for this function:

◆ kissat_sqrt()

double kissat_sqrt ( uint64_t count )

Definition at line 22 of file kimits.c.

                                    {
  KISSAT_assert (count > 0);
  const double res = sqrt (count);
  KISSAT_assert (res >= 1);
  return res;
}

Classes

Macros

Typedefs

Functions

Macro Definition Documentation

◆ BUMP_DELAY

◆ DELAYING

◆ LINEAR

◆ LOGN

◆ NLOG2N

◆ NLOG3N

◆ NLOGN

◆ REDUCE_DELAY

◆ SET_EFFORT_LIMIT

◆ SQRT

◆ UPDATE_CONFLICT_LIMIT

Typedef Documentation

◆ bounds

◆ changes

◆ delay

◆ delays

◆ enabled

◆ limited

◆ limits

◆ remember

Function Documentation

◆ kissat_bump_delay()

◆ kissat_changed()

◆ kissat_changes()

◆ kissat_delaying()

◆ kissat_init_limits()

◆ kissat_logn()

◆ kissat_nlogpown()

◆ kissat_reduce_delay()

◆ kissat_scale_delta()

◆ kissat_sqrt()