bump.c File Reference

#include "bump.h"
#include "analyze.h"
#include "inlineheap.h"
#include "inlinequeue.h"
#include "inlinevector.h"
#include "internal.h"
#include "logging.h"
#include "print.h"
#include "rank.h"
#include "sort.h"

Include dependency graph for bump.c:

Go to the source code of this file.

Macros
#define	RANK(A)
#define	SMALLER(A, B)
#define	RADIX_SORT_BUMP_LIMIT   32

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

Macro Definition Documentation

RADIX_SORT_BUMP_LIMIT

#define RADIX_SORT_BUMP_LIMIT   32

Definition at line 17 of file bump.c.

RANK

#define RANK

(

A

)

Value:

((A).rank)

Definition at line 14 of file bump.c.

SMALLER

#define SMALLER	(		A,
			B )

Value:

(RANK (A) < RANK (B))

Definition at line 15 of file bump.c.

Function Documentation

kissat_bump_analyzed()

void kissat_bump_analyzed

(

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

(

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	(	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

(

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

(

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);
}