propsearch.h File Reference

#include "global.h"

Include dependency graph for propsearch.h:

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

Go to the source code of this file.

Functions
struct clause *	kissat_search_propagate (struct kissat *)

Function Documentation

kissat_search_propagate()

struct clause * kissat_search_propagate

(

struct kissat *

solver

)

Definition at line 46 of file propsearch.c.

                                                 {
  KISSAT_assert (!solver->probing);
  KISSAT_assert (solver->watching);
  KISSAT_assert (!solver->inconsistent);
 
  START (propagate);
 
  solver->ticks = 0;
  const unsigned *saved_propagate = solver->propagate;
  clause *conflict = search_propagate (solver);
  update_search_propagation_statistics (solver, saved_propagate);
  kissat_update_conflicts_and_trail (solver, conflict, true);
  if (conflict && solver->randec) {
    if (!--solver->randec)
      kissat_very_verbose (solver, "last random decision conflict");
    else if (solver->randec == 1)
      kissat_very_verbose (solver,
                           "one more random decision conflict to go");
    else
      kissat_very_verbose (solver,
                           "%s more random decision conflicts to go",
                           FORMAT_COUNT (solver->randec));
  }
 
  STOP (propagate);
 
  return conflict;
}

Here is the caller graph for this function: