backbone.c File Reference

#include "backbone.h"
#include "allocate.h"
#include "analyze.h"
#include "backtrack.h"
#include "decide.h"
#include "inline.h"
#include "internal.h"
#include "logging.h"
#include "print.h"
#include "proprobe.h"
#include "report.h"
#include "terminate.h"
#include "trail.h"
#include "utilities.h"

Include dependency graph for backbone.c:

Go to the source code of this file.

Functions
void	kissat_binary_clauses_backbone (kissat *solver)

Function Documentation

kissat_binary_clauses_backbone()

void kissat_binary_clauses_backbone

(

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