limit.hpp File Reference

#include "global.h"
#include <cstdint>
#include <limits>

Include dependency graph for limit.hpp:

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

Go to the source code of this file.

Classes
struct	CaDiCaL::Limit
struct	CaDiCaL::Delay
struct	CaDiCaL::Last
struct	CaDiCaL::Inc

Namespaces
namespace	CaDiCaL

Macros
#define	SET_EFFORT_LIMIT(LIMIT, NAME, THRESHHOLD)

Macro Definition Documentation

SET_EFFORT_LIMIT

#define SET_EFFORT_LIMIT	(		LIMIT,
			NAME,
			THRESHHOLD )

Value:

  int64_t LIMIT; \
  do { \
    const int64_t OLD_LIMIT = stats.ticks.NAME; \
    const int64_t TICKS = stats.ticks.search[0] + stats.ticks.search[1]; \
    const int64_t LAST = last.NAME.ticks; \
    int64_t REFERENCE = TICKS - LAST; \
    if (!REFERENCE || !stats.conflicts) { \
      VERBOSE (2, "last %" PRId64 " current %" PRId64 " delta %" PRId64, \
               LAST, TICKS, REFERENCE); \
      REFERENCE = opts.preprocessinit; \
    } \
    const double EFFORT = (double) opts.NAME##effort * 1e-3; \
    const int64_t DELTA = EFFORT * REFERENCE; \
    const int64_t THRESH = opts.NAME##thresh * clauses.size (); \
    if (THRESHHOLD && DELTA < THRESH) { \
      VERBOSE (2, \
               "delaying %s with ticklimit %" PRId64 \
               " and threshhold %" PRId64, \
               #NAME, DELTA, THRESH); \
      return false; \
    } \
    last.NAME.ticks = TICKS; \
    const int64_t NEW_LIMIT = OLD_LIMIT + DELTA; \
    LIMIT = NEW_LIMIT; \
  } while (0)

Definition at line 131 of file limit.hpp.

#define SET_EFFORT_LIMIT(LIMIT, NAME, THRESHHOLD) \
  int64_t LIMIT; \
  do { \
    const int64_t OLD_LIMIT = stats.ticks.NAME; \
    const int64_t TICKS = stats.ticks.search[0] + stats.ticks.search[1]; \
    const int64_t LAST = last.NAME.ticks; \
    int64_t REFERENCE = TICKS - LAST; \
    if (!REFERENCE || !stats.conflicts) { \
      VERBOSE (2, "last %" PRId64 " current %" PRId64 " delta %" PRId64, \
               LAST, TICKS, REFERENCE); \
      REFERENCE = opts.preprocessinit; \
    } \
    const double EFFORT = (double) opts.NAME##effort * 1e-3; \
    const int64_t DELTA = EFFORT * REFERENCE; \
    const int64_t THRESH = opts.NAME##thresh * clauses.size (); \
    if (THRESHHOLD && DELTA < THRESH) { \
      VERBOSE (2, \
               "delaying %s with ticklimit %" PRId64 \
               " and threshhold %" PRId64, \
               #NAME, DELTA, THRESH); \
      return false; \
    } \
    last.NAME.ticks = TICKS; \
    const int64_t NEW_LIMIT = OLD_LIMIT + DELTA; \
    LIMIT = NEW_LIMIT; \
  } while (0)