/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
/*
 *  Main authors:
 *     Patrick Pekczynski <pekczynski@ps.uni-sb.de>
 *
 *  Copyright:
 *     Patrick Pekczynski, 2004
 *
 *  Last modified:
 *     $Date: 2008-07-11 09:32:27 +0200 (Fri, 11 Jul 2008) $
       $Author: tack $
 *     $Revision: 7289 $
 *
 *  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 GCC {

  /*
   * Analogously to "gcc/bnd.icc" we split the algorithm
   * in two parts:
   *   1) the UBC (Upper Bound Constraint) stating that there are
   *      at most k[i].max() occurences of the value v_i
   *   2) the LBC (Lower Bound Constraint) stating that there are
   *      at least k[i].min() occurences of the value v_i
   *
   * The algorithm proceeds in 5 STEPS:
   *
   * STEP 1:
   *    Build the bipartite value-graph G=(<X,D>,E),
   *    with X = all variable nodes (each variable forms a node)
   *         D = all value nodes (union over all domains of the variables)
   *    and (x_i,v) is an edge in G iff value v is in the domain D_i of x_i
   *
   * STEP 2:   Compute a matching in the value graph.
   * STEP 3:   Compute all even alternating paths from unmatched  nodes
   * STEP 4:   Compute strongly connected components in the merged graph
   * STEP 5:   Update the Domains according to the computed edges
   *
   */

  template <class View, class Card, bool isView>
  inline
  Dom<View, Card, isView>::Dom(Space* home, ViewArray<View>& x0,
                               ViewArray<Card>& k0, bool cf)
    : Propagator(home), x(x0),  y(home, x0),
      k(k0), vvg(NULL), card_fixed(cf){
    // y is used for bounds propagation since prop_bnd needs all variables
    // values within the domain bounds
    force(home);
    x.subscribe(home, this, PC_INT_DOM);
    k.subscribe(home, this, PC_INT_DOM);
  }

  template <class View, class Card, bool isView>
  forceinline
  Dom<View, Card, isView>::Dom(Space* home, bool share,
                               Dom<View, Card, isView>& p)
    : Propagator(home, share, p), vvg(NULL), card_fixed(p.card_fixed) {
    x.update(home, share, p.x);
    y.update(home, share, p.y);
    k.update(home, share, p.k);
  }

  template <class View, class Card, bool isView>
  size_t
  Dom<View, Card, isView>::dispose(Space* home) {
    unforce(home);
    if (!home->failed()) {
      x.cancel(home,this, PC_INT_DOM);
      k.cancel(home,this, PC_INT_DOM);
    }
    delete vvg;
    (void) Propagator::dispose(home);
    return sizeof(*this);
  }

  template <class View, class Card, bool isView>
  size_t
  Dom<View, Card, isView>::allocated(void) const {
    return (vvg == NULL) ? 0 : vvg->allocated();
  }

  template <class View, class Card, bool isView>
  Actor*
  Dom<View, Card, isView>::copy(Space* home, bool share) {
    return new (home) Dom<View, Card, isView>(home, share, *this);
  }

  template <class View, class Card, bool isView>
  PropCost
  Dom<View, Card, isView>::cost(ModEventDelta) const {

    unsigned int n = x.size();
    unsigned int d = x[n - 1].size();
    for (int i = n; i--; ) {
      if (x[i].size() > d) {
        d = x[i].size();
      }
    }

    PropCost pc;
    if (d < 6) {
      pc = PC_LINEAR_LO;
    } else {
      if (6 <= d && d < n/2) {
        pc = PC_LINEAR_HI;
      }
      else {
        if (n/2 <= d && d < n*n) {
          pc = PC_QUADRATIC_LO;
        } else {
          pc = PC_CUBIC_LO;
        }
      }
    }
    return cost_lo(x.size(), pc);

  }

  template <class View, class Card, bool isView>
  Support::Symbol
  Dom<View,Card,isView>::ati(void) {
    return Reflection::mangle<View,Card>("Gecode::Int::GCC::Dom",isView);
  }

  template <class View, class Card, bool isView>
  Reflection::ActorSpec
  Dom<View,Card,isView>::spec(const Space* home,
                              Reflection::VarMap& m) const {
    Reflection::ActorSpec s(ati());
    return s << y.spec(home, m) << k.spec(home, m) << card_fixed;
  }

  template <class View, class Card, bool isView>
  void
  Dom<View,Card,isView>::post(Space* home, Reflection::VarMap& vars,
                              const Reflection::ActorSpec& spec) {
    spec.checkArity(3);
    ViewArray<View> x(home, vars, spec[0]);
    ViewArray<Card> k(home, vars, spec[1]);
    bool card_fixed = spec[2]->toInt();
    (void) new (home) Dom(home, x, k, card_fixed);
  }
  
  /// \brief Perform domain propagation.
  template <class View, class Card, bool isView>
  ExecStatus
  Dom<View, Card, isView>::propagate(Space* home, ModEventDelta) {

    ExecStatus es = ES_NOFIX;
    bool card_mod = false;

    GECODE_AUTOARRAY(int, count, k.size());
    for (int i = k.size(); i--; ) {
      count[i] = 0;
    }
    bool all_assigned = true;
    // total number of assigned views
    int noa = 0;
    for (int i = y.size(); i--; ) {
      bool b = y[i].assigned();
      all_assigned &= b;
      if (b) {
        noa++;
        int idx = lookupValue(k, y[i].val());
        if (idx == -1) {
          return ES_FAILED;
        }
        count[idx]++;
        if (isView) {
          if (k[idx].max() == 0) {
            return ES_FAILED;
          }
        }
      }
    }

    if (all_assigned) {
      for (int i = k.size(); i--; ) {
        int ci = count[i];
        if (!(k[i].min() <= ci && ci <= k[i].max())) {
          return ES_FAILED;
        }
        // the solution contains ci occurences of value k[i].card();
        if (isView) {
          if (!k[i].assigned()) {
            ModEvent me = k[i].eq(home, ci);
            if (me_failed(me))
              return ES_FAILED;
            card_mod |= me_modified(me);
          }
          all_assigned &= k[i].assigned();
        }
      }
      if (all_assigned)
        return ES_SUBSUMED(this,home);
    }

    // before propagation performs inferences on cardinality variables:
    if (isView) {
      if (noa > 0) {
        int n  = y.size();
        int ks = k.size();

        for (int i = ks; i--; ) {
          if (!k[i].assigned()) {
            int ub = n - (noa - count[i]);
            int lb = count[i];
            ModEvent melq = k[i].lq(home, ub);
            if (me_failed(melq))
              return ES_FAILED;
            card_mod |= me_modified(melq);

            ModEvent megq = k[i].gq(home, lb);
            if (me_failed(megq))
              return ES_FAILED;
            card_mod |= me_modified(megq);
          }
        }
      }

      GECODE_ES_CHECK((prop_card<View, Card, true>(home, y, k, card_mod)));

      int smin = 0;
      int smax = 0;
      if (!card_consistent<View, Card>(smin, smax, y, k)) {
        return ES_FAILED;
      }
    }

    if (x.size() < 2) {
      assert(x.size() >= 0);
      if (x.size() == 0) {
        for (int j = k.size(); j--; ) {
          if (k[j].min() > k[j].counter() || k[j].max() < k[j].counter()) {
            return ES_FAILED;
          }
        }
        return ES_SUBSUMED(this,home);
      } else {
        if (x.size() == 1) {
          if (x[0].assigned()) {
            int v = x[0].val();
            int idx = lookupValue(k,v);
            if (idx == -1) {
              return ES_FAILED;
            }
            ModEvent me = k[idx].inc();
            if (me_failed(me))
              return ES_FAILED;
            card_mod |= me_modified(me);
            for (int j = k.size(); j--; )
              if (k[j].min() > k[j].counter() || k[j].max() < k[j].counter())
                return ES_FAILED;
            return ES_SUBSUMED(this,home);
          }
        }
      }
    }

    assert(x.size() > 0);

    bool mod = false;
    bool min_req_mod = false;
    int noe     = 0;
    int smin    = 0;
    int smax    = 0;
    assert(noe >= 0);
    for (int i = x.size(); i--; ) {
      noe +=x[i].size();
    }

    assert(noe > 0);

    for (int i = k.size(); i--; ) {
      int ci = k[i].counter();
      if (ci > k[i].max() ) {
        return ES_FAILED;
      } else {
        smax += (k[i].max() - ci);
        if (ci < k[i].min()) {
          smin += (k[i].min() - ci);
        }
      }
    }

    if (x.size() < smin) {
      return ES_FAILED;
    }

    if (smax < x.size()) {
      return ES_FAILED;
    }


    if (vvg == NULL) {
      assert(noe > 0);
      assert(smin >= 0);
      assert(smax >= 0);
      vvg = new VarValGraph<View, Card, isView> (x, y, k, noe, smin, smax);
      min_req_mod = vvg->min_require(home);
      if (vvg->failed()) {
        return ES_FAILED;
      }

      bool init_ubm = vvg->template maximum_matching<UBC>();
      if (!init_ubm) {
        return ES_FAILED;
      }

      if (!card_fixed) {
        bool init_lbm = vvg->template maximum_matching<LBC>();
        if (!init_lbm) {
          return ES_FAILED;
        }
      }
    } else {
      if (!vvg->sync()) {
        return ES_FAILED;
      }
    }

    bool filter_ubc = false;
    bool filter_lbc = false;

    vvg->template free_alternating_paths<UBC>();
    vvg->template strongly_connected_components<UBC>();

    filter_ubc = vvg->template narrow<UBC>(home);
    if (vvg->failed()) {
      return ES_FAILED;
    }
    if (!card_fixed) {
      if (isView) {
        if (!vvg->sync()) {
          return ES_FAILED;
        }
      }
      vvg->template free_alternating_paths<LBC>();
      vvg->template strongly_connected_components<LBC>();

      filter_lbc = vvg->template narrow<LBC>(home);
      if (vvg->failed()) {
        return ES_FAILED;
      }
    }

    bool card_assigned = true;
    if (isView) {
      es = prop_card<View, Card, true>(home, y, k, card_mod);
      if (es == ES_FAILED) {
        return ES_FAILED;
      }

      for (int i = k.size(); i--; ) {
        card_assigned &= k[i].assigned();
      }
    }

    if (card_assigned) {
      if (x.size() < 2) {
        assert(x.size() >= 0);
        if (x.size() == 0) {
          for (int j = k.size(); j--; ) {
            if (k[j].min() > k[j].counter() ||
                k[j].max() < k[j].counter()) {
              return ES_FAILED;
            }
          }
          return ES_SUBSUMED(this,home);
        } else {
          if (x.size() == 1) {
            if (x[0].assigned()) {
              int v = x[0].val();
              int idx = lookupValue(k,v);
              if (idx == -1) {
                return ES_FAILED;
              }
              ModEvent me = k[idx].inc();
              if (me_failed(me)) {
                return ES_FAILED;
              }
              card_mod |= me_modified(me);

              for (int j = k.size(); j--; ) {
                if (k[j].min() > k[j].counter() ||
                    k[j].max() < k[j].counter()) {
                  return ES_FAILED;
                }
              }
              return ES_SUBSUMED(this,home);
            }
          }
        }
      }
    }

    for (int i = k.size(); i--; ) {
      count[i] = 0;
    }
    all_assigned = true;
    // total number of assigned views
    for (int i = y.size(); i--; ) {
      bool b = y[i].assigned();
      all_assigned &= b;
      if (b) {
        int idx = lookupValue(k,y[i].val());
        if (idx == -1) {
          return ES_FAILED;
        }
        count[idx]++;
        if (isView) {
          if (k[idx].max() == 0) {
            return ES_FAILED;
          }
        }
      }
    }

    if (isView) {
      es = prop_card<View, Card, true>(home, y, k, card_mod);
      if (es == ES_FAILED) {
        return es;
      }
    }

    if (all_assigned) {
      for (int i = k.size(); i--; ) {
        int ci = count[i];
        if (!(k[i].min() <= ci && ci <= k[i].max())) {
          return ES_FAILED;
        }
        // the solution contains ci occurences of value k[i].card();
        if (isView) {
          if (!k[i].assigned()) {
            ModEvent me = k[i].eq(home, ci);
            if (me_failed(me))
              return ES_FAILED;
            card_mod |= me_modified(me);
          }
          all_assigned &= k[i].assigned();
        }
      }
      if (all_assigned) {
        return ES_SUBSUMED(this,home);
      }
    }

    if (isView) {
      int smax = 0;
      int smin = 0;
      for (int i = k.size(); i--; ) {
        smax += k[i].max();
      }
      int ysmax = y.size() - smax;
      int ysmin = y.size() - smin;
      smax = 0;
      smin = 0;
      bool card_ass = true;
      for (int i = k.size(); i--; ) {
        int lb = ysmax + k[i].max();
        int ub = ysmin + k[i].min();
        ModEvent me = k[i].gq(home, lb);
        if (me_failed(me))
          return ES_FAILED;

        card_mod |= me_modified(me);
        smax += k[i].max();

        me = k[i].lq(home, ub);
        if (me_failed(me))
          return ES_FAILED;

        card_mod |= me_modified(me);        
        card_ass &= k[i].assigned();
      }
      if (card_ass) {
        if (smax < y.size() || smax > y.size()) {
          return ES_FAILED;
        }
      }
    }

    mod = (filter_ubc || filter_lbc || min_req_mod || card_mod);

    return mod ? ES_NOFIX : ES_FIX;

  }

  template <class View, class Card, bool isView>
  inline ExecStatus
  Dom<View, Card, isView>::post(Space* home, ViewArray<View>& x0,
                                ViewArray<Card>& k0){
    bool cardfix = true;
    for (int i = k0.size(); i--; ) {
      cardfix &= k0[i].assigned();
    }

    (void) new (home) Dom<View, Card, isView>(home, x0, k0, cardfix);
    return ES_OK;
  }

}}}



// STATISTICS: int-prop