kucky.c File Reference

#include "lucky.h"
#include "analyze.h"
#include "backtrack.h"
#include "decide.h"
#include "inline.h"
#include "internal.h"
#include "print.h"
#include "proprobe.h"
#include "report.h"

Include dependency graph for kucky.c:

Go to the source code of this file.

Functions
int	kissat_lucky (struct kissat *solver)

Function Documentation

kissat_lucky()

int kissat_lucky

(

struct kissat *

solver

)

Definition at line 309 of file kucky.c.

                                         {
 
  if (solver->inconsistent)
    return 0;
 
  if (!GET_OPTION (lucky))
    return 0;
 
  START (lucky);
  KISSAT_assert (!solver->level);
  KISSAT_assert (!solver->probing);
  solver->probing = true;
  KISSAT_assert (kissat_propagated (solver));
 
  int res = 0;
 
  if (no_all_negative_clauses (solver)) {
    for (all_variables (idx)) {
      if (!ACTIVE (idx))
        continue;
      const unsigned lit = LIT (idx);
      if (VALUE (lit))
        continue;
      kissat_internal_assume (solver, lit);
#ifndef KISSAT_NDEBUG
      clause *c =
#endif
          kissat_probing_propagate (solver, 0, true);
      KISSAT_assert (!c);
    }
    kissat_verbose (solver, "set all variables to true");
    KISSAT_assert (kissat_propagated (solver));
    KISSAT_assert (!solver->unassigned);
    res = 10;
  }
 
  if (!res && no_all_positive_clauses (solver)) {
    for (all_variables (idx)) {
      if (!ACTIVE (idx))
        continue;
      const unsigned lit = LIT (idx);
      if (VALUE (lit))
        continue;
      const unsigned not_lit = NOT (lit);
      kissat_internal_assume (solver, not_lit);
#ifndef KISSAT_NDEBUG
      clause *c =
#endif
          kissat_probing_propagate (solver, 0, true);
      KISSAT_assert (!c);
    }
    kissat_verbose (solver, "set all variables to false");
    KISSAT_assert (kissat_propagated (solver));
    KISSAT_assert (!solver->unassigned);
    res = 10;
  }
 
  const unsigned active_before = solver->active;
 
  if (!res)
    res = forward_false_satisfiable (solver);
 
  if (!res)
    res = forward_true_satisfiable (solver);
 
  if (!res)
    res = backward_false_satisfiable (solver);
 
  if (!res)
    res = backward_true_satisfiable (solver);
 
  const unsigned active_after = solver->active;
  const unsigned units = active_before - active_after;
 
  if (!res && units)
    kissat_message (solver, "lucky %u units", units);
 
#ifndef KISSAT_QUIET
  bool success = res || units;
#endif
  KISSAT_assert (solver->probing);
  solver->probing = false;
  REPORT (!success, 'l');
  STOP (lucky);
 
  return res;
}

Here is the call graph for this function:

Here is the caller graph for this function: