fastel.c File Reference

#include "fastel.h"
#include "dense.h"
#include "eliminate.h"
#include "inline.h"
#include "internal.h"
#include "print.h"
#include "rank.h"
#include "report.h"
#include "terminate.h"
#include "weaken.h"

Include dependency graph for fastel.c:

Go to the source code of this file.

Classes
struct	candidate

Macros
#define	RANK_CANDIDATE(CANDIDATE)

Typedefs
typedef struct candidate	candidate

Functions
typedef	STACK (candidate)

Macro Definition Documentation

RANK_CANDIDATE

#define RANK_CANDIDATE

(

CANDIDATE

)

Value:

((CANDIDATE).score)

Typedef Documentation

candidate

typedef struct candidate candidate

Definition at line 819 of file fastel.c.

Function Documentation

STACK()

typedef STACK

(

candidate

)

Definition at line 820 of file fastel.c.

                                                       {
  if (solver->inconsistent)
    return;
  if (!GET_OPTION (fastel))
    return;
#ifndef KISSAT_QUIET
  const unsigned variables_before = solver->active;
#endif
  KISSAT_assert (!solver->level);
  START (fastel);
  kissat_enter_dense_mode (solver, 0);
  kissat_connect_irredundant_large_clauses (solver);
  const unsigned fastelrounds = GET_OPTION (fastelrounds);
  const size_t fasteloccs = GET_OPTION (fasteloccs);
#ifndef KISSAT_QUIET
  unsigned eliminated = 0;
#endif
  unsigned round = 0;
  candidates candidates;
  INIT_STACK (candidates);
  bool done = false;
  do {
    if (round++ >= fastelrounds)
      break;
    kissat_extremely_verbose (
        solver, "gathering candidates for fast elimination round %u",
        round);
    KISSAT_assert (EMPTY_STACK (candidates));
    flags *all_flags = solver->flags;
    for (all_variables (pivot)) {
      flags *pivot_flags = all_flags + pivot;
      if (!pivot_flags->active)
        continue;
      if (!pivot_flags->eliminate)
        continue;
      const unsigned lit = LIT (pivot);
      const size_t pos = flush_occurrences (solver, lit);
      if (pos > fasteloccs)
        continue;
      const unsigned not_lit = LIT (pivot);
      const size_t neg = flush_occurrences (solver, not_lit);
      if (neg > fasteloccs)
        continue;
      const unsigned score = pos + neg;
      if (score > fasteloccs)
        continue;
      candidate candidate = {pivot, score};
      PUSH_STACK (candidates, candidate);
    }
#ifndef KISSAT_QUIET
    const size_t size_candidates = SIZE_STACK (candidates);
    const size_t active_variables = solver->active;
    kissat_extremely_verbose (
        solver, "gathered %zu candidates %.0f%% in elimination round %u",
        size_candidates, kissat_percent (size_candidates, active_variables),
        round);
#endif
    RADIX_STACK (candidate, unsigned, candidates, RANK_CANDIDATE);
    unsigned eliminated_this_round = 0;
    for (all_stack (candidate, candidate, candidates)) {
      const unsigned pivot = candidate.pivot;
      flags *pivot_flags = all_flags + pivot;
      if (!pivot_flags->active)
        continue;
      if (!pivot_flags->eliminate)
        continue;
      if (TERMINATED (fastel_terminated_1)) {
        done = true;
        break;
      }
      if (try_to_fast_eliminate (solver, pivot))
        eliminated_this_round++;
      if (solver->inconsistent) {
        done = true;
        break;
      }
      pivot_flags->eliminate = false;
      kissat_flush_units_while_connected (solver);
      if (solver->inconsistent) {
        done = true;
        break;
      }
    }
    CLEAR_STACK (candidates);
#ifndef KISSAT_QUIET
    eliminated += eliminated_this_round;
    kissat_very_verbose (
        solver, "fast eliminated %u of %zu candidates %.0f%% in round %u",
        eliminated_this_round, size_candidates,
        kissat_percent (eliminated_this_round, size_candidates), round);
#endif
    if (!eliminated_this_round)
      done = true;
  } while (!done);
  RELEASE_STACK (candidates);
  for (all_variables (idx))
    FLAGS (idx)->eliminate = true;
  flush_eliminated_binary_clauses (solver);
  kissat_resume_sparse_mode (solver, true, 0);
#ifndef KISSAT_QUIET
  const unsigned original_variables = solver->statistics.variables_original;
  const unsigned variables_after = solver->active;
  kissat_verbose (
      solver,
      "[fastel] "
      "fast elimination of %u variables %.0f%% (%u remain %.0f%%)",
      eliminated, kissat_percent (eliminated, variables_before),
      variables_after,
      kissat_percent (variables_after, original_variables));
#endif
  STOP (fastel);
  REPORT (!eliminated, 'e');
}

Here is the call graph for this function: