/* -*- 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 View0, class View1>
  ExecStatus
  NaryTwoCpltSetPropagator<View0, View1>::divide_conquer(Space* home, bdd& p, 
                                      int l, int r, int ypos, int zpos) {
    if (l == r) {
      ModEvent me = ME_CPLTSET_NONE;
      if (l == ypos) {
        me  = y.intersect(home, p);
      } else {
        if (l == zpos) {
          me = z.intersect(home, p);
        } else {
          me = x[l].intersect(home, p);
        }
      }
      if (me_failed(me)) {
        return ES_FAILED;
      }
      return ES_OK;
    }
    int h = (r + l) / 2;

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

    bdd right = p;
    for (int i = h; i >= l; i-- ) {
      if (i == zpos) {
        quantify(right, z);
      } else {
        if (i == ypos) {
          quantify(right, y);
        } else {
          quantify(right, x[i]);
        }
      }
    }

    GECODE_ES_CHECK(es = divide_conquer(home, right, h + 1, r , ypos, zpos));
    return es;
  }
  
  template <class View0, class View1>
  forceinline
  NaryTwoCpltSetPropagator<View0, View1>
  ::NaryTwoCpltSetPropagator(Space* home, ViewArray<View0>& x0,
                             View1& y0, View1& z0, bdd&)
  : Propagator(home), x(x0), y(y0), z(z0) {
    Propagator::force(home);
    x.subscribe(home, this, PC_CPLTSET_DOM);
    y.subscribe(home, this, PC_CPLTSET_DOM);
    z.subscribe(home, this, PC_CPLTSET_DOM);
  }

  template <class View0, class View1>
  forceinline
  NaryTwoCpltSetPropagator<View0, View1>
  ::NaryTwoCpltSetPropagator(Space* home, bool share, 
                             NaryTwoCpltSetPropagator& p)
    : Propagator(home, share, p), d(p.d) {
    x.update(home,share,p.x);
    y.update(home,share,p.y);
    z.update(home,share,p.z);
  }

  template <class View0, class View1>
  forceinline ExecStatus
  NaryTwoCpltSetPropagator<View0, View1>::post(Space* home, ViewArray<View0>& x, 
                            View1& y, View1& z, bdd& d0) {
    (void) new (home) NaryTwoCpltSetPropagator(home, x, y, z, d0);
    return ES_OK;
  }

  template <class View0, class View1>
  Support::Symbol
  NaryTwoCpltSetPropagator<View0, View1>::ati(void) {
    return 
      Reflection::mangle<View0,View1>("Gecode::CpltSet::NaryTwoCpltSetPropagator");
  }

  template <class View0, class View1>
  Reflection::ActorSpec
  NaryTwoCpltSetPropagator<View0,View1>::spec(const Space*,
                                              Reflection::VarMap&) const {
    throw Reflection::ReflectionException("Not implemented");
  } 

  template <class View0, class View1>
  forceinline Actor*
  NaryTwoCpltSetPropagator<View0, View1>::copy(Space* home, bool share) {
    return new (home) NaryTwoCpltSetPropagator(home, share, *this);
  }
  
  template <class View0, class View1>
  forceinline ExecStatus 
  NaryTwoCpltSetPropagator<View0, View1>::propagate(Space* home, ModEventDelta) {
    bool assigned = true;
    int n = x.size();
    ExecStatus es = ES_OK;
    int ypos = n;
    int zpos = n + 1;

    GECODE_ES_CHECK(es = divide_conquer(home, d, 0, n + 1, ypos, zpos));

    assigned = true;
    for (int i = x.size(); i--; ) {
      assigned &= x[i].assigned();
    }
    if (assigned) {
      return ES_SUBSUMED(this, home);
    }

    return ES_FIX;
  }

  template <class View0, class View1>
  PropCost
  NaryTwoCpltSetPropagator<View0,View1>::cost(ModEventDelta) const {
    return cost_lo(x.size()+2, PC_LINEAR_LO);
  }

  template <class View0, class View1>
  size_t
  NaryTwoCpltSetPropagator<View0, View1>::dispose(Space* home) {
    unforce(home);
    if (!home->failed()) {
      x.cancel(home, this, PC_CPLTSET_DOM);
      y.cancel(home, this, PC_CPLTSET_DOM);
      z.cancel(home, this, PC_CPLTSET_DOM);
    }
    manager.dispose(d);
    (void) Propagator::dispose(home);
    return sizeof(*this);
  }

}}

// STATISTICS: cpltset-prop