search.c File Reference

#include "search.h"
#include "analyze.h"
#include "bump.h"
#include "classify.h"
#include "decide.h"
#include "eliminate.h"
#include "inline.h"
#include "internal.h"
#include "logging.h"
#include "lucky.h"
#include "preprocess.h"
#include "print.h"
#include "probe.h"
#include "propsearch.h"
#include "reduce.h"
#include "reluctant.h"
#include "reorder.h"
#include "rephase.h"
#include "report.h"
#include "restart.h"
#include "terminate.h"
#include "trail.h"
#include "walk.h"
#include <inttypes.h>

Include dependency graph for search.c:

Go to the source code of this file.

Functions
int	kissat_search (kissat *solver)

Function Documentation

kissat_search()

int kissat_search

(

kissat *

solver

)

Definition at line 181 of file search.c.

                                   {
  REPORT (0, '*');
  int res = 0;
  if (solver->inconsistent)
    res = 20;
  if (!res && GET_OPTION (luckyearly))
    res = kissat_lucky (solver);
  if (!res && kissat_preprocessing (solver))
    res = kissat_preprocess (solver);
  if (!res && GET_OPTION (luckylate))
    res = kissat_lucky (solver);
  if (!res)
    kissat_classify (solver);
  if (!res && searching (solver)) {
    start_search (solver);
    while (!res) {
      clause *conflict = kissat_search_propagate (solver);
      if (conflict)
        res = kissat_analyze (solver, conflict);
      else if (solver->iterating)
        iterate (solver);
      else if (!solver->unassigned)
        res = 10;
      else if (TERMINATED (search_terminated_1))
        break;
      else if (kissat_reducing (solver))
        res = kissat_reduce (solver);
      else if (kissat_switching_search_mode (solver))
        kissat_switch_search_mode (solver);
      else if (kissat_restarting (solver))
        kissat_restart (solver);
      else if (kissat_reordering (solver))
        kissat_reorder (solver);
      else if (kissat_rephasing (solver))
        kissat_rephase (solver);
      else if (kissat_probing (solver))
        res = kissat_probe (solver);
      else if (kissat_eliminating (solver))
        res = kissat_eliminate (solver);
      else if (conflict_limit_hit (solver))
        break;
      else if (decision_limit_hit (solver))
        break;
      else
        kissat_decide (solver);
    }
    stop_search (solver);
  }
  report_search_result (solver, res);
  return res;
}

Here is the call graph for this function:

Here is the caller graph for this function: