mode.c File Reference

#include "bump.h"
#include "decide.h"
#include "inline.h"
#include "print.h"
#include "report.h"
#include "resources.h"
#include "restart.h"
#include <inttypes.h>

Include dependency graph for mode.c:

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START void	kissat_init_mode_limit (kissat *solver)
bool	kissat_switching_search_mode (kissat *solver)
void	kissat_switch_search_mode (kissat *solver)

Function Documentation

kissat_init_mode_limit()

ABC_NAMESPACE_IMPL_START void kissat_init_mode_limit

(

kissat *

solver

)

Definition at line 21 of file mode.c.

                                             {
  limits *limits = &solver->limits;
 
  if (GET_OPTION (stable) == 1) {
    KISSAT_assert (!solver->stable);
 
    const uint64_t conflicts_delta = GET_OPTION (modeinit);
    const uint64_t conflicts_limit = CONFLICTS + conflicts_delta;
 
    KISSAT_assert (conflicts_limit);
 
    limits->mode.conflicts = conflicts_limit;
    limits->mode.ticks = 0;
    limits->mode.count = 0;
 
    kissat_very_verbose (solver,
                         "initial %s mode switching limit "
                         "at %s after %s conflicts",
                         mode_string (solver),
                         FORMAT_COUNT (conflicts_limit),
                         FORMAT_COUNT (conflicts_delta));
 
    solver->mode.ticks = solver->statistics_.search_ticks;
#ifndef KISSAT_QUIET
    solver->mode.conflicts = CONFLICTS;
#ifdef METRICS
    solver->mode.propagations = solver->statistics_.search_propagations;
#endif
    // clang-format off
      solver->mode.entered = kissat_process_time ();
      kissat_very_verbose (solver,
        "starting %s mode at %.2f seconds "
        "(%" PRIu64 " conflicts, %" PRIu64 " ticks"
#ifdef METRICS
    ", %" PRIu64 " propagations, %" PRIu64 " visits"
#endif
    ")", mode_string (solver),
        solver->mode.entered, solver->mode.conflicts, solver->mode.ticks
#ifdef METRICS
        , solver->mode.propagations, solver->mode.visits
#endif
    );
// clang-format on
#endif
  } else
    kissat_very_verbose (solver,
                         "no need to set mode limit (only %s mode enabled)",
                         mode_string (solver));
}

Here is the caller graph for this function:

kissat_switch_search_mode()

void kissat_switch_search_mode

(

kissat *

solver

)

Definition at line 203 of file mode.c.

                                                {
  KISSAT_assert (kissat_switching_search_mode (solver));
 
  INC (switched);
  solver->limits.mode.count++;
 
  if (solver->stable)
    switch_to_focused_mode (solver);
  else
    switch_to_stable_mode (solver);
 
  solver->averages[solver->stable].saved_decisions = DECISIONS;
 
  kissat_start_random_sequence (solver);
}

Here is the call graph for this function:

Here is the caller graph for this function:

kissat_switching_search_mode()

bool kissat_switching_search_mode

(

kissat *

solver

)

Definition at line 188 of file mode.c.

                                                   {
  KISSAT_assert (!solver->inconsistent);
 
  if (GET_OPTION (stable) != 1)
    return false;
 
  limits *limits = &solver->limits;
  statistics *statistics = &solver->statistics_;
 
  if (limits->mode.count & 1)
    return statistics->search_ticks >= limits->mode.ticks;
  else
    return statistics->conflicts >= limits->mode.conflicts;
}

Here is the caller graph for this function: