sweep.c File Reference

#include "sweep.h"
#include "dense.h"
#include "inline.h"
#include "kitten.h"
#include "logging.h"
#include "print.h"
#include "promote.h"
#include "propdense.h"
#include "proprobe.h"
#include "random.h"
#include "rank.h"
#include "report.h"
#include "terminate.h"
#include <inttypes.h>
#include <string.h>

Include dependency graph for sweep.c:

Go to the source code of this file.

Classes
struct	sweeper
struct	sweep_candidate

Macros
#define	LOGBACKBONE(MESSAGE)
#define	LOGPARTITION(MESSAGE)
#define	all_scheduled(IDX)
#define	RANK_SWEEP_CANDIDATE(CAND)

Typedefs
typedef struct sweeper	sweeper
typedef struct sweep_candidate	sweep_candidate

Functions
typedef	STACK (sweep_candidate)
bool	kissat_sweep (kissat *solver)

Macro Definition Documentation

all_scheduled

#define all_scheduled

(

IDX

)

Value:

  unsigned IDX = sweeper->first, NEXT_##IDX; \
  IDX != INVALID_IDX && (NEXT_##IDX = sweeper->next[IDX], true); \
  IDX = NEXT_##IDX

Definition at line 819 of file sweep.c.

#define all_scheduled(IDX) \
  unsigned IDX = sweeper->first, NEXT_##IDX; \
  IDX != INVALID_IDX && (NEXT_##IDX = sweeper->next[IDX], true); \
  IDX = NEXT_##IDX

LOGBACKBONE

#define LOGBACKBONE

(

MESSAGE

)

Value:

  LOGLITSET (SIZE_STACK (sweeper->backbone), \
             BEGIN_STACK (sweeper->backbone), MESSAGE)

Definition at line 468 of file sweep.c.

#define LOGBACKBONE(MESSAGE) \
  LOGLITSET (SIZE_STACK (sweeper->backbone), \
             BEGIN_STACK (sweeper->backbone), MESSAGE)

LOGPARTITION

#define LOGPARTITION

(

MESSAGE

)

Value:

  LOGLITPART (SIZE_STACK (sweeper->partition), \
              BEGIN_STACK (sweeper->partition), MESSAGE)

Definition at line 472 of file sweep.c.

#define LOGPARTITION(MESSAGE) \
  LOGLITPART (SIZE_STACK (sweeper->partition), \
              BEGIN_STACK (sweeper->partition), MESSAGE)

RANK_SWEEP_CANDIDATE

#define RANK_SWEEP_CANDIDATE

(

CAND

)

Value:

(CAND).rank

Typedef Documentation

sweep_candidate

typedef struct sweep_candidate sweep_candidate

Definition at line 1465 of file sweep.c.

sweeper

typedef struct sweeper sweeper

Definition at line 40 of file sweep.c.

Function Documentation

kissat_sweep()

bool kissat_sweep

(

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:

STACK()

typedef STACK

(

sweep_candidate

)

Definition at line 1474 of file sweep.c.

                                                  {
  kissat *solver = sweeper->solver;
  const unsigned lit = LIT (idx);
  const size_t pos = SIZE_WATCHES (WATCHES (lit));
  if (!pos)
    return false;
  const unsigned max_occurrences = sweeper->limit.clauses;
  if (pos > max_occurrences)
    return false;
  const unsigned not_lit = NOT (lit);
  const size_t neg = SIZE_WATCHES (WATCHES (not_lit));
  if (!neg)
    return false;
  if (neg > max_occurrences)
    return false;
  *occ_ptr = pos + neg;
  return true;
}