probe.h File Reference

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

Include dependency graph for probe.h:

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

Go to the source code of this file.

Functions
bool	kissat_probing (struct kissat *)
int	kissat_probe (struct kissat *)
int	kissat_probe_initially (struct kissat *)

Function Documentation

kissat_probe()

int kissat_probe

(

struct kissat *

solver

)

Definition at line 72 of file probe.c.

                                  {
  KISSAT_assert (!solver->inconsistent);
  INC (probings);
  KISSAT_assert (!solver->probing);
  solver->probing = true;
  const unsigned max_rounds = GET_OPTION (proberounds);
  for (unsigned round = 0; round != max_rounds; round++) {
    unsigned before = solver->active;
    probe (solver);
    if (solver->inconsistent)
      break;
    if (before == solver->active)
      break;
  }
  kissat_classify (solver);
  UPDATE_CONFLICT_LIMIT (probe, probings, NLOGN, true);
  solver->last.ticks.probe = solver->statistics_.search_ticks;
  KISSAT_assert (solver->probing);
  solver->probing = false;
  return solver->inconsistent ? 20 : 0;
}

Here is the call graph for this function:

Here is the caller graph for this function:

kissat_probe_initially()

int kissat_probe_initially

(

struct kissat *

solver

)

Definition at line 94 of file probe.c.

                                            {
  KISSAT_assert (!solver->level);
  KISSAT_assert (!solver->inconsistent);
  INC (probings);
  START (probe);
  KISSAT_assert (!solver->probing);
  solver->probing = true;
  probe_initially (solver);
  KISSAT_assert (solver->probing);
  solver->probing = false;
  STOP (probe);
  return solver->inconsistent ? 20 : 0;
}

Here is the caller graph for this function:

kissat_probing()

bool kissat_probing

(

struct kissat *

solver

)

Definition at line 18 of file probe.c.

                                     {
  if (!solver->enabled.probe)
    return false;
  statistics *statistics = &solver->statistics_;
  const uint64_t conflicts = statistics->conflicts;
  if (solver->last.conflicts.reduce == conflicts)
    return false;
  return solver->limits.probe.conflicts < conflicts;
}

Here is the caller graph for this function: