decide.h File Reference

#include "global.h"

Include dependency graph for decide.h:

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

Go to the source code of this file.

Macros
#define	INITIAL_PHASE   (GET_OPTION (phase) ? 1 : -1)

Functions
void	kissat_decide (struct kissat *)
void	kissat_start_random_sequence (struct kissat *)
void	kissat_internal_assume (struct kissat *, unsigned lit)
unsigned	kissat_next_decision_variable (struct kissat *)
int	kissat_decide_phase (struct kissat *, unsigned idx)

Macro Definition Documentation

INITIAL_PHASE

#define INITIAL_PHASE   (GET_OPTION (phase) ? 1 : -1)

Definition at line 15 of file decide.h.

Function Documentation

kissat_decide()

void kissat_decide

(

struct kissat *

solver

)

Definition at line 211 of file decide.c.

                                    {
  START (decide);
  KISSAT_assert (solver->unassigned);
  if (solver->warming)
    INC (warming_decisions);
  else {
    INC (decisions);
    if (solver->stable)
      INC (stable_decisions);
    else
      INC (focused_decisions);
  }
  solver->level++;
  KISSAT_assert (solver->level != INVALID_LEVEL);
  const unsigned idx = kissat_next_decision_variable (solver);
  const value value = kissat_decide_phase (solver, idx);
  unsigned lit = LIT (idx);
  if (value < 0)
    lit = NOT (lit);
  kissat_push_frame (solver, lit);
  KISSAT_assert (solver->level < SIZE_STACK (solver->frames));
  LOG ("decide literal %s", LOGLIT (lit));
  kissat_assign_decision (solver, lit);
  STOP (decide);
}

Here is the call graph for this function:

Here is the caller graph for this function:

kissat_decide_phase()

int kissat_decide_phase	(	struct kissat *	solver,
		unsigned	idx )

Definition at line 157 of file decide.c.

                                                       {
  bool force = GET_OPTION (forcephase);
 
  value *target;
  if (force)
    target = 0;
  else if (!GET_OPTION (target))
    target = 0;
  else if (solver->stable || GET_OPTION (target) > 1)
    target = solver->phases.target + idx;
  else
    target = 0;
 
  value *saved;
  if (force)
    saved = 0;
  else if (GET_OPTION (phasesaving))
    saved = solver->phases.saved + idx;
  else
    saved = 0;
 
  value res = 0;
 
  if (!solver->stable) {
    switch ((solver->statistics_.switched >> 1) & 7) {
    case 1:
      res = INITIAL_PHASE;
      break;
    case 3:
      res = -INITIAL_PHASE;
      break;
    }
  }
 
  if (!res && target && (res = *target)) {
    LOG ("%s uses target decision phase %d", LOGVAR (idx), (int) res);
    INC (target_decisions);
  }
 
  if (!res && saved && (res = *saved)) {
    LOG ("%s uses saved decision phase %d", LOGVAR (idx), (int) res);
    INC (saved_decisions);
  }
 
  if (!res) {
    res = INITIAL_PHASE;
    LOG ("%s uses initial decision phase %d", LOGVAR (idx), (int) res);
    INC (initial_decisions);
  }
  KISSAT_assert (res);
 
  return res < 0 ? -1 : 1;
}

Here is the caller graph for this function:

kissat_internal_assume()

void kissat_internal_assume	(	struct kissat *	solver,
		unsigned	lit )

Definition at line 237 of file decide.c.

                                                           {
  KISSAT_assert (solver->unassigned);
  KISSAT_assert (!VALUE (lit));
  solver->level++;
  KISSAT_assert (solver->level != INVALID_LEVEL);
  kissat_push_frame (solver, lit);
  KISSAT_assert (solver->level < SIZE_STACK (solver->frames));
  LOG ("assuming literal %s", LOGLIT (lit));
  kissat_assign_decision (solver, lit);
}

Here is the call graph for this function:

Here is the caller graph for this function:

kissat_next_decision_variable()

unsigned kissat_next_decision_variable

(

struct kissat *

solver

)

Definition at line 128 of file decide.c.

                                                        {
#ifdef LOGGING
  const char *type = 0;
#endif
  unsigned res = next_random_decision (solver);
  if (res == INVALID_IDX) {
    if (solver->stable) {
#ifdef LOGGING
      type = "maximum score";
#endif
      res = largest_score_unassigned_variable (solver);
      INC (score_decisions);
    } else {
#ifdef LOGGING
      type = "dequeued";
#endif
      res = last_enqueued_unassigned_variable (solver);
      INC (queue_decisions);
    }
  } else {
#ifdef LOGGING
    type = "random";
#endif
    INC (random_decisions);
  }
  LOG ("next %s decision %s", type, LOGVAR (res));
  return res;
}

Here is the caller graph for this function:

kissat_start_random_sequence()

void kissat_start_random_sequence

(

struct kissat *

solver

)

Definition at line 59 of file decide.c.

                                                   {
  if (!GET_OPTION (randec))
    return;
 
  if (solver->stable && !GET_OPTION (randecstable))
    return;
 
  if (!solver->stable && !GET_OPTION (randecfocused))
    return;
 
  if (solver->randec)
    kissat_very_verbose (solver,
                         "continuing random decision sequence "
                         "at %s conflicts",
                         FORMAT_COUNT (CONFLICTS));
  else {
    INC (random_sequences);
    const uint64_t count = solver->statistics_.random_sequences;
    const unsigned length = GET_OPTION (randeclength) * LOGN (count);
    kissat_very_verbose (solver,
                         "starting random decision sequence "
                         "at %s conflicts for %s conflicts",
                         FORMAT_COUNT (CONFLICTS), FORMAT_COUNT (length));
    solver->randec = length;
 
    UPDATE_CONFLICT_LIMIT (randec, random_sequences, LOGN, false);
  }
}

Here is the caller graph for this function: