backtrack.h File Reference

#include "global.h"

Include dependency graph for backtrack.h:

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

Go to the source code of this file.

Functions
void	kissat_backtrack_without_updating_phases (struct kissat *, unsigned)
void	kissat_backtrack_in_consistent_state (struct kissat *, unsigned)
void	kissat_backtrack_after_conflict (struct kissat *, unsigned)
void	kissat_backtrack_propagate_and_flush_trail (struct kissat *)

Function Documentation

kissat_backtrack_after_conflict()

void kissat_backtrack_after_conflict	(	struct kissat *	solver,
		unsigned	new_level )

Definition at line 158 of file backtrack.c.

                                                                          {
  if (solver->level)
    kissat_backtrack_without_updating_phases (solver, solver->level - 1);
  kissat_update_target_and_best_phases (solver);
  kissat_backtrack_without_updating_phases (solver, new_level);
}

Here is the call graph for this function:

kissat_backtrack_in_consistent_state()

void kissat_backtrack_in_consistent_state	(	struct kissat *	solver,
		unsigned	new_level )

Definition at line 152 of file backtrack.c.

                                                               {
  kissat_update_target_and_best_phases (solver);
  kissat_backtrack_without_updating_phases (solver, new_level);
}

Here is the call graph for this function:

Here is the caller graph for this function:

kissat_backtrack_propagate_and_flush_trail()

void kissat_backtrack_propagate_and_flush_trail

(

struct kissat *

solver

)

Definition at line 165 of file backtrack.c.

                                                                 {
  if (solver->level) {
    KISSAT_assert (solver->watching);
    kissat_backtrack_in_consistent_state (solver, 0);
#ifndef KISSAT_NDEBUG
    clause *conflict =
#endif
        solver->probing ? kissat_probing_propagate (solver, 0, true)
                        : kissat_search_propagate (solver);
    KISSAT_assert (!conflict);
  }
 
  KISSAT_assert (kissat_propagated (solver));
  KISSAT_assert (kissat_trail_flushed (solver));
}

Here is the call graph for this function:

Here is the caller graph for this function:

kissat_backtrack_without_updating_phases()

void kissat_backtrack_without_updating_phases	(	struct kissat *	solver,
		unsigned	new_level )

Definition at line 74 of file backtrack.c.

                                                                   {
  KISSAT_assert (solver->level >= new_level);
  if (solver->level == new_level)
    return;
 
  LOG ("backtracking to decision level %u", new_level);
 
  frame *new_frame = &FRAME (new_level + 1);
  SET_END_OF_STACK (solver->frames, new_frame);
 
  value *values = solver->values;
  unsigned *trail = BEGIN_ARRAY (solver->trail);
  unsigned *new_end = trail + new_frame->trail;
  assigned *assigned = solver->assigned;
 
  unsigned *old_end = END_ARRAY (solver->trail);
  unsigned unassigned = 0, reassigned = 0;
 
  unsigned *q = new_end;
  if (solver->stable) {
    heap *scores = SCORES;
    for (const unsigned *p = q; p != old_end; p++) {
      const unsigned lit = *p;
      const unsigned idx = IDX (lit);
      KISSAT_assert (idx < VARS);
      struct assigned *a = assigned + idx;
      const unsigned level = a->level;
      if (level <= new_level) {
        const unsigned new_trail = q - trail;
        KISSAT_assert (new_trail <= a->trail);
        a->trail = new_trail;
        *q++ = lit;
        LOG ("reassign %s", LOGLIT (lit));
        reassigned++;
      } else {
        unassign (solver, values, lit);
        add_unassigned_variable_back_to_heap (solver, scores, lit);
        unassigned++;
      }
    }
  } else {
    links *links = solver->links;
    for (const unsigned *p = q; p != old_end; p++) {
      const unsigned lit = *p;
      const unsigned idx = IDX (lit);
      KISSAT_assert (idx < VARS);
      struct assigned *a = assigned + idx;
      const unsigned level = a->level;
      if (level <= new_level) {
        const unsigned new_trail = q - trail;
        KISSAT_assert (new_trail <= a->trail);
        a->trail = new_trail;
        *q++ = lit;
        LOG ("reassign %s", LOGLIT (lit));
        reassigned++;
      } else {
        unassign (solver, values, lit);
        add_unassigned_variable_back_to_queue (solver, links, lit);
        unassigned++;
      }
    }
  }
  SET_END_OF_ARRAY (solver->trail, q);
 
  solver->level = new_level;
  LOG ("unassigned %u literals", unassigned);
  LOG ("reassigned %u literals", reassigned);
  (void) unassigned, (void) reassigned;
 
  KISSAT_assert (new_end <= END_ARRAY (solver->trail));
  LOG ("propagation will resume at trail position %zu",
       (size_t) (new_end - trail));
  solver->propagate = new_end;
 
  KISSAT_assert (!solver->extended);
}

Here is the caller graph for this function: