phases.h File Reference

#include "value.h"
#include "global.h"

Include dependency graph for phases.h:

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

Go to the source code of this file.

Classes
struct	phases

Macros
#define	BEST(IDX)
#define	SAVED(IDX)
#define	TARGET(IDX)

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct phases	phases

Functions
void	kissat_increase_phases (struct kissat *, unsigned)
void	kissat_decrease_phases (struct kissat *, unsigned)
void	kissat_release_phases (struct kissat *)
void	kissat_save_best_phases (struct kissat *)
void	kissat_save_target_phases (struct kissat *)

Macro Definition Documentation

BEST

#define BEST

(

IDX

)

Value:

  (solver->phases.best[KISSAT_assert (VALID_INTERNAL_INDEX (IDX)), (IDX)])

Definition at line 17 of file phases.h.

#define BEST(IDX) \
  (solver->phases.best[KISSAT_assert (VALID_INTERNAL_INDEX (IDX)), (IDX)])

SAVED

#define SAVED

(

IDX

)

Value:

  (solver->phases.saved[KISSAT_assert (VALID_INTERNAL_INDEX (IDX)), (IDX)])

Definition at line 20 of file phases.h.

#define SAVED(IDX) \
  (solver->phases.saved[KISSAT_assert (VALID_INTERNAL_INDEX (IDX)), (IDX)])

TARGET

#define TARGET

(

IDX

)

Value:

  (solver->phases.target[KISSAT_assert (VALID_INTERNAL_INDEX (IDX)), (IDX)])

Definition at line 23 of file phases.h.

#define TARGET(IDX) \
  (solver->phases.target[KISSAT_assert (VALID_INTERNAL_INDEX (IDX)), (IDX)])

Typedef Documentation

phases

typedef typedefABC_NAMESPACE_HEADER_START struct phases phases

Definition at line 9 of file phases.h.

Function Documentation

kissat_decrease_phases()

void kissat_decrease_phases	(	struct kissat *	solver,
		unsigned	new_size )

Definition at line 31 of file phases.c.

                                                                {
  const unsigned old_size = solver->size;
  KISSAT_assert (old_size > new_size);
  LOG ("decreasing phases from %u to %u", old_size, new_size);
  realloc_phases (best);
  realloc_phases (saved);
  realloc_phases (target);
}

Here is the caller graph for this function:

kissat_increase_phases()

void kissat_increase_phases	(	struct kissat *	solver,
		unsigned	new_size )

Definition at line 22 of file phases.c.

                                                                {
  const unsigned old_size = solver->size;
  KISSAT_assert (old_size < new_size);
  LOG ("increasing phases from %u to %u", old_size, new_size);
  increase_phases (best);
  increase_phases (saved);
  increase_phases (target);
}

Here is the caller graph for this function:

kissat_release_phases()

void kissat_release_phases

(

struct kissat *

solver

)

Definition at line 43 of file phases.c.

                                            {
  const unsigned size = solver->size;
  release_phases (best, size);
  release_phases (saved, size);
  release_phases (target, size);
}

Here is the caller graph for this function:

kissat_save_best_phases()

void kissat_save_best_phases

(

struct kissat *

solver

)

Definition at line 60 of file phases.c.

                                              {
  KISSAT_assert (sizeof (value) == 1);
  LOG ("saving %u best values", VARS);
  save_phases (solver, solver->phases.best);
}

kissat_save_target_phases()

void kissat_save_target_phases

(

struct kissat *

solver

)

Definition at line 66 of file phases.c.

                                                {
  KISSAT_assert (sizeof (value) == 1);
  LOG ("saving %u target values", VARS);
  save_phases (solver, solver->phases.target);
}