rustsat-cadical 0.7.5

#ifndef _limit_hpp_INCLUDED
#define _limit_hpp_INCLUDED

#include <cstdint>
#include <limits>

namespace CaDiCaL {

struct Internal;

struct Limit {

  bool initialized;

  int64_t conflicts;     // conflict limit if non-negative
  int64_t decisions;     // decision limit if non-negative
  int64_t preprocessing; // limit on preprocessing rounds
  int64_t localsearch;   // limit on local search rounds
  int64_t ticks;         // ticks limit if non-negative

  int64_t compact;           // conflict limit for next 'compact'
  int64_t condition;         // conflict limit for next 'condition'
  int64_t elim;              // conflict limit for next 'elim'
  int64_t flush;             // conflict limit for next 'flush'
  int64_t inprobe;           // conflict limit for next 'inprobe'
  int64_t reduce;            // conflict limit for next 'reduce'
  int64_t rephase;           // conflict limit for next 'rephase'
  int64_t report;            // report limit for header
  int64_t restart;           // conflict limit for next 'restart'
  int64_t stabilize;         // conflict/ticks limit for next 'stabilize'
  int64_t incremental_decay; // conflict/ticks limit for next clause 'decay'
                             // for incremental clauses
  int64_t random_decision;   // randomized decision limit for conflicts

  int keptsize;           // maximum kept size in 'reduce'
  int keptglue;           // maximum kept glue in 'reduce'
  int64_t recompute_tier; // conflict limit for next tier recomputation

  // How often rephased during (1) or out (0) of stabilization.
  //
  int64_t rephased[2];

  // Current elimination bound per eliminated variable.
  //
  int64_t elimbound;

  struct {
    int check;  // countdown to next terminator call
    int forced; // forced termination for testing
  } terminate;

  Limit ();
};

struct Delay {
  struct {
    int64_t interval = 0, limit = 0;
    bool bypass = 0;

    bool delay () {
      if (bypass)
        return false;
      if (limit) {
        --limit;
        return true;
      } else {
        return false;
      }
    }

    void bump_delay () {
      interval += interval < INT64_MAX;
      limit = interval;
    }

    void reduce_delay () {
      if (!interval)
        return;
      interval /= 2;
      limit = interval;
    }

    void bypass_delay () { bypass = 1; }
    void unbypass_delay () { bypass = 0; }
  } bumpreasons;
};

struct Last {
  struct {
    int64_t propagations;
  } transred;
  struct {
    int64_t ticks;
  } backbone, probe, sweep, vivify, walk;
  struct {
    int64_t fixed, subsumephases, marked;
  } elim;
  struct {
    int64_t reductions;
  } inprobe;
  struct {
    int64_t conflicts;
  } reduce, rephase;
  struct {
    int64_t ticks;
    int64_t marked;
  } ternary;
  struct {
    int64_t fixed;
  } collect;
  struct {
    int64_t marked, ticks;
  } factor;
  struct {
    int64_t conflicts;
    int64_t ticks;
    int64_t rephased;
  } stabilize;
  struct {
    int64_t last_id;
  } incremental_decay;
  Last ();
};

struct Inc {
  int64_t flush;         // flushing interval in terms of conflicts
  int64_t stabilize;     // base ticks limit after first mode switch
  int64_t conflicts;     // next conflict limit if non-negative
  int64_t decisions;     // next decision limit if non-negative
  int64_t ticks;         // next ticks limit if non-negative
  int64_t preprocessing; // next preprocessing limit if non-negative
  int64_t localsearch;   // next local search limit if non-negative
  Inc ();
};

#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; \
    VERBOSE (2, \
             "new ticks limit %" PRId64 "= %" PRId64 " + %f * %" PRId64, \
             NEW_LIMIT, OLD_LIMIT, EFFORT, REFERENCE); \
  } while (0)

} // namespace CaDiCaL

#endif