#include "internal.hpp"

namespace CaDiCaL {

External::External (Internal *i)
    : internal (i), max_var (0), vsize (0), extended (false),
      terminator (0), learner (0), propagator (0), solution (0),
      vars (max_var) {
  assert (internal);
  assert (!internal->external);
  internal->external = this;
}

External::~External () {
  if (solution)
    delete[] solution;
}

void External::enlarge (int new_max_var) {

  assert (!extended);

  size_t new_vsize = vsize ? 2 * vsize : 1 + (size_t) new_max_var;
  while (new_vsize <= (size_t) new_max_var)
    new_vsize *= 2;
  LOG ("enlarge external size from %zd to new size %zd", vsize, new_vsize);
  vsize = new_vsize;
}

void External::init (int new_max_var) {
  assert (!extended);
  if (new_max_var <= max_var)
    return;
  int new_vars = new_max_var - max_var;
  int old_internal_max_var = internal->max_var;
  int new_internal_max_var = old_internal_max_var + new_vars;
  internal->init_vars (new_internal_max_var);
  if ((size_t) new_max_var >= vsize)
    enlarge (new_max_var);
  LOG ("initialized %d external variables", new_vars);
  if (!max_var) {
    assert (e2i.empty ());
    e2i.push_back (0);
    assert (internal->i2e.empty ());
    internal->i2e.push_back (0);
  } else {
    assert (e2i.size () == (size_t) max_var + 1);
    assert (internal->i2e.size () == (size_t) old_internal_max_var + 1);
  }
  unsigned iidx = old_internal_max_var + 1, eidx;
  for (eidx = max_var + 1u; eidx <= (unsigned) new_max_var;
       eidx++, iidx++) {
    LOG ("mapping external %u to internal %u", eidx, iidx);
    assert (e2i.size () == eidx);
    e2i.push_back (iidx);
    internal->i2e.push_back (eidx);
    assert (internal->i2e[iidx] == (int) eidx);
    assert (e2i[eidx] == (int) iidx);
  }
  if (new_max_var >= (int64_t) is_observed.size ())
    is_observed.resize (1 + (size_t) new_max_var, false);
  if (internal->opts.checkfrozen)
    if (new_max_var >= (int64_t) moltentab.size ())
      moltentab.resize (1 + (size_t) new_max_var, false);
  assert (iidx == (size_t) new_internal_max_var + 1);
  assert (eidx == (size_t) new_max_var + 1);
  max_var = new_max_var;
}

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

void External::reset_assumptions () {
  assumptions.clear ();
  internal->reset_assumptions ();
}

void External::reset_constraint () {
  constraint.clear ();
  internal->reset_constraint ();
}

void External::reset_extended () {
  if (!extended)
    return;
  LOG ("reset extended");
  extended = false;
}

void External::reset_limits () { internal->reset_limits (); }

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

int External::internalize (int elit) {
  int ilit;
  if (elit) {
    assert (elit != INT_MIN);
    const int eidx = abs (elit);
    if (eidx > max_var)
      init (eidx);
    ilit = e2i[eidx];
    if (elit < 0)
      ilit = -ilit;
    if (!ilit) {
      assert (internal->max_var < INT_MAX);
      ilit = internal->max_var + 1u;
      internal->init_vars (ilit);
      e2i[eidx] = ilit;
      LOG ("mapping external %d to internal %d", eidx, ilit);
      e2i[eidx] = ilit;
      internal->i2e.push_back (eidx);
      assert (internal->i2e[ilit] == eidx);
      assert (e2i[eidx] == ilit);
      if (elit < 0)
        ilit = -ilit;
    }
    if (internal->opts.checkfrozen) {
      assert (eidx < (int64_t) moltentab.size ());
      if (moltentab[eidx])
        FATAL ("can not reuse molten literal %d", eidx);
    }
    Flags &f = internal->flags (ilit);
    if (f.status == Flags::UNUSED)
      internal->mark_active (ilit);
    else if (f.status != Flags::ACTIVE && f.status != Flags::FIXED)
      internal->reactivate (ilit);
    if (!marked (tainted, elit) && marked (witness, -elit)) {
      assert (!internal->opts.checkfrozen);
      LOG ("marking tainted %d", elit);
      mark (tainted, elit);
    }
  } else
    ilit = 0;
  return ilit;
}

void External::add (int elit) {
  assert (elit != INT_MIN);
  reset_extended ();
  if (internal->opts.check &&
      (internal->opts.checkwitness || internal->opts.checkfailed))
    original.push_back (elit);

  // The external literals of the new clause must be saved for later
  // when the proof is printed during add_original_lit (0)
  if (elit && internal->proof)
    eclause.push_back (elit);

  const int ilit = internalize (elit);
  assert (!elit == !ilit);
  if (elit)
    LOG ("adding external %d as internal %d", elit, ilit);
  internal->add_original_lit (ilit);

  // Clean-up saved external literals once proof line is printed
  if (!elit && internal->proof)
    eclause.clear ();
}

void External::assume (int elit) {
  assert (elit);
  reset_extended ();
  assumptions.push_back (elit);
  const int ilit = internalize (elit);
  assert (ilit);
  LOG ("assuming external %d as internal %d", elit, ilit);
  internal->assume (ilit);
}

bool External::flip (int elit) {
  assert (elit);
  assert (elit != INT_MIN);
  assert (!propagator);

  int eidx = abs (elit);
  if (eidx > max_var)
    return false;
  if (marked (witness, elit))
    return false;
  int ilit = e2i[eidx];
  if (!ilit)
    return false;
  bool res = internal->flip (ilit);
  if (res && extended)
    reset_extended ();
  return res;
}

bool External::flippable (int elit) {
  assert (elit);
  assert (elit != INT_MIN);
  assert (!propagator);

  int eidx = abs (elit);
  if (eidx > max_var)
    return false;
  if (marked (witness, elit))
    return false;
  int ilit = e2i[eidx];
  if (!ilit)
    return false;
  return internal->flippable (ilit);
}

bool External::failed (int elit) {
  assert (elit);
  assert (elit != INT_MIN);
  int eidx = abs (elit);
  if (eidx > max_var)
    return 0;
  int ilit = e2i[eidx];
  if (!ilit)
    return 0;
  if (elit < 0)
    ilit = -ilit;
  return internal->failed (ilit);
}

void External::constrain (int elit) {
  if (constraint.size () && !constraint.back ()) {
    LOG (constraint, "replacing previous constraint");
    reset_constraint ();
  }
  assert (elit != INT_MIN);
  reset_extended ();
  constraint.push_back (elit);
  const int ilit = internalize (elit);
  assert (!elit == !ilit);
  if (elit)
    LOG ("adding external %d as internal %d to constraint", elit, ilit);
  internal->constrain (ilit);
}

bool External::failed_constraint () {
  return internal->failed_constraint ();
}

void External::phase (int elit) {
  assert (elit);
  assert (elit != INT_MIN);
  int eidx = abs (elit);
  if (eidx > max_var) {
  UNUSED:
    LOG ("forcing phase of unused external %d ignored", elit);
    return;
  }
  int ilit = e2i[eidx];
  if (!ilit)
    goto UNUSED;
  if (elit < 0)
    ilit = -ilit;
  internal->phase (ilit);
}

void External::unphase (int elit) {
  assert (elit);
  assert (elit != INT_MIN);
  int eidx = abs (elit);
  if (eidx > max_var) {
  UNUSED:
    LOG ("resetting forced phase of unused external %d ignored", elit);
    return;
  }
  int ilit = e2i[eidx];
  if (!ilit)
    goto UNUSED;
  if (elit < 0)
    ilit = -ilit;
  internal->unphase (ilit);
}

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

// External propagation related functions

void External::add_observed_var (int elit) {
  if (!propagator) {
    LOG ("No connected propagator that could observe the variable, "
         "observed flag is not set.");
    return;
  }

  assert (elit);
  assert (elit != INT_MIN);
  reset_extended (); // tainting!

  int eidx = abs (elit);
  if (eidx <= max_var &&
      (marked (witness, elit) || marked (witness, -elit))) {
    LOG ("Error, only clean variables are allowed to become observed.");
    assert (false);

    // TODO: here needs to come the taint and restore of the newly
    // observed variable. Restore_clauses must be called before continue.
    // LOG ("marking tainted %d", elit);
    // mark (tainted, elit);
    // mark (tainted, -elit);
    // restore_clauses ...
  }

  if (eidx >= (int64_t) is_observed.size ())
    is_observed.resize (1 + (size_t) eidx, false);

  if (is_observed[eidx])
    return;

  LOG ("marking %d as externally watched", eidx);

  // Will do the necessary internalization
  freeze (elit);
  is_observed[eidx] = true;

  int ilit = internalize (elit);
  internal->add_observed_var (ilit);

  if (propagator->is_lazy)
    return;

  // Fixed variables are notified only upon assignment. In case
  // this variable was already assigned (e.g. via unit clause),
  // it must be notified explicitly now. (-> Can cause a repeated fixed
  // assignment notification, in case it was unobserved and observed again.)
  const int tmp = fixed (elit);
  if (!tmp)
    return;
  int unit = tmp < 0 ? -elit : elit;

  LOG ("notify propagator about fixed assignment upon observe for %d",
       unit);
  propagator->notify_assignment (unit, true);
}

void External::remove_observed_var (int elit) {
  if (!propagator) {
    LOG ("No connected propagator that could have watched the variable");
    return;
  }
  int eidx = abs (elit);

  if (eidx > max_var)
    return;

  if (is_observed[eidx]) {
    // Follow opposite order of add_observed_var, first remove internal
    // is_observed
    int ilit = e2i[eidx]; // internalize (elit);
    internal->remove_observed_var (ilit);

    melt (elit);
    is_observed[eidx] = false;
    LOG ("unmarking %d as externally watched", eidx);
  }
}

void External::reset_observed_vars () {
  // Shouldn't be called if there is no connected propagator
  assert (propagator);
  reset_extended ();
  assert ((size_t) max_var + 1 == is_observed.size ());

  for (auto elit : vars) {
    int eidx = abs (elit);
    assert (eidx <= max_var);
    if (is_observed[eidx]) {
      int ilit = internalize (elit);
      internal->remove_observed_var (ilit);
      LOG ("unmarking %d as externally watched", eidx);
      melt (elit);
    }
    is_observed[eidx] = false;
  }
  internal->notified = 0;
  LOG ("reset notified counter to 0");
}

bool External::observed (int elit) {
  assert (elit);
  assert (elit != INT_MIN);
  int eidx = abs (elit);
  if (eidx > max_var)
    return false;
  if (eidx >= (int) is_observed.size ())
    return false;

  return is_observed[eidx];
}

bool External::is_witness (int elit) {
  assert (elit);
  assert (elit != INT_MIN);
  int eidx = abs (elit);
  if (eidx > max_var)
    return false;
  return (marked (witness, elit) || marked (witness, -elit));
}

bool External::is_decision (int elit) {
  assert (elit);
  assert (elit != INT_MIN);
  int eidx = abs (elit);
  if (eidx > max_var)
    return false;

  int ilit = internalize (elit);
  return internal->is_decision (ilit);
}

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

// Internal checker if 'solve' claims the formula to be satisfiable.

void External::check_satisfiable () {
  LOG ("checking satisfiable");
  if (!extended)
    extend ();
  if (internal->opts.checkwitness)
    check_assignment (&External::ival);
  if (internal->opts.checkassumptions && !assumptions.empty ())
    check_assumptions_satisfied ();
  if (internal->opts.checkconstraint && !constraint.empty ())
    check_constraint_satisfied ();
}

// Internal checker if 'solve' claims formula to be unsatisfiable.

void External::check_unsatisfiable () {
  LOG ("checking unsatisfiable");
  if (!internal->opts.checkfailed)
    return;
  if (!assumptions.empty () || !constraint.empty ())
    check_failing ();
}

// Check result of 'solve' to be correct.

void External::check_solve_result (int res) {
  if (!internal->opts.check)
    return;
  if (res == 10)
    check_satisfiable ();
  if (res == 20)
    check_unsatisfiable ();
}

// Prepare checking that completely molten literals are not used as argument
// of 'add' or 'assume', which is invalid under freezing semantics.  This
// case would be caught by our 'restore' implementation so is only needed
// for checking the deprecated 'freeze' semantics.

void External::update_molten_literals () {
  if (!internal->opts.checkfrozen)
    return;
  assert ((size_t) max_var + 1 == moltentab.size ());
#ifdef LOGGING
  int registered = 0, molten = 0;
#endif
  for (auto lit : vars) {
    if (moltentab[lit]) {
      LOG ("skipping already molten literal %d", lit);
#ifdef LOGGING
      molten++;
#endif
    } else if (frozen (lit))
      LOG ("skipping currently frozen literal %d", lit);
    else {
      LOG ("new molten literal %d", lit);
      moltentab[lit] = true;
#ifdef LOGGING
      registered++;
      molten++;
#endif
    }
  }
  LOG ("registered %d new molten literals", registered);
  LOG ("reached in total %d molten literals", molten);
}

int External::solve (bool preprocess_only) {
  reset_extended ();
  update_molten_literals ();
  int res = internal->solve (preprocess_only);
  check_solve_result (res);
  reset_limits ();
  return res;
}

void External::terminate () { internal->terminate (); }

int External::lookahead () {
  reset_extended ();
  update_molten_literals ();
  int ilit = internal->lookahead ();
  const int elit =
      (ilit && ilit != INT_MIN) ? internal->externalize (ilit) : 0;
  LOG ("lookahead internal %d external %d", ilit, elit);
  return elit;
}

CaDiCaL::CubesWithStatus External::generate_cubes (int depth,
                                                   int min_depth = 0) {
  reset_extended ();
  update_molten_literals ();
  reset_limits ();
  auto cubes = internal->generate_cubes (depth, min_depth);
  auto externalize = [this] (int ilit) {
    const int elit = ilit ? internal->externalize (ilit) : 0;
    MSG ("lookahead internal %d external %d", ilit, elit);
    return elit;
  };
  auto externalize_map = [this, externalize] (std::vector<int> cube) {
    (void) this;
    MSG ("Cube : ");
    std::for_each (begin (cube), end (cube), externalize);
  };
  std::for_each (begin (cubes.cubes), end (cubes.cubes), externalize_map);

  return cubes;
}

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

void External::freeze (int elit) {
  reset_extended ();
  int ilit = internalize (elit);
  unsigned eidx = vidx (elit);
  if (eidx >= frozentab.size ())
    frozentab.resize (eidx + 1, 0);
  unsigned &ref = frozentab[eidx];
  if (ref < UINT_MAX) {
    ref++;
    LOG ("external variable %d frozen once and now frozen %u times", eidx,
         ref);
  } else
    LOG ("external variable %d frozen but remains frozen forever", eidx);
  internal->freeze (ilit);
}

void External::melt (int elit) {
  reset_extended ();
  int ilit = internalize (elit);
  unsigned eidx = vidx (elit);
  assert (eidx < frozentab.size ());
  unsigned &ref = frozentab[eidx];
  assert (ref > 0);
  if (ref < UINT_MAX) {
    if (!--ref)
      LOG ("external variable %d melted once and now completely melted",
           eidx);
    else
      LOG ("external variable %d melted once but remains frozen %u times",
           eidx, ref);
  } else
    LOG ("external variable %d melted but remains frozen forever", eidx);
  internal->melt (ilit);
}

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

void External::check_assignment (int (External::*a) (int) const) {

  // First check all assigned and consistent.
  //
  for (auto idx : vars) {
    if (!(this->*a) (idx))
      FATAL ("unassigned variable: %d", idx);
    if ((this->*a) (idx) != -(this->*a) (-idx))
      FATAL ("inconsistently assigned literals %d and %d", idx, -idx);
  }

  // Then check that all (saved) original clauses are satisfied.
  //
  bool satisfied = false;
  const auto end = original.end ();
  auto start = original.begin (), i = start;
#ifndef QUIET
  int64_t count = 0;
#endif
  for (; i != end; i++) {
    int lit = *i;
    if (!lit) {
      if (!satisfied) {
        fatal_message_start ();
        fputs ("unsatisfied clause:\n", stderr);
        for (auto j = start; j != i; j++)
          fprintf (stderr, "%d ", *j);
        fputc ('0', stderr);
        fatal_message_end ();
      }
      satisfied = false;
      start = i + 1;
#ifndef QUIET
      count++;
#endif
    } else if (!satisfied && (this->*a) (lit) > 0)
      satisfied = true;
  }
  VERBOSE (1, "satisfying assignment checked on %" PRId64 " clauses",
           count);
}

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

void External::check_assumptions_satisfied () {
  for (const auto &lit : assumptions) {
    // Not 'signed char' !!!!
    const int tmp = ival (lit);
    if (tmp < 0)
      FATAL ("assumption %d falsified", lit);
    if (!tmp)
      FATAL ("assumption %d unassigned", lit);
  }
  VERBOSE (1, "checked that %zd assumptions are satisfied",
           assumptions.size ());
}

void External::check_constraint_satisfied () {
  for (const auto lit : constraint) {
    if (ival (lit) > 0) {
      VERBOSE (1, "checked that constraint is satisfied");
      return;
    }
  }
  FATAL ("constraint not satisfied");
}

void External::check_failing () {
  Solver *checker = new Solver ();
  checker->prefix ("checker ");
#ifdef LOGGING
  if (internal->opts.log)
    checker->set ("log", true);
#endif
  for (const auto lit : original)
    checker->add (lit);
  for (const auto lit : assumptions) {
    if (!failed (lit))
      continue;
    LOG ("checking failed literal %d in core", lit);
    checker->add (lit);
    checker->add (0);
  }
  if (failed_constraint ()) {
    LOG (constraint, "checking failed constraint");
    for (const auto lit : constraint)
      checker->add (lit);
  } else if (constraint.size ())
    LOG (constraint, "constraint satisfied and ignored");
  int res = checker->solve ();
  if (res != 20)
    FATAL ("failed assumptions do not form a core");
  delete checker;
  VERBOSE (1, "checked that %zd failing assumptions form a core",
           assumptions.size ());
}

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

// Traversal of unit clauses is implemented here.

// In principle we want to traverse the clauses of the simplified formula
// only, particularly eliminated variables should be completely removed.
// This poses the question what to do with unit clauses.  Should they be
// considered part of the simplified formula or of the witness to construct
// solutions for the original formula?  Ideally they should be considered
// to be part of the witness only, i.e., as they have been simplified away.

// Therefore we distinguish frozen and non-frozen units during clause
// traversal.  Frozen units are treated as unit clauses while non-frozen
// units are treated as if they were already eliminated and put on the
// extension stack as witness clauses.

// Furthermore, eliminating units during 'compact' could be interpreted as
// variable elimination, i.e., just add the resolvents (remove falsified
// literals), then drop the clauses with the unit, and push the unit on the
// extension stack.  This is of course only OK if the user did not freeze
// that variable (even implicitly during assumptions).

// Thanks go to Fahiem Bacchus for asking why there is a necessity to
// distinguish these two cases (frozen and non-frozen units).  The answer is
// that it is not strictly necessary, and this distinction could be avoided
// by always treating units as remaining unit clauses, thus only using the
// first of the two following functions and dropping the 'if (!frozen (idx))
// continue;' check in it.  This has however the down-side that those units
// are still in the simplified formula and only as units.  I would not
// consider such a formula as really being 'simplified'. On the other hand
// if the user explicitly freezes a literal, then it should continue to be
// in the simplified formula during traversal.  So also only using the
// second function is not ideal.

// There is however a catch where this solution breaks down (in the sense of
// producing less optimal results - that is keeping units in the formula
// which better would be witness clauses).  The problem is with compact
// preprocessing which removes eliminated but also fixed internal variables.
// One internal unit (fixed) variable is kept and all the other external
// literals which became unit are mapped to that internal literal (negated
// or positively).  Compact is called non-deterministically from the point
// of the user and thus there is no control on when this happens.  If
// compact happens those external units are mapped to a single internal
// literal now and then all share the same 'frozen' counter.   So if the
// user freezes one of them all in essence get frozen, which in turn then
// makes a difference in terms of traversing such a unit as unit clause or
// as unit witness.

bool External::traverse_all_frozen_units_as_clauses (ClauseIterator &it) {
  if (internal->unsat)
    return true;

  vector<int> clause;

  for (auto idx : vars) {
    if (!frozen (idx))
      continue;
    const int tmp = fixed (idx);
    if (!tmp)
      continue;
    int unit = tmp < 0 ? -idx : idx;
    clause.push_back (unit);
    if (!it.clause (clause))
      return false;
    clause.clear ();
  }

  return true;
}

bool External::traverse_all_non_frozen_units_as_witnesses (
    WitnessIterator &it) {
  if (internal->unsat)
    return true;

  vector<int> clause_and_witness;

  for (auto idx : vars) {
    if (frozen (idx))
      continue;
    const int tmp = fixed (idx);
    if (!tmp)
      continue;
    int unit = tmp < 0 ? -idx : idx;
    clause_and_witness.push_back (unit);
    if (!it.witness (clause_and_witness, clause_and_witness))
      return false;
    clause_and_witness.clear ();
  }

  return true;
}

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

void External::copy_flags (External &other) const {
  const vector<Flags> &this_ftab = internal->ftab;
  vector<Flags> &other_ftab = other.internal->ftab;
  const unsigned limit = min (max_var, other.max_var);
  for (unsigned eidx = 1; eidx <= limit; eidx++) {
    const int this_ilit = e2i[eidx];
    if (!this_ilit)
      continue;
    const int other_ilit = other.e2i[eidx];
    if (!other_ilit)
      continue;
    if (!internal->active (this_ilit))
      continue;
    if (!other.internal->active (other_ilit))
      continue;
    assert (this_ilit != INT_MIN);
    assert (other_ilit != INT_MIN);
    const Flags &this_flags = this_ftab[abs (this_ilit)];
    Flags &other_flags = other_ftab[abs (other_ilit)];
    this_flags.copy (other_flags);
  }
}

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

void External::export_learned_empty_clause () {
  assert (learner);
  if (learner->learning (0)) {
    LOG ("exporting learned empty clause");
    learner->learn (0);
  } else
    LOG ("not exporting learned empty clause");
}

void External::export_learned_unit_clause (int ilit) {
  assert (learner);
  if (learner->learning (1)) {
    LOG ("exporting learned unit clause");
    const int elit = internal->externalize (ilit);
    assert (elit);
    learner->learn (elit);
    learner->learn (0);
  } else
    LOG ("not exporting learned unit clause");
}

void External::export_learned_large_clause (const vector<int> &clause) {
  assert (learner);
  size_t size = clause.size ();
  assert (size <= (unsigned) INT_MAX);
  if (learner->learning ((int) size)) {
    LOG ("exporting learned clause of size %zu", size);
    for (auto ilit : clause) {
      const int elit = internal->externalize (ilit);
      assert (elit);
      learner->learn (elit);
    }
    learner->learn (0);
  } else
    LOG ("not exporting learned clause of size %zu", size);
}

} // namespace CaDiCaL
