reluctant.c File Reference

#include "internal.h"
#include "logging.h"

Include dependency graph for reluctant.c:

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START void	kissat_enable_reluctant (reluctant *reluctant, uint64_t period, uint64_t limit)
void	kissat_disable_reluctant (reluctant *reluctant)
void	kissat_tick_reluctant (reluctant *reluctant)
void	kissat_init_reluctant (kissat *solver)

Function Documentation

kissat_disable_reluctant()

void kissat_disable_reluctant

(

reluctant *

reluctant

)

Definition at line 18 of file reluctant.c.

                                                     {
  reluctant->period = 0;
}

Here is the caller graph for this function:

kissat_enable_reluctant()

ABC_NAMESPACE_IMPL_START void kissat_enable_reluctant	(	reluctant *	reluctant,
		uint64_t	period,
		uint64_t	limit )

Definition at line 6 of file reluctant.c.

                                              {
  if (limit && period > limit)
    period = limit;
  reluctant->limited = (limit > 0);
  reluctant->trigger = false;
  reluctant->period = period;
  reluctant->wait = period;
  reluctant->u = reluctant->v = 1;
  reluctant->limit = limit;
}

Here is the caller graph for this function:

kissat_init_reluctant()

void kissat_init_reluctant

(

kissat *

solver

)

Definition at line 59 of file reluctant.c.

                                            {
  if (GET_OPTION (reluctant)) {
    LOG ("enable reluctant doubling with period %d limit %d",
         GET_OPTION (reluctantint), GET_OPTION (reluctantlim));
    kissat_enable_reluctant (&solver->reluctant, GET_OPTION (reluctantint),
                             GET_OPTION (reluctantlim));
  } else {
    LOG ("reluctant doubling disabled and thus no stable restarts");
    kissat_disable_reluctant (&solver->reluctant);
  }
}

Here is the call graph for this function:

kissat_tick_reluctant()

void kissat_tick_reluctant

(

reluctant *

reluctant

)

Definition at line 22 of file reluctant.c.

                                                  {
  if (!reluctant->period)
    return;
 
  if (reluctant->trigger)
    return;
 
  KISSAT_assert (reluctant->wait > 0);
  if (--reluctant->wait)
    return;
 
  uint64_t u = reluctant->u;
  uint64_t v = reluctant->v;
 
  if ((u & -u) == v) {
    u++;
    v = 1;
  } else {
    KISSAT_assert (UINT64_MAX / 2 >= v);
    v *= 2;
  }
 
  KISSAT_assert (v);
  KISSAT_assert (UINT64_MAX / v >= reluctant->period);
  uint64_t wait = v * reluctant->period;
 
  if (reluctant->limited && wait > reluctant->limit) {
    u = v = 1;
    wait = reluctant->period;
  }
 
  reluctant->trigger = true;
  reluctant->wait = wait;
  reluctant->u = u;
  reluctant->v = v;
}

Here is the caller graph for this function: