reduce.h File Reference

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

Include dependency graph for reduce.h:

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

Go to the source code of this file.

Functions
bool	kissat_reducing (struct kissat *)
int	kissat_reduce (struct kissat *)

Function Documentation

kissat_reduce()

int kissat_reduce

(

struct kissat *

solver

)

Definition at line 155 of file reduce.c.

                                   {
  START (reduce);
  INC (reductions);
  kissat_phase (solver, "reduce", GET (reductions),
                "reduce limit %" PRIu64 " hit after %" PRIu64 " conflicts",
                solver->limits.reduce.conflicts, CONFLICTS);
  kissat_compute_and_set_tier_limits (solver);
  bool compact = kissat_compacting (solver);
  reference start = compact ? 0 : solver->first_reducible;
  if (start != INVALID_REF) {
#ifndef KISSAT_QUIET
    size_t arena_size = SIZE_STACK (solver->arena);
    size_t words_to_sweep = arena_size - start;
    size_t bytes_to_sweep = sizeof (word) * words_to_sweep;
    kissat_phase (solver, "reduce", GET (reductions),
                  "reducing clauses after offset %" REFERENCE_FORMAT
                  " in arena",
                  start);
    kissat_phase (solver, "reduce", GET (reductions),
                  "reducing %zu words %s %.0f%%", words_to_sweep,
                  FORMAT_BYTES (bytes_to_sweep),
                  kissat_percent (words_to_sweep, arena_size));
#endif
    if (kissat_flush_and_mark_reason_clauses (solver, start)) {
      reducibles reds;
      INIT_STACK (reds);
      if (collect_reducibles (solver, &reds, start)) {
        sort_reducibles (solver, &reds);
        mark_less_useful_clauses_as_garbage (solver, &reds);
        RELEASE_STACK (reds);
        kissat_sparse_collect (solver, compact, start);
      } else if (compact)
        kissat_sparse_collect (solver, compact, start);
      else
        kissat_unmark_reason_clauses (solver, start);
    } else
      KISSAT_assert (solver->inconsistent);
  } else
    kissat_phase (solver, "reduce", GET (reductions), "nothing to reduce");
  kissat_classify (solver);
  UPDATE_CONFLICT_LIMIT (reduce, reductions, SQRT, false);
  solver->last.conflicts.reduce = CONFLICTS;
  REPORT (0, '-');
  STOP (reduce);
  return solver->inconsistent ? 20 : 0;
}

Here is the call graph for this function:

Here is the caller graph for this function:

kissat_reducing()

bool kissat_reducing

(

struct kissat *

solver

)

Definition at line 16 of file reduce.c.

                                      {
  if (!GET_OPTION (reduce))
    return false;
  if (!solver->statistics_.clauses_redundant)
    return false;
  if (CONFLICTS < solver->limits.reduce.conflicts)
    return false;
  return true;
}

Here is the call graph for this function:

Here is the caller graph for this function: