vivify.c File Reference

#include "vivify.h"
#include "allocate.h"
#include "backtrack.h"
#include "collect.h"
#include "colors.h"
#include "decide.h"
#include "deduce.h"
#include "inline.h"
#include "print.h"
#include "promote.h"
#include "proprobe.h"
#include "rank.h"
#include "report.h"
#include "sort.h"
#include "terminate.h"
#include "tiers.h"
#include "trail.h"
#include "cover.h"
#include <inttypes.h>
#include <string.h>

Include dependency graph for vivify.c:

Go to the source code of this file.

Classes
struct	countref

Macros
#define	MORE_OCCURRENCES(A, B)
#define	COUNTREF_COUNTS   1
#define	LD_MAX_COUNTREF_SIZE   31
#define	MAX_COUNTREF_SIZE   ((1u << LD_MAX_COUNTREF_SIZE) - 1)
#define	WORSE_CANDIDATE(A, B)
#define	RANK_COUNTREF_BY_INVERSE_SIZE(CR)
#define	RANK_COUNTREF_BY_VIVIFY(CR)
#define	RANK_COUNTREF_BY_COUNT(CR)

Typedefs
typedef struct countref	countref
typedef struct vivifier	vivifier

Functions
typedef	STACK (countref)
void	kissat_vivify (kissat *solver)

Macro Definition Documentation

COUNTREF_COUNTS

#define COUNTREF_COUNTS   1

Definition at line 138 of file vivify.c.

LD_MAX_COUNTREF_SIZE

#define LD_MAX_COUNTREF_SIZE   31

Definition at line 139 of file vivify.c.

MAX_COUNTREF_SIZE

#define MAX_COUNTREF_SIZE   ((1u << LD_MAX_COUNTREF_SIZE) - 1)

Definition at line 140 of file vivify.c.

MORE_OCCURRENCES

#define MORE_OCCURRENCES	(		A,
			B )

Value:

more_occurrences (counts, (A), (B))

Definition at line 32 of file vivify.c.

RANK_COUNTREF_BY_COUNT

#define RANK_COUNTREF_BY_COUNT

(

CR

)

Value:

  ((unsigned) ((CR).count[COUNTREF_COUNTS - 1 - i]))

Definition at line 426 of file vivify.c.

#define RANK_COUNTREF_BY_COUNT(CR) \
  ((unsigned) ((CR).count[COUNTREF_COUNTS - 1 - i]))

RANK_COUNTREF_BY_INVERSE_SIZE

#define RANK_COUNTREF_BY_INVERSE_SIZE

(

CR

)

Value:

((unsigned) (~(CR).size))

Definition at line 424 of file vivify.c.

RANK_COUNTREF_BY_VIVIFY

#define RANK_COUNTREF_BY_VIVIFY

(

CR

)

Value:

((unsigned) ((CR).vivify))

Definition at line 425 of file vivify.c.

WORSE_CANDIDATE

#define WORSE_CANDIDATE	(		A,
			B )

Value:

worse_candidate (solver, counts, (A), (B))

Definition at line 354 of file vivify.c.

Typedef Documentation

countref

typedef struct countref countref

Definition at line 149 of file vivify.c.

vivifier

typedef struct vivifier vivifier

Definition at line 167 of file vivify.c.

Function Documentation

kissat_vivify()

void kissat_vivify

(

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);
}

STACK()

typedef STACK

(

countref

)

Definition at line 150 of file vivify.c.

                {
  kissat *solver;
  unsigned *counts;
  references schedule;
  size_t scheduled, tried, vivified;
  countrefs countrefs;
  unsigneds sorted;
#ifndef KISSAT_QUIET
  const char *mode;
  const char *name;
  char tag;
#endif
  int tier;
};