kimits.c File Reference

#include "internal.h"
#include "logging.h"
#include "mode.h"
#include "print.h"
#include "reduce.h"
#include "rephase.h"
#include "resources.h"
#include "restart.h"
#include <inttypes.h>
#include <math.h>

Include dependency graph for kimits.c:

Go to the source code of this file.

Macros
#define	INIT_CONFLICT_LIMIT(NAME, SCALE)
#define	VERY_VERBOSE_IF_NOT_BUMPREASONS(...)

Functions
ABC_NAMESPACE_IMPL_START double	kissat_logn (uint64_t count)
double	kissat_sqrt (uint64_t count)
double	kissat_nlogpown (uint64_t count, unsigned exponent)
uint64_t	kissat_scale_delta (kissat *solver, const char *pretty, uint64_t delta)
void	kissat_init_limits (kissat *solver)
void	kissat_reduce_delay (kissat *solver, delay *delay)
void	kissat_bump_delay (kissat *solver, delay *delay)
bool	kissat_delaying (kissat *solver, delay *delay)

Macro Definition Documentation

INIT_CONFLICT_LIMIT

#define INIT_CONFLICT_LIMIT	(		NAME,
			SCALE )

Value:

  do { \
    const uint64_t DELTA = GET_OPTION (NAME##init); \
    const uint64_t SCALED = \
        !(SCALE) ? DELTA : kissat_scale_delta (solver, #NAME, DELTA); \
    limits->NAME.conflicts = CONFLICTS + SCALED; \
    kissat_very_verbose (solver, \
                         "initial " #NAME " limit of %s conflicts", \
                         FORMAT_COUNT (limits->NAME.conflicts)); \
  } while (0)

Definition at line 90 of file kimits.c.

#define INIT_CONFLICT_LIMIT(NAME, SCALE) \
  do { \
    const uint64_t DELTA = GET_OPTION (NAME##init); \
    const uint64_t SCALED = \
        !(SCALE) ? DELTA : kissat_scale_delta (solver, #NAME, DELTA); \
    limits->NAME.conflicts = CONFLICTS + SCALED; \
    kissat_very_verbose (solver, \
                         "initial " #NAME " limit of %s conflicts", \
                         FORMAT_COUNT (limits->NAME.conflicts)); \
  } while (0)

VERY_VERBOSE_IF_NOT_BUMPREASONS

#define VERY_VERBOSE_IF_NOT_BUMPREASONS

(

...

)

Value:

  VERY_VERBOSE_OR_LOG (delay == &solver->delays.bumpreasons, __VA_ARGS__)

Definition at line 154 of file kimits.c.

#define VERY_VERBOSE_IF_NOT_BUMPREASONS(...) \
  VERY_VERBOSE_OR_LOG (delay == &solver->delays.bumpreasons, __VA_ARGS__)

Function Documentation

kissat_bump_delay()

void kissat_bump_delay	(	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_delaying()

bool kissat_delaying	(	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

(

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()

ABC_NAMESPACE_IMPL_START 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	(	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	(	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;
}