bump.h File Reference

#include <stdbool.h>
#include "global.h"

Include dependency graph for bump.h:

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

Go to the source code of this file.

Macros
#define	MAX_SCORE   1e150

Functions
void	kissat_bump_analyzed (struct kissat *)
void	kissat_update_scores (struct kissat *)
void	kissat_rescale_scores (struct kissat *)
void	kissat_bump_variable (struct kissat *, unsigned idx)
void	kissat_bump_score_increment (struct kissat *)

Macro Definition Documentation

MAX_SCORE

#define MAX_SCORE   1e150

Definition at line 17 of file bump.h.

Function Documentation

kissat_bump_analyzed()

void kissat_bump_analyzed

(

struct kissat *

solver

)

Definition at line 105 of file bump.c.

                                           {
  START (bump);
  const size_t bumped = SIZE_STACK (solver->analyzed);
  if (!solver->stable)
    move_analyzed_variables_to_front_of_queue (solver);
  else
    bump_analyzed_variable_scores (solver);
  ADD (literals_bumped, bumped);
  STOP (bump);
}

Here is the caller graph for this function:

kissat_bump_score_increment()

void kissat_bump_score_increment

(

struct kissat *

solver

)

Definition at line 45 of file bump.c.

                                                  {
  const double old_scinc = solver->scinc;
  const double decay = GET_OPTION (decay) * 1e-3;
  KISSAT_assert (0 <= decay), KISSAT_assert (decay <= 0.5);
  const double factor = 1.0 / (1.0 - decay);
  const double new_scinc = old_scinc * factor;
  LOG ("new score increment %g = %g * %g", new_scinc, factor, old_scinc);
  solver->scinc = new_scinc;
  if (new_scinc > MAX_SCORE)
    kissat_rescale_scores (solver);
}

Here is the call graph for this function:

kissat_bump_variable()

void kissat_bump_variable	(	struct kissat *	solver,
		unsigned	idx )

Definition at line 69 of file bump.c.

                                                         {
  bump_analyzed_variable_score (solver, idx);
}

kissat_rescale_scores()

void kissat_rescale_scores

(

struct kissat *

solver

)

Definition at line 30 of file bump.c.

                                            {
  INC (rescaled);
  heap *scores = &solver->scores;
  const double max_score = kissat_max_score_on_heap (scores);
  kissat_phase (solver, "rescale", GET (rescaled),
                "maximum score %g increment %g", max_score, solver->scinc);
  const double rescale = MAX (max_score, solver->scinc);
  KISSAT_assert (rescale > 0);
  const double factor = 1.0 / rescale;
  kissat_rescale_heap (solver, scores, factor);
  solver->scinc *= factor;
  kissat_phase (solver, "rescale", GET (rescaled), "rescaled by factor %g",
                factor);
}

Here is the call graph for this function:

Here is the caller graph for this function:

kissat_update_scores()

void kissat_update_scores

(

struct kissat *

solver

)

Definition at line 116 of file bump.c.

                                           {
  KISSAT_assert (solver->stable);
  heap *scores = SCORES;
  for (all_variables (idx))
    if (ACTIVE (idx) && !kissat_heap_contains (scores, idx))
      kissat_push_heap (solver, scores, idx);
}