transitive.h File Reference

#include "global.h"

Include dependency graph for transitive.h:

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

Go to the source code of this file.

Functions
void	kissat_transitive_reduction (struct kissat *)

Function Documentation

kissat_transitive_reduction()

void kissat_transitive_reduction

(

struct kissat *

solver

)

Definition at line 301 of file transitive.c.

                                                  {
  if (solver->inconsistent)
    return;
  KISSAT_assert (solver->watching);
  KISSAT_assert (solver->probing);
  KISSAT_assert (!solver->level);
  if (!GET_OPTION (transitive))
    return;
  if (TERMINATED (transitive_terminated_2))
    return;
  START (transitive);
  INC (transitive_reductions);
#if !defined(KISSAT_NDEBUG) || defined(METRICS)
  KISSAT_assert (!solver->transitive_reducing);
  solver->transitive_reducing = true;
#endif
  prioritize_binaries (solver);
  bool success = false;
  uint64_t reduced = 0;
  unsigned units = 0;
 
  SET_EFFORT_LIMIT (limit, transitive, transitive_ticks);
 
#ifndef KISSAT_QUIET
  const unsigned active = solver->active;
  const uint64_t old_ticks = solver->statistics_.transitive_ticks;
  kissat_extremely_verbose (
      solver, "starting with %" PRIu64 " transitive ticks", old_ticks);
  unsigned probed = 0;
#endif
  unsigneds probes;
  INIT_STACK (probes);
  schedule_transitive (solver, &probes);
  bool terminate = false;
  while (!terminate && !EMPTY_STACK (probes)) {
    const unsigned idx = POP_STACK (probes);
    solver->flags[idx].transitive = false;
    if (!ACTIVE (idx))
      continue;
    for (unsigned sign = 0; !terminate && sign < 2; sign++) {
      const unsigned lit = 2 * idx + sign;
      if (solver->values[lit])
        continue;
#ifndef KISSAT_QUIET
      probed++;
#endif
      if (transitive_reduce (solver, lit, limit, &reduced, &units))
        success = true;
      if (solver->inconsistent)
        terminate = true;
      else if (solver->statistics_.transitive_ticks > limit)
        terminate = true;
      else if (TERMINATED (transitive_terminated_3))
        terminate = true;
    }
  }
  const size_t remain = SIZE_STACK (probes);
  if (remain) {
    if (!GET_OPTION (transitivekeep)) {
      kissat_very_verbose (
          solver, "dropping remaining %zu transitive candidates", remain);
      while (!EMPTY_STACK (probes)) {
        const unsigned idx = POP_STACK (probes);
        solver->flags[idx].transitive = false;
      }
    }
  } else
    kissat_very_verbose (solver, "transitive reduction complete");
  RELEASE_STACK (probes);
 
#ifndef KISSAT_QUIET
  const uint64_t new_ticks = solver->statistics_.transitive_ticks;
  const uint64_t delta_ticks = new_ticks - old_ticks;
  kissat_extremely_verbose (
      solver, "finished at %" PRIu64 " after %" PRIu64 " transitive ticks",
      new_ticks, delta_ticks);
#endif
  kissat_phase (solver, "transitive", GET (probings),
                "probed %u (%.0f%%): reduced %" PRIu64 ", units %u", probed,
                kissat_percent (probed, 2 * active), reduced, units);
 
#if !defined(KISSAT_NDEBUG) || defined(METRICS)
  KISSAT_assert (solver->transitive_reducing);
  solver->transitive_reducing = false;
#endif
  REPORT (!success, 't');
  STOP (transitive);
#ifdef KISSAT_QUIET
  (void) success;
#endif
}