vivify.h File Reference

#include "global.h"

Include dependency graph for vivify.h:

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

Go to the source code of this file.

Functions
void	kissat_vivify (struct kissat *)

Function Documentation

kissat_vivify()

void kissat_vivify

(

struct kissat *

solver

)

Definition at line 1402 of file vivify.c.

                                    {
  if (solver->inconsistent)
    return;
  KISSAT_assert (!solver->level);
  KISSAT_assert (solver->probing);
  KISSAT_assert (solver->watching);
  if (!GET_OPTION (vivify))
    return;
  if (TERMINATED (vivify_terminated_2))
    return;
  double irr_budget = DELAYING (vivifyirr) ? 0 : GET_OPTION (vivifyirr);
  double tier1_budget = GET_OPTION (vivifytier1);
  double tier2_budget = GET_OPTION (vivifytier2);
  double tier3_buget = GET_OPTION (vivifytier3);
  if (!REDUNDANT_CLAUSES)
    tier1_budget = tier2_budget = tier3_buget = 0;
  double sum = irr_budget + tier1_budget + tier2_budget + tier3_buget;
  if (!sum)
    return;
 
  START (vivify);
  INC (vivifications);
#if !defined(KISSAT_NDEBUG) || defined(METRICS)
  KISSAT_assert (!solver->vivifying);
  solver->vivifying = true;
#endif
 
  SET_EFFORT_LIMIT (limit, vivify, probing_ticks);
  const uint64_t total = limit - solver->statistics_.probing_ticks;
  limit = solver->statistics_.probing_ticks;
  unsigned tier1_limit = vivify_tier1_limit (solver);
  unsigned tier2_limit = vivify_tier2_limit (solver);
  if (tier1_budget && tier2_budget && tier1_limit == tier2_limit) {
    tier1_budget += tier2_budget, tier2_budget = 0;
    LOG ("vivification tier1 matches tier2 "
         "thus using tier2 budget for tier1");
  }
 
  {
    vivifier vivifier;
    init_vivifier (solver, &vivifier);
    if (tier1_budget) {
      limit += (total * tier1_budget) / sum;
      vivify_tier1 (&vivifier, limit);
    }
    if (tier2_budget && !solver->inconsistent &&
        !TERMINATED (vivify_terminated_3)) {
      limit += (total * tier2_budget) / sum;
      vivify_tier2 (&vivifier, limit);
    }
    if (tier3_buget && !solver->inconsistent &&
        !TERMINATED (vivify_terminated_4)) {
      limit += (total * tier3_buget) / sum;
      vivify_tier3 (&vivifier, limit);
    }
    if (irr_budget && !solver->inconsistent &&
        !TERMINATED (vivify_terminated_5)) {
      limit += (total * irr_budget) / sum;
      vivify_irredundant (&vivifier, limit);
      if (kissat_average (vivifier.vivified, vivifier.tried) < 0.01)
        BUMP_DELAY (vivifyirr);
      else
        REDUCE_DELAY (vivifyirr);
    }
    release_vivifier (&vivifier);
  }
 
#ifndef KISSAT_QUIET
  if (solver->statistics_.probing_ticks < limit) {
    uint64_t delta = limit - solver->statistics_.probing_ticks;
    kissat_phase (solver, "vivify-limit", GET (vivifications),
                  "has %" PRIu64 " ticks left %.2f%%", delta,
                  kissat_percent (delta, total));
  } else {
    uint64_t delta = solver->statistics_.probing_ticks - limit;
    kissat_phase (solver, "vivify-limit", GET (vivifications),
                  "exceeded by %" PRIu64 " ticks %.2f%%", delta,
                  kissat_percent (delta, total));
  }
#endif
#if !defined(KISSAT_NDEBUG) || defined(METRICS)
  KISSAT_assert (solver->vivifying);
  solver->vivifying = false;
#endif
  STOP (vivify);
}