backtrack.c File Reference

#include "backtrack.h"
#include "analyze.h"
#include "inline.h"
#include "inlineheap.h"
#include "inlinequeue.h"
#include "print.h"
#include "proprobe.h"
#include "propsearch.h"
#include "trail.h"

Include dependency graph for backtrack.c:

Go to the source code of this file.

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

Function Documentation

kissat_backtrack_after_conflict()

void kissat_backtrack_after_conflict	(	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	(	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

(

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	(	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: