/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
/*
 *  Main authors:
 *     Christian Schulte <schulte@gecode.org>
 *
 *  Copyright:
 *     Christian Schulte, 2007
 *
 *  Last modified:
 *     $Date: 2008-07-11 10:26:26 +0200 (Fri, 11 Jul 2008) $ by $Author: tack $
 *     $Revision: 7330 $
 *
 *  This file is part of Gecode, the generic constraint
 *  development environment:
 *     http://www.gecode.org
 *
 *  Permission is hereby granted, free of charge, to any person obtaining
 *  a copy of this software and associated documentation files (the
 *  "Software"), to deal in the Software without restriction, including
 *  without limitation the rights to use, copy, modify, merge, publish,
 *  distribute, sublicense, and/or sell copies of the Software, and to
 *  permit persons to whom the Software is furnished to do so, subject to
 *  the following conditions:
 *
 *  The above copyright notice and this permission notice shall be
 *  included in all copies or substantial portions of the Software.
 *
 *  THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
 *  EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
 *  MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
 *  NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
 *  LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
 *  OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
 *  WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 *
 */

namespace Gecode { namespace Int { namespace Circuit {

  template <class View>
  forceinline
  Base<View>::Base(Space* home, ViewArray<View>& x)
    : NaryPropagator<View,PC_INT_DOM>(home,x), y(home,x) {}

  template <class View>
  forceinline
  Base<View>::Base(Space* home, bool share, Base<View>& p)
    : NaryPropagator<View,PC_INT_DOM>(home,share,p) {
    y.update(home,share,p.y);
  }

  /// Information required for non-recursive checking for a single scc
  template <class View>
  class SsccInfo {
  public:
    int min, low, pre;
    ViewValues<View> v;
  };

  /// Information for performing a recorded tell
  template<class View>
  class TellInfo {
  public:
    View x; int n;
  };

  template <class View>
  ExecStatus
  Base<View>::connected(Space* home) {
    int n = x.size();

    /// First non-assigned node.
    int start = 0;
    while (x[start].assigned()) {
      start = x[start].val();
      if (start == 0) break;
    }

    /// Information needed for checking scc's
    GECODE_AUTOARRAY(SsccInfo<View>,si,n);
    unsigned int n_edges = 0;
    for (int i=n; i--; ) {
      n_edges += x[i].size();
      si[i].pre=-1;
    }

    // Stack to remember which nodes have not been processed completely
    GECODE_AUTOSTACK(int,-1,next,n);

    // Array to remember which mandatory tells need to be done
    GECODE_AUTOARRAY(TellInfo<View>,eq,n);
    int n_eq = 0;

    // Array to remember which edges need to be pruned
    GECODE_AUTOARRAY(TellInfo<View>,nq,n_edges);
    int n_nq = 0;

    /* 
     * Check whether there is a single strongly connected component.
     * This is a downstripped version of Tarjan's algorithm as
     * the computation of sccs proper is not needed. In addition, it
     * checks a mandatory condition for a graph to be Hamiltonian
     * (due to Mats Carlsson).
     *
     * To quote Mats: Suppose you do a depth-first search of the graph. 
     * In that search, the root node will have a number of child subtrees 
     * T1, ..., Tn. By construction, if i<j then there is no edge from 
     * Ti to Tj. The necessary condition for Hamiltonianicity is that 
     * there be an edge from Ti+1 to Ti, for 0 < i < n.
     *
     * In addition, we do the following: if there is only a single edge
     * from Ti+1 to Ti, then it must be mandatory and the variable must
     * be assigned to that value.
     *
     * The same holds true for a back edge from T0 to the root node.
     *
     * Then, all edges that reach from Ti+k+1 to Ti can be pruned.
     *
     */

    // Start always at node start
    int i = start;
    // Counter for scc
    int cnt = 0;
    // Smallest preorder number of last subtree (initially, the root node)
    int subtree_min = 0;
    // Largest preorder number of last subtree (initially, the root node)
    int subtree_max = 0;
    // Number of back edges into last subtree or root
    int back = 0;
  start:
    si[i].min = si[i].pre = si[i].low = cnt++;
    si[i].v.init(x[i]);
    do {
      if (si[si[i].v.val()].pre < 0) {
        next.push(i);
        i=si[i].v.val();
        goto start;
      } else if ((subtree_min <= si[si[i].v.val()].pre) &&
                 (si[si[i].v.val()].pre <= subtree_max)) {
        back++;
        eq[n_eq].x = x[i];
        eq[n_eq].n = si[i].v.val();
      } else if (si[si[i].v.val()].pre < subtree_min) {
        nq[n_nq].x = x[i];
        nq[n_nq].n = si[i].v.val();
        n_nq++;
      }
    cont:
      if (si[si[i].v.val()].low < si[i].min)
        si[i].min = si[si[i].v.val()].low;
      ++si[i].v;
    } while (si[i].v());
    if (si[i].min < si[i].low) {
      si[i].low = si[i].min;
    } else if (i != start) {
      // If it is not the first node visited, there is more than one SCC
      return ES_FAILED;
    }
    if (!next.empty()) {
      i=next.pop(); 
      if (i == start) {
        // No back edge
        if (back == 0)
          return ES_FAILED;
        // Exactly one back edge, make it mandatory (keep topmost entry on ti)
        if (back == 1)
          n_eq++;
        back        = 0;
        subtree_min = subtree_max+1;
        subtree_max = cnt-1;
      }
      goto cont;
    }
    // Whether all nodes have been visited
    if (cnt != n)
      return ES_FAILED;
    ExecStatus es = ES_FIX;
    // Assign all mandatory edges
    while (n_eq-- > 0) {
      ModEvent me = eq[n_eq].x.eq(home,eq[n_eq].n);
      if (me_failed(me))
        return ES_FAILED;
      if (me_modified(me))
        es = ES_NOFIX;
    }      
    // Remove all edges that would require a non-simple cycle
    while (n_nq-- > 0) {
      ModEvent me = nq[n_nq].x.nq(home,nq[n_nq].n);
      if (me_failed(me))
        return ES_FAILED;
      if (me_modified(me))
        es = ES_NOFIX;
    }      
    return es;
  }

