sweep.h File Reference

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

Include dependency graph for sweep.h:

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

Go to the source code of this file.

Functions
bool	kissat_sweep (struct kissat *)

Function Documentation

kissat_sweep()

bool kissat_sweep

(

struct kissat *

solver

)

Definition at line 1650 of file sweep.c.

                                   {
  if (!GET_OPTION (sweep))
    return false;
  if (solver->inconsistent)
    return false;
  if (TERMINATED (sweep_terminated_7))
    return false;
  if (DELAYING (sweep))
    return false;
  KISSAT_assert (!solver->level);
  KISSAT_assert (!solver->unflushed);
  START (sweep);
  INC (sweep);
  statistics *statistics = &solver->statistics_;
  uint64_t equivalences = statistics->sweep_equivalences;
  uint64_t units = statistics->sweep_units;
  sweeper sweeper;
  init_sweeper (solver, &sweeper);
  const unsigned scheduled = schedule_sweeping (&sweeper);
  uint64_t swept = 0, limit = 10;
  for (;;) {
    if (solver->inconsistent)
      break;
    if (TERMINATED (sweep_terminated_8))
      break;
    if (solver->statistics_.kitten_ticks > sweeper.limit.ticks)
      break;
    unsigned idx = next_scheduled (&sweeper);
    if (idx == INVALID_IDX)
      break;
    FLAGS (idx)->sweep = false;
#ifndef KISSAT_QUIET
    const char *res =
#endif
        sweep_variable (&sweeper, idx);
    kissat_extremely_verbose (
        solver, "swept[%" PRIu64 "] external variable %d %s", swept,
        kissat_export_literal (solver, LIT (idx)), res);
    if (++swept == limit) {
      kissat_very_verbose (solver,
                           "found %" PRIu64 " equivalences and %" PRIu64
                           " units after sweeping %" PRIu64 " variables ",
                           statistics->sweep_equivalences - equivalences,
                           solver->statistics_.sweep_units - units, swept);
      limit *= 10;
    }
  }
  kissat_very_verbose (solver, "swept %" PRIu64 " variables", swept);
  equivalences = statistics->sweep_equivalences - equivalences,
  units = solver->statistics_.sweep_units - units;
  kissat_phase (solver, "sweep", GET (sweep),
                "found %" PRIu64 " equivalences and %" PRIu64 " units",
                equivalences, units);
  unschedule_sweeping (&sweeper, swept, scheduled);
  unsigned inactive = release_sweeper (&sweeper);
 
  if (!solver->inconsistent) {
    solver->propagate = solver->trail.begin;
    kissat_probing_propagate (solver, 0, true);
  }
 
  uint64_t eliminated = equivalences + units;
#ifndef KISSAT_QUIET
  KISSAT_assert (solver->active >= inactive);
  solver->active -= inactive;
  REPORT (!eliminated, '=');
  solver->active += inactive;
#else
  (void) inactive;
#endif
  if (kissat_average (eliminated, swept) < 0.001)
    BUMP_DELAY (sweep);
  else
    REDUCE_DELAY (sweep);
  STOP (sweep);
  return eliminated;
}

Here is the call graph for this function: