propsearch.c File Reference

#include "propsearch.h"
#include "fastassign.h"
#include "print.h"
#include "trail.h"
#include "proplit.h"

Include dependency graph for propsearch.c:

Go to the source code of this file.

Macros
#define	PROPAGATE_LITERAL   search_propagate_literal
#define	PROPAGATION_TYPE   "search"

Functions
clause *	kissat_search_propagate (kissat *solver)

Macro Definition Documentation

PROPAGATE_LITERAL

#define PROPAGATE_LITERAL   search_propagate_literal

Definition at line 8 of file propsearch.c.

PROPAGATION_TYPE

#define PROPAGATION_TYPE   "search"

Definition at line 9 of file propsearch.c.

Function Documentation

kissat_search_propagate()

clause * kissat_search_propagate

(

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: