reduce.c File Reference

#include "reduce.h"
#include "allocate.h"
#include "collect.h"
#include "inline.h"
#include "print.h"
#include "rank.h"
#include "report.h"
#include "tiers.h"
#include "trail.h"
#include <inttypes.h>
#include <math.h>

Include dependency graph for reduce.c:

Go to the source code of this file.

Classes
struct	reducible

Macros
#define	RANK_REDUCIBLE(RED)
#define	USEFULNESS   RANK_REDUCIBLE

Typedefs
typedef struct reducible	reducible

Functions
ABC_NAMESPACE_IMPL_START bool	kissat_reducing (kissat *solver)
typedef	STACK (reducible)
int	kissat_reduce (kissat *solver)

Macro Definition Documentation

RANK_REDUCIBLE

#define RANK_REDUCIBLE

(

RED

)

Value:

(RED).rank

Definition at line 33 of file reduce.c.

USEFULNESS

#define USEFULNESS   RANK_REDUCIBLE

Definition at line 98 of file reduce.c.

Typedef Documentation

reducible

typedef struct reducible reducible

Definition at line 26 of file reduce.c.

Function Documentation

kissat_reduce()

int kissat_reduce

(

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

ABC_NAMESPACE_IMPL_START bool kissat_reducing

(

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:

STACK()

typedef STACK

(

reducible

)

Definition at line 36 of file reduce.c.

                                                     {
  KISSAT_assert (start_ref != INVALID_REF);
  KISSAT_assert (start_ref <= SIZE_STACK (solver->arena));
  ward *const arena = BEGIN_STACK (solver->arena);
  clause *start = (clause *) (arena + start_ref);
  const clause *const end = (clause *) END_STACK (solver->arena);
  KISSAT_assert (start < end);
  while (start != end && !start->redundant)
    start = kissat_next_clause (start);
  if (start == end) {
    solver->first_reducible = INVALID_REF;
    LOG ("no reducible clause candidate left");
    return false;
  }
  const reference redundant = (ward *) start - arena;
#ifdef LOGGING
  if (redundant < solver->first_reducible)
    LOG ("updating start of redundant clauses from %zu to %zu",
         (size_t) solver->first_reducible, (size_t) redundant);
  else
    LOG ("no update to start of redundant clauses %zu",
         (size_t) solver->first_reducible);
#endif
  solver->first_reducible = redundant;
  const unsigned tier1 = TIER1;
  const unsigned tier2 = MAX (tier1, TIER2);
  KISSAT_assert (tier1 <= tier2);
  for (clause *c = start; c != end; c = kissat_next_clause (c)) {
    if (!c->redundant)
      continue;
    if (c->garbage)
      continue;
    const unsigned used = c->used;
    if (used)
      c->used = used - 1;
    if (c->reason)
      continue;
    const unsigned glue = c->glue;
    if (glue <= tier1 && used)
      continue;
    if (glue <= tier2 && used >= MAX_USED - 1)
      continue;
    KISSAT_assert (kissat_clause_in_arena (solver, c));
    reducible red;
    const uint64_t negative_size = ~c->size;
    const uint64_t negative_glue = ~c->glue;
    red.rank = negative_size | (negative_glue << 32);
    red.ref = (ward *) c - arena;
    PUSH_STACK (*reds, red);
  }
  if (EMPTY_STACK (*reds)) {
    kissat_phase (solver, "reduce", GET (reductions),
                  "did not find any reducible redundant clause");
    return false;
  }
  return true;
}