congruence.h File Reference

#include <stdbool.h>
#include "global.h"

Include dependency graph for congruence.h:

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

Go to the source code of this file.

Functions
bool	kissat_congruence (struct kissat *)

Function Documentation

kissat_congruence()

bool kissat_congruence

(

struct kissat *

solver

)

Definition at line 4591 of file congruence.c.

                                        {
  if (solver->inconsistent)
    return false;
  kissat_check_statistics (solver);
  KISSAT_assert (!solver->level);
  KISSAT_assert (solver->probing);
  KISSAT_assert (solver->watching);
  if (!GET_OPTION (congruence))
    return false;
  if (!GET_OPTION (congruenceands) && !GET_OPTION (congruenceites) &&
      !GET_OPTION (congruencexors))
    return false;
  if (GET_OPTION (congruenceonce) && solver->statistics_.closures)
    return false;
  if (TERMINATED (congruence_terminated_8))
    return false;
  if (DELAYING (congruence))
    return false;
  START (congruence);
  INC (closures);
  closure closure;
  init_closure (solver, &closure);
  extract_gates (&closure);
  bool reset = false;
  if (!solver->inconsistent && !TERMINATED (congruence_terminated_9)) {
    find_units (&closure);
    if (!solver->inconsistent && !TERMINATED (congruence_terminated_10)) {
      find_equivalences (&closure);
      if (!solver->inconsistent && !TERMINATED (congruence_terminated_11)) {
        size_t propagated = propagate_units_and_equivalences (&closure);
        if (!solver->inconsistent && propagated &&
            !TERMINATED (congruence_terminated_12)) {
          forward_subsume_matching_clauses (&closure);
          reset = true;
        }
      }
    }
  }
  if (!reset)
    reset_closure (&closure);
  unsigned equivalent = reset_repr (&closure);
  kissat_phase (solver, "congruence", GET (closures),
                "merged %u equivalent variables %.2f%%", equivalent,
                kissat_percent (equivalent, solver->active));
  KISSAT_assert (solver->active >= equivalent);
#ifndef KISSAT_QUIET
  solver->active -= equivalent;
  REPORT (!equivalent, 'c');
  if (!solver->inconsistent)
    solver->active += equivalent;
#endif
  if (kissat_average (equivalent, solver->active) < 0.001)
    BUMP_DELAY (congruence);
  else
    REDUCE_DELAY (congruence);
  STOP (congruence);
  kissat_check_statistics (solver);
  return equivalent;
}