#include "rephase.h"
#include "backtrack.h"
#include "decide.h"
#include "internal.h"
#include "logging.h"
#include "print.h"
#include "report.h"
#include "terminate.h"
#include "walk.h"
#include <inttypes.h>
#include <string.h>

Include dependency graph for rephase.c:

Macros
#define	size_rephase_schedule (sizeof rephase_schedule / sizeof *rephase_schedule)

Functions
bool	kissat_rephasing (kissat *solver)

void	kissat_rephase (kissat *solver)

Macro Definition Documentation

◆ size_rephase_schedule

#define size_rephase_schedule (sizeof rephase_schedule / sizeof *rephase_schedule)

Definition at line 93 of file rephase.c.

93#define size_rephase_schedule \

94 (sizeof rephase_schedule / sizeof *rephase_schedule)

Function Documentation

◆ kissat_rephase()

void kissat_rephase ( kissat * solver )

Definition at line 128 of file rephase.c.

                                     {
  kissat_backtrack_propagate_and_flush_trail (solver);
  KISSAT_assert (!solver->inconsistent);
  START (rephase);
  INC (rephased);
#ifndef KISSAT_QUIET
  const char type =
#endif
      reset_phases (solver);
  REPORT (0, type);
  STOP (rephase);
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ kissat_rephasing()

bool kissat_rephasing ( kissat * solver )

Definition at line 34 of file rephase.c.

                                       {
  if (!GET_OPTION (rephase))
    return false;
  if (!solver->stable)
    return false;
  return CONFLICTS > solver->limits.rephase.conflicts;
}