https://github.com/TakehideSoh/SAF
Tip revision: d26cc9f94a4f79c046ee0cdd3a127a44f7b443b6 authored by TakehideSoh on 23 June 2023, 07:02:26 UTC
Merge pull request #2 from TakehideSoh/dev
Merge pull request #2 from TakehideSoh/dev
Tip revision: d26cc9f
reluctant.hpp
#ifndef _reluctant_hpp_INCLUDED
#define _reluctant_hpp_INCLUDED
namespace CaDiCaL {
// This is Donald Knuth's version of the Luby restart sequence which he
// called 'reluctant doubling'. His bit-twiddling formulation in line (DK)
// requires to keep two words around which are updated every time the
// reluctant doubling sequence is advanced. The original version in the
// literature uses a complex recursive function which computes the length of
// the next inactive sub-sequence every time (but is state-less).
//
// In our code we incorporate a base interval 'period' and only after period
// many calls to 'tick' times the current sequence value we update the
// reluctant doubling sequence value. The 'tick' call is decoupled from
// the activation signal of the sequence (the 'bool ()' operator) through
// 'trigger'. It is also possible to set an upper limit to the length of an
// inactive sub-sequence. If that limit is reached the whole reluctant
// doubling sequence starts over with the initial values.
class Reluctant {
uint64_t u, v, limit;
uint64_t period, countdown;
bool trigger, limited;
public:
Reluctant () : period (0), trigger (false) { }
void enable (int p, int64_t l) {
assert (p > 0);
u = v = 1;
period = countdown = p;
trigger = false;
if (l <= 0) limited = false;
else limited = true, limit = l;
};
void disable () { period = 0, trigger = false; }
// Increments the count until the 'period' is hit. Then it performs the
// actual increment of reluctant doubling. This gives the common 'Luby'
// sequence with the specified base interval period. As soon the limit is
// reached (countdown goes to zero) we remember this event and then
// disable updating the reluctant sequence until the signal is delivered.
void tick () {
if (!period) return; // disabled
if (trigger) return; // already triggered
if (--countdown) return; // not there yet
if ((u & -u) == v) u = u + 1, v = 1; else v = 2*v; // (DK)
if (limited && v >= limit) u = v = 1;
countdown = v * period;
trigger = true;
}
operator bool () {
if (!trigger) return false;
trigger = false;
return true;
}
};
}
#endif