  template <class View>
  ExecStatus
  Base<View>::path(Space* home) {
    // Prunes that partial assigned paths are not completed to cycles

    int n=x.size();

    // The path starting at assigned x[i] ends at x[end[j]] which is
    // not assigned.
    GECODE_AUTOARRAY(int,end,n);
    for (int i=n; i--; )
      end[i]=-1;

    // A stack that records all indices i such that end[i] != -1
    GECODE_AUTOSTACK(int,-1,tell,n);

    for (int i=y.size(); i--; ) {
      assert(!y[i].assigned());
      // Non-assigned views serve as starting points for assigned paths
      ViewValues<View> v(y[i]);
      // Try all connected values
      do {
        int j0=v.val();
        // Starting point for not yet followed assigned path found
        if (x[j0].assigned() && (end[j0] < 0)) {
          // Follow assigned path until non-assigned view:
          // all assigned view on the paths can be skipped, as
          // if x[i] is assigned to j, then x[j] will only have
          // x[i] as predecessor due to propagating distinct.
          int j = j0;
          do {
            j=x[j].val();
          } while (x[j].assigned());
          // Now there cannot be a cycle from x[j] to x[v.val()]!
          // However, the tell cannot be done here as j might be
          // equal to i and might hence kill the iterator v!
          end[j0]=j; tell.push(j0);
        }
        ++v;
      } while (v());
    }

    // Now do the tells based on the end information
    while (!tell.empty()) {
      int i = tell.pop();
      assert(end[i] >= 0);
      GECODE_ME_CHECK(x[end[i]].nq(home,i));
    }
    return ES_NOFIX;
  }

  template <class View>
  forceinline size_t
  Base<View>::dispose(Space* home) {
    (void) NaryPropagator<View,PC_INT_DOM>::dispose(home);
    return sizeof(*this);
  }

  template <class View>
  Reflection::ActorSpec
  Base<View>::spec(const Space* home, Reflection::VarMap& m,
                   const Support::Symbol& name) const {
    return NaryPropagator<View,PC_INT_DOM>::spec(home, m, name);                   
  }

}}}

// STATISTICS: int-prop