proprobe.h File Reference

#include <stdbool.h>
#include "global.h"

Include dependency graph for proprobe.h:

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

Go to the source code of this file.

Functions
struct clause *	kissat_probing_propagate (struct kissat *, struct clause *, bool flush)

Function Documentation

kissat_probing_propagate()

struct clause * kissat_probing_propagate	(	struct kissat *	solver,
		struct clause *	ignore,
		bool	flush )

Definition at line 37 of file proprobe.c.

                                              {
  KISSAT_assert (solver->probing);
  KISSAT_assert (solver->watching);
  KISSAT_assert (!solver->inconsistent);
 
  START (propagate);
 
  clause *conflict = 0;
  unsigned *propagate = solver->propagate;
  solver->ticks = 0;
  while (!conflict && propagate != END_ARRAY (solver->trail)) {
    const unsigned lit = *propagate++;
    conflict = probing_propagate_literal (solver, ignore, lit);
  }
 
  const unsigned propagated = propagate - solver->propagate;
  solver->propagate = propagate;
  update_probing_propagation_statistics (solver, propagated);
  kissat_update_conflicts_and_trail (solver, conflict, flush);
 
  STOP (propagate);
 
  return conflict;
}

Here is the caller graph for this function: