probe.c File Reference

#include "probe.h"
#include "backbone.h"
#include "backtrack.h"
#include "congruence.h"
#include "factor.h"
#include "internal.h"
#include "print.h"
#include "substitute.h"
#include "sweep.h"
#include "terminate.h"
#include "transitive.h"
#include "vivify.h"
#include <inttypes.h>

Include dependency graph for probe.c:

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START bool	kissat_probing (kissat *solver)
int	kissat_probe (kissat *solver)
int	kissat_probe_initially (kissat *solver)

Function Documentation

kissat_probe()

int kissat_probe

(

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

(

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()

ABC_NAMESPACE_IMPL_START bool kissat_probing

(

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: