proprobe.c File Reference

#include "proprobe.h"
#include "fastassign.h"
#include "trail.h"
#include "proplit.h"

Include dependency graph for proprobe.c:

Go to the source code of this file.

Macros
#define	PROPAGATE_LITERAL   probing_propagate_literal
#define	PROPAGATION_TYPE   "probing"
#define	PROBING_PROPAGATION

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

Macro Definition Documentation

PROBING_PROPAGATION

#define PROBING_PROPAGATION

Definition at line 9 of file proprobe.c.

PROPAGATE_LITERAL

#define PROPAGATE_LITERAL   probing_propagate_literal

Definition at line 7 of file proprobe.c.

PROPAGATION_TYPE

#define PROPAGATION_TYPE   "probing"

Definition at line 8 of file proprobe.c.

Function Documentation

kissat_probing_propagate()

clause * kissat_probing_propagate	(	kissat *	solver,
		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: