tiers.c File Reference

#include "tiers.h"
#include "internal.h"
#include "logging.h"
#include "print.h"

Include dependency graph for tiers.c:

Go to the source code of this file.

Functions
void	kissat_compute_and_set_tier_limits (struct kissat *solver)
void	kissat_print_tier_usage_statistics (kissat *solver, bool stable)

Function Documentation

kissat_compute_and_set_tier_limits()

void kissat_compute_and_set_tier_limits

(

struct kissat *

solver

)

Definition at line 53 of file tiers.c.

                                                                {
  bool stable = solver->stable;
  unsigned tier1, tier2;
  compute_tier_limits (solver, stable, &tier1, &tier2);
  solver->tier1[stable] = tier1;
  solver->tier2[stable] = tier2;
  kissat_phase (solver, "retiered", GET (retiered),
                "recomputed %s tier1 limit %u and tier2 limit %u "
                "after %" PRIu64 " conflicts",
                stable ? "stable" : "focused", tier1, tier2, CONFLICTS);
}

Here is the caller graph for this function:

kissat_print_tier_usage_statistics()

void kissat_print_tier_usage_statistics	(	kissat *	solver,
		bool	stable )

Definition at line 76 of file tiers.c.

                                                                      {
  unsigned tier1, tier2;
  compute_tier_limits (solver, stable, &tier1, &tier2);
  statistics *statistics = &solver->statistics_;
  uint64_t *used_stats = statistics->used[stable].glue;
  uint64_t total_used = 0;
  for (unsigned glue = 0; glue <= MAX_GLUE_USED; glue++)
    total_used += used_stats[glue];
  const char *mode = stable ? "stable" : "focused";
  KISSAT_assert (tier1 <= tier2);
  unsigned span = tier2 - tier1 + 1;
  const unsigned max_printed = 5;
  KISSAT_assert (max_printed & 1), KISSAT_assert (max_printed / 2 > 0);
  unsigned prefix, suffix;
  if (span > max_printed) {
    prefix = tier1 + max_printed / 2 - 1;
    suffix = tier2 - max_printed / 2 + 1;
  } else
    prefix = UINT_MAX, suffix = 0;
  uint64_t accumulated_middle = 0;
  int glue_digits = 1, clauses_digits = 1;
  for (unsigned glue = 0; glue <= MAX_GLUE_USED; glue++) {
    if (glue < tier1)
      continue;
    uint64_t used = used_stats[glue];
    int tmp_glue = 0, tmp_clauses = 0;
    if (glue <= prefix || suffix <= glue) {
      tmp_glue = decimal_digits (glue);
      tmp_clauses = decimal_digits (used);
    } else {
      accumulated_middle += used;
      if (glue + 1 == suffix) {
        tmp_glue = decimal_digits (prefix + 1) + decimal_digits (glue) + 1;
        tmp_clauses = decimal_digits (accumulated_middle);
      }
    }
    if (tmp_glue > glue_digits)
      glue_digits = tmp_glue;
    if (tmp_clauses > clauses_digits)
      clauses_digits = tmp_clauses;
    if (glue == tier2)
      break;
  }
  char fmt[32];
  sprintf (fmt, "%%%d" PRIu64, clauses_digits);
  accumulated_middle = 0;
  uint64_t accumulated = 0;
  for (unsigned glue = 0; glue <= MAX_GLUE_USED; glue++) {
    uint64_t used = used_stats[glue];
    accumulated += used;
    if (glue < tier1)
      continue;
    if (glue <= prefix || suffix <= glue + 1) {
      fputs (solver->prefix, stdout);
      fputs (mode, stdout);
      fputs (" glue ", stdout);
    }
    if (glue <= prefix || suffix <= glue) {
      int len = printf ("%u", glue);
      while (len > 0 && len < glue_digits)
        fputc (' ', stdout), len++;
      fputs (" used ", stdout);
      printf (fmt, used);
      printf (" clauses %5.2f%% accumulated %5.2f%%",
              kissat_percent (used, total_used),
              kissat_percent (accumulated, total_used));
      if (glue == tier1)
        fputs (" tier1", stdout);
      if (glue == tier2)
        fputs (" tier2", stdout);
      fputc ('\n', stdout);
    } else {
      accumulated_middle += used;
      if (glue + 1 == suffix) {
        int len = printf ("%u-%u", prefix + 1, suffix - 1);
        while (len > 0 && len < glue_digits)
          fputc (' ', stdout), len++;
        fputs (" used ", stdout);
        printf (fmt, accumulated_middle);
        printf (" clauses %5.2f%% accumulated %5.2f%%\n",
                kissat_percent (accumulated_middle, total_used),
                kissat_percent (accumulated, total_used));
      }
    }
    if (glue == tier2)
      break;
  }
}

Here is the call graph for this function: