/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
/*
 *  Main authors:
 *     Patrick Pekczynski <pekczynski@ps.uni-sb.de>
 *
 *  Copyright:
 *     Patrick Pekczynski, 2006
 *
 *  Last modified:
 *     $Date: 2008-01-31 18:29:16 +0100 (Thu, 31 Jan 2008) $ by $Author: tack $
 *     $Revision: 6017 $
 *
 *  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 CpltSet {

  template <class View>
  forceinline bdd 
  NaryCpltSetPropagator<View>::bnd_phi(int j) {
    /// \f$ B(c)\f$
    if (j == -1) {
      return d;
    }

    /// \f$ D_j \f$
    bdd cur = x[j].dom();
    /// \f$ \phi_{j - 1}\f$
    bdd phires = bnd_phi(j - 1);
    /// \f$ \exists_{V(D_j)} D_j \wedge phi_{j - 1}\f$

    // strange
    if (!manager.ctrue(cur)) {    
      bdd outvars = bdd_vars(cur);
      manager.existquant(cur, phires, outvars);
    } else {
      cur &= phires;
    }
    return cur;
  }

  // used in eeq propagation with n*n and-abstractions
  template <class View>
  forceinline bdd 
  NaryCpltSetPropagator<View>::phi(int i, int j) {
    // \f$ B(c)\f$
    if (j == -1) {
      return d;
    }
    // \f$ phi_i^{j - 1}\f$
    if (j == i) {
      return phi(i, j - 1);
    }

    bdd cur = bdd_true();
    // \f$ D_j \f$
    cur &= x[j].dom();
    // \f$ \phi_i^{j - 1}\f$
    cur &= phi(i, j - 1);
    // \f$ \exists_{V(x_j)} D_j \wedge phi_i^{j - 1}\f$
    int start = x[j].offset();
    int end   = start + x[j].tableWidth() - 1;
    return manager.eliminate(cur, start, end);
  }

  template <class View>
  forceinline
  NaryCpltSetPropagator<View>::NaryCpltSetPropagator(Space* home, 
                                                     ViewArray<View>& x0,
                                                     bdd& d0)
    : Propagator(home), x(x0), d(d0) {
    force(home);
    for (int i = x.size(); i--;) {
      x[i].subscribe(home, this, PC_CPLTSET_DOM);
    }
  }

  template <class View>
  forceinline
  NaryCpltSetPropagator<View>::NaryCpltSetPropagator(Space* home, bool share, 
                                                     NaryCpltSetPropagator& p)
    : Propagator(home,share,p) {
    d = p.d;
    x.update(home,share,p.x);
  }
  
  template <class View>
  forceinline PropCost
  NaryCpltSetPropagator<View>::cost(ModEventDelta) const {
    return PC_CRAZY_HI;
  }

  template <class View>
  Support::Symbol
  NaryCpltSetPropagator<View>::ati(void) {
    return Reflection::mangle<View>("Gecode::CpltSet::NaryCpltSetPropagator");
  }

  template <class View>
  Reflection::ActorSpec
  NaryCpltSetPropagator<View>::spec(const Space*, Reflection::VarMap&) const {
    throw Reflection::ReflectionException("Not implemented");
  } 
 
  template <class View>
  size_t
  NaryCpltSetPropagator<View>::dispose(Space* home) {
    unforce(home);
    if (!home->failed()) {
      for (int i = x.size(); i--;) {
        x[i].cancel(home, this, PC_CPLTSET_DOM);
      }
    }
    manager.dispose(d);
    Propagator::dispose(home);
    return sizeof(*this);
  }

  template <class View>
  forceinline ExecStatus
  NaryCpltSetPropagator<View>::post(Space* home, ViewArray<View>& x, bdd& d) {
    (void) new (home) NaryCpltSetPropagator(home,x, d);
    return ES_OK;
  }

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

  template <class View>
  ExecStatus
  NaryCpltSetPropagator<View>::divide_conquer(Space* home,
                                              bdd& p, int l, int r) {
    if (l == r) {
      GECODE_ME_CHECK(x[l].intersect(home, p));
      return ES_OK;
    }

    int h = (r + l) / 2;

    // computing psi without recursion
    bdd left = p;
    for (int i = r; i >= h + 1; i--) {
      quantify(left, x[i]);
    }
   
    ExecStatus es = ES_OK;
    GECODE_ES_CHECK(es = divide_conquer(home, left, l, h));

    bdd right = p;
    for (int i = h; i >= l; i-- ) {
      quantify(right, x[i]);
    }

    GECODE_ES_CHECK(es = divide_conquer(home, right, h + 1, r));
    return es;
  }

  template <class View>
  forceinline ExecStatus 
  NaryCpltSetPropagator<View>::propagate(Space* home, ModEventDelta) {
    bool assigned = true;
    int n = x.size();
    
    ExecStatus es = ES_OK;
    if (n == 1) {
      GECODE_ME_CHECK(x[0].intersect(home, d));
    } else {
      GECODE_ES_CHECK(es = divide_conquer(home, d, 0, n - 1));
    }

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

    if (assigned) {
      return ES_SUBSUMED(this, home);
    }

    return ES_FIX;
  }

}}

// STATISTICS: cpltset-prop