#include "global.h"

#include "internal.hpp"

ABC_NAMESPACE_IMPL_START

namespace CaDiCaL {

/*------------------------------------------------------------------------*/

// We experimented with resetting and reinitializing the saved phase with
// many solvers. Actually RSAT had already such a scheme.  Our newest
// version seems to be quite beneficial for satisfiable instances.  In an
// arithmetic increasing interval in the number of conflicts we either use
// the original phase (set by the option 'phase'), its inverted value, flip
// the current phase, pick random phases, then pick the best since the last
// time a best phase was picked and finally also use local search to find
// phases which minimize the number of falsified clauses.  During
// stabilization (see 'stabilizing' in 'restart.cpp' when 'stable' is true)
// we execute a different rephasing schedule.  The same applies if local
// search is disabled.

/*------------------------------------------------------------------------*/

bool Internal::rephasing () {
  if (!opts.rephase)
    return false;
  if (opts.forcephase)
    return false;
  if (opts.rephase == 2) {
    if (stable)
      return stats.stabconflicts > lim.rephase;
    else
      return false;
  }
  return stats.conflicts > lim.rephase;
}

/*------------------------------------------------------------------------*/

// Pick the original default phase.

char Internal::rephase_original () {
  stats.rephased.original++;
  signed char val = opts.phase ? 1 : -1; // original = initial
  PHASE ("rephase", stats.rephased.total, "switching to original phase %d",
         val);
  for (auto idx : vars)
    phases.saved[idx] = val;
  return 'O';
}

// Pick the inverted original default phase.

char Internal::rephase_inverted () {
  stats.rephased.inverted++;
  signed char val = opts.phase ? -1 : 1; // original = -initial
  PHASE ("rephase", stats.rephased.total,
         "switching to inverted original phase %d", val);
  for (auto idx : vars)
    phases.saved[idx] = val;
  return 'I';
}

// Flip the current phase.

char Internal::rephase_flipping () {
  stats.rephased.flipped++;
  PHASE ("rephase", stats.rephased.total,
         "flipping all phases individually");
  for (auto idx : vars)
    phases.saved[idx] *= -1;
  return 'F';
}

// Complete random picking of phases.

char Internal::rephase_random () {
  stats.rephased.random++;
  PHASE ("rephase", stats.rephased.total, "resetting all phases randomly");
  Random random (opts.seed);       // global seed
  random += stats.rephased.random; // different every time
  for (auto idx : vars)
    phases.saved[idx] = random.generate_bool () ? -1 : 1;
  return '#';
}

// Best phases are those saved at the largest trail height without conflict.
// See code and comments in 'update_target_and_best' in 'backtrack.cpp'

char Internal::rephase_best () {
  stats.rephased.best++;
  PHASE ("rephase", stats.rephased.total,
         "overwriting saved phases by best phases");
  signed char val;
  for (auto idx : vars)
    if ((val = phases.best[idx]))
      phases.saved[idx] = val;
  return 'B';
}

// Trigger local search 'walk' in 'walk.cpp'.

char Internal::rephase_walk () {
  stats.rephased.walk++;
  PHASE ("rephase", stats.rephased.total,
         "starting local search to improve current phase");
  if (opts.walkfullocc)
    walk_full_occs ();
  else
    walk ();
  return 'W';
}

/*------------------------------------------------------------------------*/

void Internal::rephase () {

  stats.rephased.total++;
  last.stabilize.rephased++;
  CADICAL_assert (last.stabilize.rephased <= stats.rephased.total);
  PHASE ("rephase", stats.rephased.total,
         "reached rephase limit %" PRId64 " after %" PRId64 " conflicts",
         lim.rephase,
         opts.rephase == 2 ? stats.stabconflicts : stats.conflicts);

  // Report current 'target' and 'best' and then set 'rephased' below, which
  // will trigger reporting the new 'target' and 'best' after updating it in
  // the next 'update_target_and_best' called from the next 'backtrack'.
  //
  report ('~', 1);

  backtrack ();

  size_t count = lim.rephased[stable]++;
  bool single;
  char type;

  if (opts.stabilize && opts.stabilizeonly)
    single = true;
  else
    single = !opts.stabilize;

  if (single && !opts.walk) {
    // (inverted,best,flipping,best,random,best,original,best)^\omega
    switch (count % 8) {
    case 0:
      type = rephase_inverted ();
      break;
    case 1:
      type = rephase_best ();
      break;
    case 2:
      type = rephase_flipping ();
      break;
    case 3:
      type = rephase_best ();
      break;
    case 4:
      type = rephase_random ();
      break;
    case 5:
      type = rephase_best ();
      break;
    case 6:
      type = rephase_original ();
      break;
    case 7:
      type = rephase_best ();
      break;
    default:
      type = 0;
      break;
    }
  } else if (single && opts.walk) {
    // (inverted,best,walk,
    //  flipping,best,walk,
    //    random,best,walk,
    //  original,best,walk)^\omega
    switch (count % 12) {
    case 0:
      type = rephase_inverted ();
      break;
    case 1:
      type = rephase_best ();
      break;
    case 2:
      type = rephase_walk ();
      break;
    case 3:
      type = rephase_flipping ();
      break;
    case 4:
      type = rephase_best ();
      break;
    case 5:
      type = rephase_walk ();
      break;
    case 6:
      type = rephase_random ();
      break;
    case 7:
      type = rephase_best ();
      break;
    case 8:
      type = rephase_walk ();
      break;
    case 9:
      type = rephase_original ();
      break;
    case 10:
      type = rephase_best ();
      break;
    case 11:
      type = rephase_walk ();
      break;
    default:
      type = 0;
      break;
    }
  } else if (opts.rephase == 2 && opts.walk) {
    // (inverted,best,walk,
    //  flipping,best,walk,
    //    random,best,walk,
    //  original,best,walk)^\omega
    switch (count % 12) {
    case 0:
      type = rephase_inverted ();
      break;
    case 1:
      type = rephase_best ();
      break;
    case 2:
      type = rephase_walk ();
      break;
    case 3:
      type = rephase_flipping ();
      break;
    case 4:
      type = rephase_best ();
      break;
    case 5:
      type = rephase_walk ();
      break;
    case 6:
      type = rephase_random ();
      break;
    case 7:
      type = rephase_best ();
      break;
    case 8:
      type = rephase_walk ();
      break;
    case 9:
      type = rephase_original ();
      break;
    case 10:
      type = rephase_best ();
      break;
    case 11:
      type = rephase_walk ();
      break;
    default:
      type = 0;
      break;
    }
  } else if (stable && !opts.walk) {
    // original,inverted,(best,original,best,inverted)^\omega
    if (!count)
      type = rephase_original ();
    else if (count == 1)
      type = rephase_inverted ();
    else
      switch ((count - 2) % 4) {
      case 0:
        type = rephase_best ();
        break;
      case 1:
        type = rephase_original ();
        break;
      case 2:
        type = rephase_best ();
        break;
      case 3:
        type = rephase_inverted ();
        break;
      default:
        type = 0;
        break;
      }
  } else if (stable && opts.walk) {
    // original,inverted,(best,walk,original,best,walk,inverted)^\omega
    if (!count)
      type = rephase_original ();
    else if (count == 1)
      type = rephase_inverted ();
    else
      switch ((count - 2) % 6) {
      case 0:
        type = rephase_best ();
        break;
      case 1:
        type = rephase_walk ();
        break;
      case 2:
        type = rephase_original ();
        break;
      case 3:
        type = rephase_best ();
        break;
      case 4:
        type = rephase_walk ();
        break;
      case 5:
        type = rephase_inverted ();
        break;
      default:
        type = 0;
        break;
      }
  } else if (!stable && (!opts.walk || !opts.walknonstable)) {
    // flipping,(random,best,flipping,best)^\omega
    if (!count)
      type = rephase_flipping ();
    else
      switch ((count - 1) % 4) {
      case 0:
        type = rephase_random ();
        break;
      case 1:
        type = rephase_best ();
        break;
      case 2:
        type = rephase_flipping ();
        break;
      case 3:
        type = rephase_best ();
        break;
      default:
        type = 0;
        break;
      }
  } else {
    CADICAL_assert (!stable && opts.walk && opts.walknonstable);
    // flipping,(random,best,walk,flipping,best,walk)^\omega
    if (!count)
      type = rephase_original ();
    else
      switch ((count - 1) % 6) {
      case 0:
        type = rephase_random ();
        break;
      case 1:
        type = rephase_best ();
        break;
      case 2:
        type = rephase_walk ();
        break;
      case 3:
        type = rephase_flipping ();
        break;
      case 4:
        type = rephase_best ();
        break;
      case 5:
        type = rephase_walk ();
        break;
      default:
        type = 0;
        break;
      }
  }
  CADICAL_assert (type);

  // clear after walk such that random walk can still access the target
  // by using the saved phases
  copy_phases (phases.target);
  target_assigned = 0;

  int64_t delta = opts.rephaseint * (stats.rephased.total + 1);
  lim.rephase =
      (opts.rephase == 2 ? stats.stabconflicts : stats.conflicts) + delta;

  PHASE ("rephase", stats.rephased.total,
         "new rephase limit %" PRId64 " after %" PRId64 " conflicts",
         lim.rephase, delta);

  // This will trigger to report the effect of this new set of phases at the
  // 'backtrack' (actually 'update_target_and_best') after the next
  // conflict, as well as resetting 'best_assigned' then to allow to compute
  // a new "best" assignment at that point.
  //
  last.rephase.conflicts = stats.conflicts;
  rephased = type;

  if (!marked_failed || unsat_constraint) {
    CADICAL_assert (opts.warmup);
    return;
  }
  if (stable)
    shuffle_scores ();
  else
    shuffle_queue ();
}

} // namespace CaDiCaL

ABC_NAMESPACE_IMPL_END