backbone.h File Reference

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

Include dependency graph for backbone.h:

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

Go to the source code of this file.

Functions
void	kissat_binary_clauses_backbone (struct kissat *)

Function Documentation

kissat_binary_clauses_backbone()

void kissat_binary_clauses_backbone

(

struct kissat *

solver

)

Definition at line 574 of file backbone.c.

                                                     {
  if (solver->inconsistent)
    return;
  if (!GET_OPTION (backbone))
    return;
  if (TERMINATED (backbone_terminated_3))
    return;
  KISSAT_assert (solver->watching);
  KISSAT_assert (solver->probing);
  KISSAT_assert (!solver->level);
  START (backbone);
  INC (backbone_computations);
#if !defined(KISSAT_NDEBUG) || defined(METRICS)
  KISSAT_assert (!solver->backbone_computing);
  solver->backbone_computing = true;
#endif
#ifndef KISSAT_QUIET
  const unsigned failed =
#endif
      compute_backbone (solver);
  REPORT (!failed, 'b');
#if !defined(KISSAT_NDEBUG) || defined(METRICS)
  KISSAT_assert (solver->backbone_computing);
  solver->backbone_computing = false;
#endif
  STOP (backbone);
}