/* exactly-var(Xn, Y, k) == #{ x \in Xn | x = k } = Y */

static int fd_exactly_var_filter(fd_constraint this)
{
  int k, c;
  int set, possible;
  int value;
  int i;

  if (fd_var_single(VAR(this, this->nvariables - 1), &c))
    {
      k = this->constants[0];

      set = possible = 0;

      // count the variables that are set to k and those which contain k
      // in their domain
      for (i = 0; i < this->nvariables - 1; ++i)
	if (fd_var_single(VAR(this, i), &value))
	  {
	    if (value == k)
	      // if there are more than c variables set to k, fail
	      if (++set > c)
		return FD_NOSOLUTION;
	  }
	else if (_fd_var_contains_val(VAR(this, i), k))
	  possible++;

      // see if it still possible to satisfy the constraint
      if (set + possible < c)
	return FD_NOSOLUTION;

      if (set + possible == c)
	{
	  for (i = 0; possible > 0; ++i)
	    if (!fd_var_single(VAR(this, i), NULL) &&
		_fd_var_contains_val(VAR(this, i), k))
	      {
		_fd_var_set_value(VAR(this, i), k);

		possible--;

		_fd_revise_connected(this, VAR(this, i));
	      }

	  fd__constraint_set_entailed(this);

	  return FD_OK;
	}

      if (set == c)
	{
	  for (i = 0;  possible > 0; ++i)
	    if (!fd_var_single(VAR(this, i), NULL) &&
		_fd_var_del_val(k, VAR(this, i)))
	      {
		possible--;

		_fd_revise_connected(this, VAR(this, i));
	      }

	  fd__constraint_set_entailed(this);

	  return FD_OK;
	}
    }
  else // !fd_var_single(Y)
    {
      int cmin, cmax;
      int changed = 0;

      cmax = _fd_var_max(VAR(this, this->nvariables - 1));

      k = this->constants[0];

      set = possible = 0;

      // count the variables that are set to k and those which contain k
      // in their domain
      for (i = 0; i < this->nvariables - 1; ++i)
	if (fd_var_single(VAR(this, i), &value))
	  {
	    if (value == k)
	      // if there are more than d-max(Y) variables set to k, fail
	      if (++set > cmax)
		return FD_NOSOLUTION;
	  }
	else if (_fd_var_contains_val(VAR(this, i), k))
	  possible++;

      cmin = _fd_var_min(VAR(this, this->nvariables - 1));

      // if it isn't possible to set d-min(Y) variables to k, fail
      if (set + possible < cmin)
	return FD_NOSOLUTION;

      if (set + possible == cmin)
	{
	  for (i = 0; possible > 0; ++i)
	    if (!fd_var_single(VAR(this, i), NULL) &&
		_fd_var_contains_val(VAR(this, i), k))
	      {
		_fd_var_set_value(VAR(this, i), k);

		possible--;

		_fd_revise_connected(this, VAR(this, i));
	      }

	  _fd_var_set_value(VAR(this, this->nvariables - 1), cmin);
	  _fd_revise_connected(this, VAR(this, this->nvariables - 1));

	  fd__constraint_set_entailed(this);

	  return FD_OK;
	}

      if (set == cmax)
	{
	  for (i = 0;  possible > 0; ++i)
	    if (!fd_var_single(VAR(this, i), NULL) &&
		_fd_var_del_val(k, VAR(this, i)))
	      {
		possible--;

		_fd_revise_connected(this, VAR(this, i));
	      }

	  _fd_var_set_value(VAR(this, this->nvariables - 1), cmax);
	  _fd_revise_connected(this, VAR(this, this->nvariables - 1));

	  fd__constraint_set_entailed(this);

	  return FD_OK;
	}

      if (set > cmin)
	changed = _fd_var_del_lt(set, VAR(this, this->nvariables - 1));

      if (set + possible < cmax)
	changed = _fd_var_del_gt(set + possible, VAR(this, this->nvariables - 1));

      if (changed)
	  _fd_revise_connected(this, VAR(this, this->nvariables - 1));
    }

  // the constraint can still be satisfied: set < c && set + possible > c
  return FD_OK;
}

static int fd_exactly_var_propagate2(fd_constraint this, fd_int culprit)
{
  // only revise if culprit's domain is a singleton
  if (!fd_var_single(culprit, NULL))
    return FD_OK;

  return fd_exactly_var_filter(this);
}

fd_constraint fd_exactly_var(fd_int *variables, int nvariables, fd_int card, int k)
{
  fd_constraint c = _fd_constraint_new(nvariables + 1, 1);
  int i;

  if (c)
    {
      for (i = 0; i < nvariables; ++i)
	c->variables[i] = FD_INT2C_VAR(variables[i]);
      c->variables[nvariables] = FD_INT2C_VAR(card);
      c->constants[0] = k;
#ifdef CONSTRAINT_CLASS
      c->kind = FD_CONSTR_EXACTLY_VAR;
#else /* CONSTRAINT_CLASS */
      c->propagator2 = fd_exactly_var_propagate2;
#endif /* CONSTRAINT_CLASS */

      for (i = 0; i <= nvariables; ++i)
	_fd_var_add_constraint(VAR(c, i), c);

      _fd_add_constraint(c);
    }

  return c;
}