/*
 * cl_aux_functions.c
 *
 *  Created on: 09/09/2019
 *      Author: Pedro
 */

#ifndef __OPENCL_VERSION__
#include <stdbool.h>
#include <limits.h>
#include <sys/types.h>
#include "cl_aux_functions.h"
#include "../utils/cl_syntax.h"
#endif

#if CUDA_VERSION
#include "../utils/cu_syntax.h"
#endif

#include "../config.h"
#include "../domains.h"
#include "cl_constraints.h"
#include "cl_variables.h"
#include "cl_ttl.h"

#if CL_D_TYPE == CL_BITMAP
#include "cl_bitmaps.h"
#elif CL_D_TYPE == CL_INTERVAL
#include  "cl_intervals.h"
#endif

/*
 * Adds a variable to the vector of variables to propagate
 * vs_id_to_prop_ - circular vector with the ids of the variables to propagate
 * vs_prop_ - vector with all CSP variables
 * v_id_to_prop - id of the variable to propagate
 */
CUDA_FUNC void v_add_to_prop(CL_MEMORY unsigned short *vs_id_to_prop_, CL_MEMORY VARS_PROP *vs_prop_, int v_id_to_prop) {

	// if that variable is not already set for propagation
	if (vs_prop_[v_id_to_prop].to_prop == 0) {

		// add that variable id to the vector of variables to propagate
		vs_id_to_prop_[vs_id_to_prop_[1]] = convert_ushort (v_id_to_prop);

		if (vs_id_to_prop_[1] < CL_N_VS + 2) {
			vs_id_to_prop_[1] = convert_ushort (vs_id_to_prop_[1] + 1);
		} else {
			vs_id_to_prop_[1] = 2;
		}

		// mark that variable as added to vs_id_to_prop_ vector
		vs_prop_[v_id_to_prop].to_prop = 1;
	}

#if CL_CHECK_ERRORS
	int i;
	if (vs_id_to_prop_[0] <= vs_id_to_prop_[1]) {
		for (i = vs_id_to_prop_[0]; i < vs_id_to_prop_[1]; i++) {
			if (vs_id_to_prop_[i] == v_id_to_prop) {
				break;
			}
		}
		if (vs_id_to_prop_[i] != v_id_to_prop) {
			printf((__constant char *)"\n###error 31\n");
		}

	} else {
		for (i = vs_id_to_prop_[0]; i < CL_N_VS + 2; i++) {
			if (vs_id_to_prop_[i] == v_id_to_prop) {
				break;
			}
		}
		if (vs_id_to_prop_[i] != v_id_to_prop) {
			for (i = 2; i < vs_id_to_prop_[1]; i++) {
				if (vs_id_to_prop_[i] == v_id_to_prop) {
					break;
				}
			}
		}
		if (vs_id_to_prop_[i] != v_id_to_prop) {
			printf((__constant char *)"\n###error 32\n");
		}
	}
#endif

}

/*
 * Place the ID of the next variable to propagate in prop_v_id
 * vs_id_to_prop_ - circular vector with the ids of the variables to propagate
 * vs_prop_ - vector with all CSP variables
 * prop_v_id - ID of the next variable to propagate
 */
CUDA_FUNC void v_get_id_to_prop(CL_MEMORY unsigned short *vs_id_to_prop_, CL_MEMORY VARS_PROP *vs_prop_, unsigned int *prop_v_id TTL_CTR) {
	int v_idx;

	// If variables to propagate vector is empty
	if (vs_id_to_prop_[0] == vs_id_to_prop_[1]) {
		// Restart the first and next index on variables to propagate vector
		vs_id_to_prop_[0] = 2;
		vs_id_to_prop_[1] = 2;

		*prop_v_id = CL_N_VS;

#if CL_CHECK_ERRORS
		int i;
		for (i = 0; i < CL_N_VS; i++) {
			CHECK_TTL(ttl_ctr, 153)

					if (vs_prop_[i].to_prop == 1) {
						printf((__constant char *)"\n###error 33\n");
					}
		}
#endif

	} else {
		v_idx = convert_int (vs_id_to_prop_[vs_id_to_prop_[0]]);

		// mark that variable as not added to vs_id_to_prop_ vector
		vs_prop_[vs_id_to_prop_[vs_id_to_prop_[0]]].to_prop = 0;

		if (vs_id_to_prop_[0] < CL_N_VS + 2) {
			vs_id_to_prop_[0] = convert_ushort (vs_id_to_prop_[0] + 1);
		} else {
			vs_id_to_prop_[0] = 2;
		}

		*prop_v_id = convert_ushort (v_idx);
	}
CHECK_TTL(ttl_ctr, 232)
}

#if CL_LABEL_M == CL_ANTI_FIRST_FAIL || (CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1)
/*
 * Place the ID of the next variable to label in prop_v_id. Selecting it by the one not labeled yet and with more values on its domain, or CL_N_VS if none
 * vs_prop_ - vector with all CSP variables
 * vs - vector with all CSP variables common to all work-items
 * prop_v_id - ID of the next variable to label
 */
#if CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1
CUDA_FUNC void v_get_id_to_label_anti_first_fail(CL_MEMORY VARS_PROP *vs_prop_, CL_VS_MEM VARS *vs, unsigned int *prop_v_id TTL_CTR)
#else
CUDA_FUNC void v_get_id_to_label(CL_MEMORY VARS_PROP* vs_prop_, CL_VS_MEM VARS* vs, unsigned int* prop_v_id TTL_CTR)
#endif
{
int vals_cnt = 0;
int n_vals;
int v_idx = CL_N_VS;
int i;

for (i = 0; i < CL_N_VS; i++) {
	CHECK_TTL(ttl_ctr, 3)

#if CL_CHECK_ERRORS
	bool empty;
	cl_d_is_empty_m(&empty, &vs_prop_->prop_d TTL_CTR_V);
	if (empty || vs_prop_[i].n_vals == 0 || vs_prop_[i].n_vals > vs_prop_[i].max + 1 || vs_prop_[i].min > vs_prop_[i].max || vs_prop_[i].max > CL_D_MAX) {
		printf((__constant char *)"\n###error 77\n");
	}
#endif

	n_vals = V_N_VALS(vs_prop_[i]);

#if CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1
	if (vs[i].to_label && vs[i].label_h == CL_ANTI_FIRST_FAIL && n_vals > 1 && n_vals > vals_cnt)
#else
			if (vs[i].to_label && n_vals > 1 && n_vals > vals_cnt)
#endif
			{
		vals_cnt = n_vals;

		v_idx = i;

		// The minimum values of a variable to label will be two, so stop searching
		if (n_vals == CL_D_MAX + 1) {
			i = CL_N_VS;
		}
	}
}

*prop_v_id = convert_ushort (v_idx);
}
#endif

#if CL_LABEL_M == CL_FIRST_FAIL || (CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1)
/*
 * Place the ID of the next variable to label in prop_v_id. Selecting it by selecting the one not labeled yet and with less values on its domain,
 * or CL_N_VS if none
 * vs_prop_ - vector with all CSP variables
 * vs - vector with all CSP variables common to all work-items
 * prop_v_id - ID of the next variable to label
 */
#if CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1
CUDA_FUNC void v_get_id_to_label_first_fail(CL_MEMORY VARS_PROP *vs_prop_, CL_VS_MEM VARS *vs, unsigned int *prop_v_id TTL_CTR)
#else
CUDA_FUNC void v_get_id_to_label(CL_MEMORY VARS_PROP* vs_prop_, CL_VS_MEM VARS* vs, unsigned int* prop_v_id TTL_CTR)
#endif
{
int vals_cnt = 0xFFFF;
int n_vals;
int v_idx = CL_N_VS;
int i;

for (i = 0; i < CL_N_VS; i++) {
	CHECK_TTL(ttl_ctr, 3)

#if CL_CHECK_ERRORS
	bool empty;
	cl_d_is_empty_m(&empty, &vs_prop_->prop_d TTL_CTR_V);
	if (empty || vs_prop_[i].n_vals == 0 || vs_prop_[i].n_vals > vs_prop_[i].max + 1 || vs_prop_[i].min > vs_prop_[i].max || vs_prop_[i].max > CL_D_MAX) {
		printf((__constant char *)"\n###error 34\n");
	}
#endif

	n_vals = V_N_VALS(vs_prop_[i]);
#if CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1
	if (vs[i].to_label && vs[i].label_h == CL_FIRST_FAIL && n_vals > 1 && n_vals < vals_cnt)
#else
			if (vs[i].to_label && n_vals > 1 && n_vals < vals_cnt)
#endif
			{
		vals_cnt = n_vals;

		v_idx = i;

		// The minimum values of a variable to label will be two, so stop searching
		if (n_vals == 2) {
			i = CL_N_VS;
		}
	}
}

*prop_v_id = convert_ushort (v_idx);
}
#endif

#if CL_LABEL_M == CL_INPUT_ORDER || (CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1)
/*
 * Place the ID of the next variable to label in prop_v_id. Selecting it by selecting the first one not labeled yet, or CL_N_VS if none
 * vs_prop_ - vector with all CSP variables
 * vs - vector with all CSP variables common to all work-+items
 * prop_v_id - ID of the next variable to label
 */
#if CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1
CUDA_FUNC void v_get_id_to_label_input_order(CL_MEMORY VARS_PROP *vs_prop_, CL_VS_MEM VARS *vs, unsigned int *prop_v_id TTL_CTR)
#else
CUDA_FUNC void v_get_id_to_label(CL_MEMORY VARS_PROP* vs_prop_, CL_VS_MEM VARS* vs, unsigned int* prop_v_id TTL_CTR)
#endif
{
int v_idx = CL_N_VS;
int i;

for (i = 0; i < CL_N_VS; i++) {
	CHECK_TTL(ttl_ctr, 29)

#if CL_CHECK_ERRORS
	bool empty;
	cl_d_is_empty_m(&empty, &vs_prop_->prop_d TTL_CTR_V);
	if (empty || vs_prop_[i].n_vals == 0 || vs_prop_[i].n_vals > vs_prop_[i].max + 1 || vs_prop_[i].min > vs_prop_[i].max || vs_prop_[i].max > CL_D_MAX) {
		printf((__constant char *)"\n###error 36\n");
	}
#endif

#if CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1
	if (vs[i].to_label && vs[i].label_h == CL_INPUT_ORDER && V_N_VALS(vs_prop_[i]) > 1)
#else
			if (vs[i].to_label && V_N_VALS(vs_prop_[i]) > 1)
#endif
			{
		v_idx = i;
		i = CL_N_VS;
	}
}

*prop_v_id = convert_ushort (v_idx);
}
#endif

#if CL_LABEL_M == CL_LARGEST || (CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1)
/*
 * Place the ID of the next variable to label in prop_v_id. Selecting it by selecting the one not labeled yet and with the biggest value on its domain,
 * or CL_N_VS if none
 * vs_prop_ - vector with all CSP variables
 * vs - vector with all CSP variables common to all work-items
 * prop_v_id - ID of the next variable to label
 */
#if CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1
CUDA_FUNC void v_get_id_to_label_largest(CL_MEMORY VARS_PROP *vs_prop_, CL_VS_MEM VARS *vs, unsigned int *prop_v_id TTL_CTR)
#else
CUDA_FUNC void v_get_id_to_label(CL_MEMORY VARS_PROP* vs_prop_, CL_VS_MEM VARS* vs, unsigned int* prop_v_id TTL_CTR)
#endif
{
int v_idx = CL_N_VS;
int max = 0;
int i;

for (i = 0; i < CL_N_VS; i++) {
	CHECK_TTL(ttl_ctr, 3)

#if CL_CHECK_ERRORS
	bool empty;
	cl_d_is_empty_m(&empty, &vs_prop_->prop_d TTL_CTR_V);
	if (empty || vs_prop_[i].n_vals == 0 || vs_prop_[i].n_vals > vs_prop_[i].max + 1 || vs_prop_[i].min > vs_prop_[i].max || vs_prop_[i].max > CL_D_MAX) {
		printf((__constant char *)"\n###error 77\n");
	}
#endif

#if CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1
	if (vs[i].to_label && vs[i].label_h == CL_LARGEST && V_N_VALS(vs_prop_[i]) > 1 && V_MAX(vs_prop_[i]) > max)
#else
			if (vs[i].to_label && V_N_VALS(vs_prop_[i]) > 1 && V_MAX(vs_prop_[i]) > max)
#endif
			{

		v_idx = i;
		max = V_MAX(vs_prop_[i]);

		// If the minimum value is CL_D_MAX + 1, stop searching
		if (max == CL_D_MAX) {
			i = CL_N_VS;
		}
	}
}

*prop_v_id = convert_ushort (v_idx);
}
#endif

#if CL_LABEL_M == CL_MAX_REGRET || (CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1)
/*
 * Place the ID of the next variable to label in prop_v_id. Selecting it  by selecting the one on vs_id_to_prop_ vector that has the largest
 * difference between the two smallest values, or CL_N_VS if none
 * vs_prop_ - vector with all CSP variables
 * vs - vector with all CSP variables common to all work-items
 * prop_v_id - ID of the next variable to label
 */
#if CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1
CUDA_FUNC void v_get_id_to_label_max_regret(CL_MEMORY VARS_PROP *vs_prop_, CL_VS_MEM VARS *vs, unsigned int *prop_v_id TTL_CTR)
#else
CUDA_FUNC void v_get_id_to_label(CL_MEMORY VARS_PROP* vs_prop_, CL_VS_MEM VARS* vs, unsigned int* prop_v_id TTL_CTR)
#endif
{
int diff_aux;
int diff = 0;
int v_idx = CL_N_VS;
int values[2];
int i;

for (i = 0; i < CL_N_VS; i++) {
	CHECK_TTL(ttl_ctr, 31)

#if CL_CHECK_ERRORS
	bool empty;
	cl_d_is_empty_m(&empty, &vs_prop_->prop_d TTL_CTR_V);
	if (empty || vs_prop_[i].n_vals == 0 || vs_prop_[i].n_vals > vs_prop_[i].max + 1 || vs_prop_[i].min > vs_prop_[i].max || vs_prop_[i].max > CL_D_MAX) {
		printf((__constant char *)"\n###error 40\n");
	}
#endif

#if CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1
	if (vs[i].to_label && vs[i].label_h == CL_MAX_REGRET && V_N_VALS(vs_prop_[i]) > 1)
#else
			if (vs[i].to_label && V_N_VALS(vs_prop_[i]) > 1)
#endif
			{

		cl_d_get_nth_vals_m5(&vs_prop_[i].prop_d, 1, 2, values TTL_CTR_V);
		diff_aux = values[1] - values[0];

		if (diff_aux > diff) {

			diff = diff_aux;
			v_idx = i;
		}
	}
}

*prop_v_id = convert_ushort (v_idx);
}
#endif

#if CL_LABEL_M == CL_MOST_CONSTRAINED || (CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1)
/*
 * Place the ID of the next variable to label in prop_v_id. Selecting it by selecting the one not labeled yet and with less values on its domain,
 * breaking ties by the higher number of constraints,
 * or CL_N_VS if none
 * vs_prop_ - vector with all CSP variables
 * vs - vector with all CSP variables common to all work-items
 * prop_v_id - ID of the next variable to label
 */
#if CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1
CUDA_FUNC void v_get_id_to_label_most_constrained(CL_MEMORY VARS_PROP *vs_prop_, CL_VS_MEM VARS *vs, unsigned int *prop_v_id TTL_CTR)
#else
CUDA_FUNC void v_get_id_to_label(CL_MEMORY VARS_PROP* vs_prop_, CL_VS_MEM VARS* vs, unsigned int* prop_v_id TTL_CTR)
#endif
{
int vals_cnt = 0xFFFF;
int n_vals;
int n_cs = 0;
int v_idx = CL_N_VS;
int i;

for (i = 0; i < CL_N_VS; i++) {
	CHECK_TTL(ttl_ctr, 3)

#if CL_CHECK_ERRORS
	bool empty;
	cl_d_is_empty_m(&empty, &vs_prop_->prop_d TTL_CTR_V);
	if (empty || vs_prop_[i].n_vals == 0 || vs_prop_[i].n_vals > vs_prop_[i].max + 1 || vs_prop_[i].min > vs_prop_[i].max || vs_prop_[i].max > CL_D_MAX) {
		printf((__constant char *)"\n###error 80\n");
	}
#endif

	n_vals = V_N_VALS(vs_prop_[i]);

#if CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1
	if (vs[i].to_label && vs[i].label_h == CL_MOST_CONSTRAINED && n_vals > 1 && ((n_vals < vals_cnt) || (n_vals == vals_cnt && n_cs < vs[i].n_cs)))
#else
			if (vs[i].to_label && n_vals > 1 && ((n_vals < vals_cnt) || (n_vals == vals_cnt && n_cs < vs[i].n_cs)))
#endif
			{

		vals_cnt = n_vals;
		n_cs = vs[i].n_cs;

		v_idx = i;
	}
}

*prop_v_id = convert_ushort (v_idx);
}
#endif

#if CL_LABEL_M == CL_OCCURRENCE || (CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1)
/*
 * Place the ID of the next variable to label in prop_v_id. Selecting it by selecting the one not labeled yet that is more constrained, or CL_N_VS if none
 * vs_prop_ - vector with all CSP variables local to this work-item
 * vs - vector with all CSP variables common to all work-items
 * prop_v_id - ID of the next variable to label
 */
#if CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1
CUDA_FUNC void v_get_id_to_label_occurrence(CL_MEMORY VARS_PROP *vs_prop_, CL_VS_MEM VARS *vs, unsigned int *prop_v_id TTL_CTR)
#else
CUDA_FUNC void v_get_id_to_label(CL_MEMORY VARS_PROP* vs_prop_, CL_VS_MEM VARS* vs, unsigned int* prop_v_id TTL_CTR)
#endif
{
int max_cs_cnt = 0;
int v_idx = CL_N_VS;
int i;

for (i = 0; i < CL_N_VS; i++) {
	CHECK_TTL(ttl_ctr, 30)

#if CL_CHECK_ERRORS
	bool empty;
	cl_d_is_empty_m(&empty, &vs_prop_->prop_d TTL_CTR_V);
	if (empty || vs_prop_[i].n_vals == 0 || vs_prop_[i].n_vals > vs_prop_[i].max + 1 || vs_prop_[i].min > vs_prop_[i].max || vs_prop_[i].max > CL_D_MAX) {
		printf((__constant char *)"\n###error 38\n");
	}
#endif

#if CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1
	if (vs[i].to_label && vs[i].label_h == CL_OCCURRENCE && vs[i].n_cs > max_cs_cnt && V_N_VALS(vs_prop_[i]) > 1)
#else
			if (vs[i].to_label && vs[i].n_cs > max_cs_cnt && V_N_VALS(vs_prop_[i]) > 1)
#endif
			{
		max_cs_cnt = vs[i].n_cs;

		v_idx = i;
	}
}

*prop_v_id = convert_ushort (v_idx);
}
#endif

#if CL_LABEL_M == CL_SMALLEST || (CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1)
/*
 * Place the ID of the next variable to label in prop_v_id. Selecting it by selecting the one not labeled yet and with the smallest value on its domain,
 * or CL_N_VS if none
 * vs_prop_ - vector with all CSP variables
 * vs - vector with all CSP variables common to all work-items
 * prop_v_id - ID of the next variable to label
 */
#if CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1
CUDA_FUNC void v_get_id_to_label_smallest(CL_MEMORY VARS_PROP *vs_prop_, CL_VS_MEM VARS *vs, unsigned int *prop_v_id TTL_CTR)
#else
CUDA_FUNC void v_get_id_to_label(CL_MEMORY VARS_PROP* vs_prop_, CL_VS_MEM VARS* vs, unsigned int* prop_v_id TTL_CTR)
#endif
{
int v_idx = CL_N_VS;
int min = CL_D_MAX;
int i;

for (i = 0; i < CL_N_VS; i++) {
	CHECK_TTL(ttl_ctr, 3)

#if CL_CHECK_ERRORS
	bool empty;
	cl_d_is_empty_m(&empty, &vs_prop_->prop_d TTL_CTR_V);
	if (empty || vs_prop_[i].n_vals == 0 || vs_prop_[i].n_vals > vs_prop_[i].max + 1 || vs_prop_[i].min > vs_prop_[i].max || vs_prop_[i].max > CL_D_MAX) {
		printf((__constant char *)"\n###error 42\n");
	}
#endif

#if CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1
	if (vs[i].to_label && vs[i].label_h == CL_SMALLEST && V_N_VALS(vs_prop_[i]) > 1 && V_MIN(vs_prop_[i]) < min)
#else
			if (vs[i].to_label && V_N_VALS(vs_prop_[i]) > 1 && V_MIN(vs_prop_[i]) < min)
#endif
			{

		v_idx = i;
		min = V_MIN(vs_prop_[i]);

		// If the minimum value is CL_D_MIN, stop searching
		if (min == CL_D_MIN) {
			i = CL_N_VS;
		}
	}
}

*prop_v_id = convert_ushort (v_idx);
}
#endif

#if CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1
/*
 * Use the defined heuristic to select the next variable to label when using FlatZinc seq_search
 * vs_prop_ - vector with all CSP variables
 * vs - vector with all CSP variables common to all work-items
 * prop_v_id - ID of the next variable to label
 * last_label_h_idx - index of label_hs where is the the ENUM of the heuristic for labeling that was used the last time
 * label_hs - array with all the labeling heuristics that must be used by input order
 */
CUDA_FUNC void v_get_id_to_label(CL_MEMORY VARS_PROP *vs_prop_, CL_VS_MEM VARS *vs, unsigned int *prop_v_id TTL_CTR, int *last_label_h_idx,
	__global int *label_hs TTL_CTR) {

*prop_v_id = CL_N_VS;
int i, j;

for (i = (*last_label_h_idx); i < CL_FZN_SEQ_N_LABELS; i++) {
	CHECK_TTL(ttl_ctr, 293)

	for (j = 0; j < CL_N_VS; j++) {
		CHECK_TTL(ttl_ctr, 294)

		if (vs[j].to_label && V_N_VALS(vs_prop_[j]) > 1 && vs[j].label_h == label_hs[*last_label_h_idx]) {
			break;
		}
	}

	if (j < CL_N_VS) {
		switch (vs[j].label_h) {
		case CL_ANTI_FIRST_FAIL:
			v_get_id_to_label_anti_first_fail(vs_prop_, vs, prop_v_id TTL_CTR_E);
			break;
		case CL_FIRST_FAIL:
			v_get_id_to_label_first_fail(vs_prop_, vs, prop_v_id TTL_CTR_E);
			break;
		case CL_INPUT_ORDER:
			v_get_id_to_label_input_order(vs_prop_, vs, prop_v_id TTL_CTR_E);
			break;
		case CL_LARGEST:
			v_get_id_to_label_largest(vs_prop_, vs, prop_v_id TTL_CTR_E);
			break;
		case CL_MAX_REGRET:
			v_get_id_to_label_max_regret(vs_prop_, vs, prop_v_id TTL_CTR_E);
			break;
		case CL_MOST_CONSTRAINED:
			v_get_id_to_label_most_constrained(vs_prop_, vs, prop_v_id TTL_CTR_E);
			break;
		case CL_OCCURRENCE:
			v_get_id_to_label_occurrence(vs_prop_, vs, prop_v_id TTL_CTR_E);
			break;
		case CL_SMALLEST:
			v_get_id_to_label_smallest(vs_prop_, vs, prop_v_id TTL_CTR_E);
			break;
		default:
#if CL_CHECK_ERRORS
				printf((__constant char *)"\n###error 82\n");
#endif
			break;
		}
		break;

	} else {
		(*last_label_h_idx)++;
	}
}
}
#endif

#if CL_ASSIGN_M == CL_INDOMAIN_INTERVAL || (CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1)
/*
 * Select the first contiguous interval or, if none, select half of the domain
 * v - variable to be assigned
 * hist - place on backtracking history where the remaining values of the variable should be stored
 * hist_labeleds_n_vals - place where the number of values remaining on the assigned variable should be stored
 */
#if CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1
CUDA_FUNC void v_assign_interval(CL_MEMORY VARS_PROP *v, __global DOMAIN_ *hist, __global int *hist_labeleds_n_vals)
#else
CUDA_FUNC void v_assign(CL_MEMORY VARS_PROP* v, __global DOMAIN_* hist, __global int* hist_labeleds_n_vals)
#endif
{

#if CL_CHECK_ERRORS
	bool empty;
	cl_d_is_empty_m(&empty, &v->prop_d TTL_CTR_V);
	if (empty || v->n_vals == 0 || v->n_vals > v->max + 1 || v->min > v->max || v->max > CL_D_MAX) {
		printf((__constant char *)"\n###error 74\n");
	}
#endif

int n_vals = V_N_VALS(*v);

// If the labeled variable had more than one value on its domain remove the labeled value from its backtracking domain
if (n_vals > 1) {
	int max = V_MAX(*v);
	int min = V_MIN(*v);

	// one interval from min to max
	if (n_vals == max - min + 1) {

		int split_val = (V_MAX(*v) - min) / 2 + min;
		cl_v_del_gt_no_tests_m(v, split_val);
		cl_d_del_le_no_tests_g(hist, split_val);

		*hist_labeleds_n_vals = n_vals - V_N_VALS(*v);

	} else {
		int i;
		int contiguous = 0;
		int values[CL_D_MAX + 1];

		cl_d_get_nth_vals_m4(hist, 1, n_vals, values TTL_CTR_V);

		for (i = 1; i < n_vals; i++) {
			if (values[i] == values[i - 1]) {
				contiguous++;

			} else {
				if (contiguous > 0) {
					break;
				}
			}
		}

		// no interval
		if (contiguous == 0) {
			int split_val = (V_MAX(*v) - min) / 2 + min;
			cl_v_del_gt_no_tests_m(v, split_val);
			cl_d_del_le_no_tests_g(hist, split_val);

			*hist_labeleds_n_vals = n_vals - V_N_VALS(*v);

			// use first interval
		} else {

			bool changed;
			int j;

			cl_v_del_lt_m(&changed, v, values[i - 1 - contiguous]);
			cl_v_del_gt_m(&changed, v, values[i - 1]);

			for (j = i - 1 - contiguous; j < i; j++) {
				cl_d_del_val_no_tests_g(hist, values[j]);
			}

			*hist_labeleds_n_vals = n_vals - V_N_VALS(*v);
		}
	}

} else {
	cl_d_clear_g(hist);
	(*hist_labeleds_n_vals) = 0;
}
}
#endif

#if CL_ASSIGN_M == CL_INDOMAIN_MAX || (CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1)
/*
 * Assign the maximum value
 * v - variable to be assigned
 * hist - place on backtracking history where the remaining values of the variable should be stored
 * hist_labeleds_n_vals - place where tje number of values remaining on the assigned variable should be stored
 */
#if CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1
CUDA_FUNC void v_assign_max(CL_MEMORY VARS_PROP *v, __global DOMAIN_ *hist, __global int *hist_labeleds_n_vals)
#else
CUDA_FUNC void v_assign(CL_MEMORY VARS_PROP* v, __global DOMAIN_* hist, __global int* hist_labeleds_n_vals)
#endif
{

#if CL_CHECK_ERRORS
	bool empty;
	cl_d_is_empty_m(&empty, &v->prop_d TTL_CTR_V);
	if (empty || v->n_vals == 0 || v->n_vals > v->max + 1 || v->min > v->max || v->max > CL_D_MAX) {
		printf((__constant char *)"\n###error 45\n");
	}
#endif

(*hist_labeleds_n_vals) = V_N_VALS(*v) - 1;

// If the labeled variable had more than one value on its domain remove the labeled value from its backtracking domain
if ((*hist_labeleds_n_vals) > 0) {
	int max = V_MAX(*v);
	bool changed;
	cl_v_del_all_except_val_m(&changed, v, max TTL_CTR_V);
	cl_d_del_val_no_tests_g(hist, max);

} else {
	cl_d_clear_g(hist);
}
}
#endif

#if CL_ASSIGN_M == CL_INDOMAIN_MEDIAN || (CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1)
/*
 * Assign the median value of the domain values
 * v - variable to be assigned
 * hist - place on backtracking history where the remaining values of the variable should be stored
 * hist_labeleds_n_vals - place where tje number of values remaining on the assigned variable should be stored
 */
#if CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1
CUDA_FUNC void v_assign_median(CL_MEMORY VARS_PROP *v, __global DOMAIN_ *hist, __global int *hist_labeleds_n_vals)
#else
CUDA_FUNC void v_assign(CL_MEMORY VARS_PROP* v, __global DOMAIN_* hist, __global int* hist_labeleds_n_vals)
#endif
{

#if CL_CHECK_ERRORS
	bool empty;
	cl_d_is_empty_m(&empty, &v->prop_d TTL_CTR_V);
	if (empty || v->n_vals == 0 || v->n_vals > v->max + 1 || v->min > v->max || v->max > CL_D_MAX) {
		printf((__constant char *)"\n###error 71\n");
	}
#endif

int n_vals = V_N_VALS(*v);
(*hist_labeleds_n_vals) = n_vals - 1;

// If the labeled variable had more than one value on its domain remove the labeled value from its backtracking domain
if (n_vals > 1) {
	int median = n_vals / 2;
	int values[CL_D_MAX + 1];

	cl_d_get_nth_vals_m4(hist, 1, n_vals, values TTL_CTR_V);

	bool changed;
	cl_v_del_all_except_val_m(&changed, v, values[median] TTL_CTR_V);
	cl_d_del_val_no_tests_g(hist, values[median]);

} else {
	cl_d_clear_g(hist);
}
}
#endif

#if CL_ASSIGN_M == CL_INDOMAIN_MIDDLE || (CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1)
/*
 * Assign the value closest to the mean of the bounds
 * v - variable to be assigned
 * hist - place on backtracking history where the remaining values of the variable should be stored
 * hist_labeleds_n_vals - place where tje number of values remaining on the assigned variable should be stored
 */
#if CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1
CUDA_FUNC void v_assign_middle(CL_MEMORY VARS_PROP *v, __global DOMAIN_ *hist, __global int *hist_labeleds_n_vals)
#else
CUDA_FUNC void v_assign(CL_MEMORY VARS_PROP* v, __global DOMAIN_* hist, __global int* hist_labeleds_n_vals)
#endif
{

#if CL_CHECK_ERRORS
	bool empty;
	cl_d_is_empty_m(&empty, &v->prop_d TTL_CTR_V);
	if (empty || v->n_vals == 0 || v->n_vals > v->max + 1 || v->min > v->max || v->max > CL_D_MAX) {
		printf((__constant char *)"\n###error 72\n");
	}
#endif

int n_vals = V_N_VALS(*v);
(*hist_labeleds_n_vals) = n_vals - 1;

// If the labeled variable had more than one value on its domain remove the labeled value from its backtracking domain
if (n_vals > 1) {
	int mean = (V_MAX(*v) + V_MIN(*v)) / 2;
	int values[CL_D_MAX + 1];
	int lower_value, higher_value;
	int i;

	cl_d_get_nth_vals_m4(hist, 1, n_vals, values TTL_CTR_V);

	i = 0;
	while (values[i] < mean) {
		i++;
	}
	if (values[i] != mean) {
		lower_value = values[i];
		higher_value = values[i];

		if (i > 0) {
			lower_value = values[i - 1];
		}
		if (i < n_vals - 1) {
			higher_value = values[i + 1];
		}
		if (mean - lower_value < higher_value - mean) {
			mean = lower_value;

		} else {
			mean = higher_value;
		}
	}

	bool changed;
	cl_v_del_all_except_val_m(&changed, v, mean TTL_CTR_V);
	cl_d_del_val_no_tests_g(hist, mean);

} else {
	cl_d_clear_g(hist);
}
}
#endif

#if CL_ASSIGN_M == CL_INDOMAIN_MIN || (CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1)
/*
 * Assign the minimum value
 * v - variable to be assigned
 * hist - place on backtracking history where the remaining values of the variable should be stored
 * hist_labeleds_n_vals - place where the number of values remaining on the assigned variable should be stored
 */
#if CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1
CUDA_FUNC void v_assign_min(CL_MEMORY VARS_PROP *v, __global DOMAIN_ *hist, __global int *hist_labeleds_n_vals)
#else
CUDA_FUNC void v_assign(CL_MEMORY VARS_PROP* v, __global DOMAIN_* hist, __global int* hist_labeleds_n_vals)
#endif
{

#if CL_CHECK_ERRORS
	bool empty;
	cl_d_is_empty_m(&empty, &v->prop_d TTL_CTR_V);
	if (empty || v->n_vals == 0 || v->n_vals > v->max + 1 || v->min > v->max || v->max > CL_D_MAX) {
		printf((__constant char *)"\n###error 44\n");
	}
#endif

(*hist_labeleds_n_vals) = V_N_VALS(*v) - 1;

// If the labeled variable has more than one value on its domain remove the labeled value from its backtracking domain
if ((*hist_labeleds_n_vals) > 0) {

	int min = V_MIN(*v);
	bool changed;
	cl_v_del_all_except_val_m(&changed, v, min TTL_CTR_V);
	cl_d_del_val_no_tests_g(hist, min);

} else {
	cl_d_clear_g(hist TTL_CTR_V);
}
}
#endif

#if CL_ASSIGN_M == CL_INDOMAIN_REVERSE_SPLIT || (CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1)
/*
 * Split the domain in half between the minimum and the maximum, and keeps the second half
 * v - variable to be assigned
 * hist - place on backtracking history where the remaining values of the variable should be stored
 * hist_labeleds_n_vals - place where the number of values remaining on the assigned variable should be stored
 */
#if CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1
CUDA_FUNC void v_assign_reverse_split(CL_MEMORY VARS_PROP *v, __global DOMAIN_ *hist, __global int *hist_labeleds_n_vals)
#else
CUDA_FUNC void v_assign(CL_MEMORY VARS_PROP* v, __global DOMAIN_* hist, __global int* hist_labeleds_n_vals)
#endif
{

#if CL_CHECK_ERRORS
	bool empty;
	cl_d_is_empty_m(&empty, &v->prop_d TTL_CTR_V);
	if (empty || v->n_vals == 0 || v->n_vals > v->max + 1 || v->min > v->max || v->max > CL_D_MAX) {
		printf((__constant char *)"\n###error 73\n");
	}
#endif

int n_vals = V_N_VALS(*v);

if (n_vals > 1) {
	int min = V_MIN(*v);

	int split_val = (V_MAX(*v) - min) / 2 + min;
	cl_v_del_lt_no_tests_m(v, split_val + 1);
	cl_d_del_gt_no_tests_g(hist, split_val);

	*hist_labeleds_n_vals = n_vals - V_N_VALS(*v);
} else {
	*hist_labeleds_n_vals = 0;
	cl_d_clear_g(hist);
}
}
#endif

#if CL_ASSIGN_M == CL_INDOMAIN_SPLIT || (CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1)
/*
 * Split the domain in half between the minimum and the maximum, and keeps the first half
 * v - variable to be assigned
 * hist - place on backtracking history where the remaining values of the variable should be stored
 * hist_labeleds_n_vals - place where tje number of values remaining on the assigned variable should be stored
 */
#if CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1
CUDA_FUNC void v_assign_split(CL_MEMORY VARS_PROP *v, __global DOMAIN_ *hist, __global int *hist_labeleds_n_vals)
#else
CUDA_FUNC void v_assign(CL_MEMORY VARS_PROP* v, __global DOMAIN_* hist, __global int* hist_labeleds_n_vals)
#endif
{

#if CL_CHECK_ERRORS
	bool empty;
	cl_d_is_empty_m(&empty, &v->prop_d TTL_CTR_V);
	if (empty || v->n_vals == 0 || v->n_vals > v->max + 1 || v->min > v->max || v->max > CL_D_MAX) {
		printf((__constant char *)"\n###error 46\n");
	}
#endif

int n_vals = V_N_VALS(*v);

if (n_vals > 1) {
	int min = V_MIN(*v);

	int split_val = (V_MAX(*v) - min) / 2 + min;
	cl_v_del_gt_no_tests_m(v, split_val);
	cl_d_del_le_no_tests_g(hist, split_val);

	*hist_labeleds_n_vals = n_vals - V_N_VALS(*v);
} else {
	*hist_labeleds_n_vals = 0;
	cl_d_clear_g(hist);
}
}
#endif

#if CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1
/*
 * Use the defined heuristic to assign the variable when using FlatZinc seq_search
 * v - variable to be assigned
 * hist - place on backtracking history where the remaining values of the variable should be stored
 * hist_labeleds_n_vals - place where tje number of values remaining on the assigned variable should be stored
 * v_g - constant structure of the variable to be assigned
 */
CUDA_FUNC void v_assign(CL_MEMORY VARS_PROP *v, __global DOMAIN_ *hist, __global int *hist_labeleds_n_vals, CL_VS_MEM VARS *v_g) {

switch (v_g->assign_h) {
case CL_INDOMAIN_INTERVAL:
	v_assign_interval(v, hist, hist_labeleds_n_vals);
	break;
case CL_INDOMAIN_MAX:
	v_assign_max(v, hist, hist_labeleds_n_vals);
	break;
case CL_INDOMAIN_MEDIAN:
	v_assign_median(v, hist, hist_labeleds_n_vals);
	break;
case CL_INDOMAIN_MIDDLE:
	v_assign_middle(v, hist, hist_labeleds_n_vals);
	break;
case CL_INDOMAIN_MIN:
	v_assign_min(v, hist, hist_labeleds_n_vals);
	break;
case CL_INDOMAIN_REVERSE_SPLIT:
	v_assign_reverse_split(v, hist, hist_labeleds_n_vals);
	break;
case CL_INDOMAIN_SPLIT:
	v_assign_split(v, hist, hist_labeleds_n_vals);
	break;
default:
#if CL_CHECK_ERRORS
		printf((__constant char *)"\n###error 84\n");
#endif
	break;
}
}
#endif

#if CL_WORK == CL_OPT

/*
 * Update the domain of the variable to optimize according to the global value to optimize on the received backtracking store. Global memory
 * Return 1 if domain changed and 0 if not
 * hist - backtracking data
 * val_to_opt - global value to optimize
 */
CUDA_FUNC void upd_opt_var_hist_g(__global DOMAIN_ *hist, __global unsigned int *val_to_opt TTL_CTR) {

if (*val_to_opt > CL_D_MAX) {
	cl_d_clear_g(hist TTL_CTR_V);
	return;
}

#if CL_CHECK_ERRORS
bool empty;
cl_d_is_empty_g(&empty, hist TTL_CTR_V);
if (empty || *val_to_opt > CL_D_MAX) {
	printf((__constant char *)"\n###error 47\n");
}
#endif

bool changed;
int val_to_opt_aux = convert_int (*val_to_opt);

#if CL_OPT_M == CL_DECREASE
cl_d_del_gt_g(&changed, hist, val_to_opt_aux TTL_CTR_V);
#else
	cl_d_del_lt_g(&changed, hist, val_to_opt_aux TTL_CTR_V);
#endif
}
#endif

#if CL_N_SHARED_SS > 0
/*
 * Pick a new store from the shared stores and prepares all the structures to begin its exploration.
 * prop_v_id will get CL_N_VS if no store is available.
 * shared_ss - All the shared stores
 * shared_ss_flags - flags for each shared store state
 * vs_id_to_prop_ - List with the ID of the variables to propagate
 * vs_prop_ - variables on the current state
 * hist - backtracking history
 * hist_tree_level - level of the backtracking
 * hist_labeleds_id - list of the ID of the variables that were labeled for each backtracking history level
 * hist_labeleds_n_vals - number of values that remain on the variables that were labeled for each backtracking history level
 * prop_v_id - ID of the first variable that must be propagated
 */
CUDA_FUNC void get_shared_store( __global DOMAIN_* shared_ss, __global int* shared_ss_flags, CL_MEMORY unsigned short* vs_id_to_prop_,
		CL_MEMORY VARS_PROP* vs_prop_, __global DOMAIN_* hist, int* hist_tree_level, __global int* hist_labeleds_id,
		__global int* hist_labeleds_n_vals, unsigned int* prop_v_id TTL_CTR) {

	int ss_to_get;

	// flags for signaling the state of each work-sharing store
	// 0 - next shared SS to be picked
	// 1 - next shared SS to be filled
	// 2...number of SS already filled
	// 3..3+CL_N_SHARED_SS - V_ID that was labeled to generate this SS
	if ((ss_to_get = atomic_inc(&shared_ss_flags[0])) < atomic_add(&shared_ss_flags[2], 0)) {

		__global DOMAIN_* new_ss;
		*prop_v_id = convert_uint(shared_ss_flags[3 + ss_to_get]);
		int i;

		// copy the new store
		new_ss = &shared_ss[ss_to_get * CL_N_VS];
		for (i = 0; i < CL_N_VS; i++) {
			CHECK_TTL(ttl_ctr, 35)

					cl_d_copy_mg(&vs_prop_[i].prop_d, &new_ss[i] TTL_CTR_V);
			cl_d_copy_g(&hist[i], &new_ss[i] TTL_CTR_V);

			vs_prop_[i].to_prop = 0;
			cl_v_calc_min_val_m(&vs_prop_[i] TTL_CTR_V);
			cl_v_calc_max_val_m(&vs_prop_[i] TTL_CTR_V);
			cl_v_cnt_vals_m(&vs_prop_[i] TTL_CTR_V);
		}

		cl_d_clear_g(&hist[*prop_v_id] TTL_CTR_V);

		// reset the indexes of the array that contains the IDs of the variables to propagate
		vs_id_to_prop_[0] = 2;
		vs_id_to_prop_[1] = 2;

		(*hist_tree_level) = 1;
		hist_labeleds_id[0] = convert_int(*prop_v_id);
		(*hist_labeleds_n_vals) = 0;
	}
}

/*
 * Set a new store on the shared stores
 * shared_ss - All the shared stores
 * shared_ss_flags - flags for each shared store state
 * vs_prop_ - variables on the current state
 * v_id - ID of the variable whose domain is to be pruned to create a new shared store
 * hist - backtracking history
 * hist_labeleds_n_vals - number of values that remain on the variables that were labeled for each backtracking history level
 */
CUDA_FUNC void set_shared_store( __global DOMAIN_* shared_ss, __global int* shared_ss_flags, CL_MEMORY VARS_PROP* vs_prop_, int v_id,
		__global DOMAIN_* hist, __global int* hist_labeleds_n_vals TTL_CTR) {

	int ss_to_fill;

	// flags for signaling the state of each work-sharing store
	// 0 - next shared SS to be picked
	// 1 - next shared SS to be filled
	// 2...number of SS already filled
	// 3..3+CL_N_SHARED_SS - V_ID that was labeled to generate this SS
	if ((ss_to_fill = atomic_inc(&shared_ss_flags[1])) < CL_N_SHARED_SS) {

		__global DOMAIN_* new_ss;
		int min;
		int i;

		// copy the new store
		new_ss = &shared_ss[ss_to_fill * CL_N_VS];
		for (i = 0; i < CL_N_VS; i++) {
			CHECK_TTL(ttl_ctr, 33)

					cl_d_copy_gm(&new_ss[i], &vs_prop_[i].prop_d TTL_CTR_V);
		}

		cl_d_calc_min_val_g(&min, hist TTL_CTR_V);

		// remove value from backtracking history
		cl_d_del_val_no_tests_g(hist, min);
		(*hist_labeleds_n_vals)--;

		cl_d_new_vals_gp(&new_ss[v_id], &min, 1 TTL_CTR_V);

		// save the ID of the variable that was labeled to generate the new SS
		shared_ss_flags[3 + ss_to_fill] = v_id;

		atomic_inc(&shared_ss_flags[2]);
	}
}
#endif

/*
 * Mark all constraints as not to be ignored
 * cs_ignore - array with one flag per constraint
 */
#if CL_CS_IGNORE
CUDA_FUNC void clear_cs_ignore(__global char *cs_ignore) {
int i;

for (i = 0; i < CL_N_CS; i++) {
	cs_ignore[i] = 0;
}
}
#endif

#if CL_PRINT_CSP

/*
 * Print the name of the constraint
 * cs -constraint to print the name
 */
CUDA_FUNC void cs_print_type_device(CL_CS_MEM cl_constr* cs) {
	switch (cs->kind) {
	case ALL_DIFFERENT:
		printf((__constant char *)"ALL_DIFFERENT");
		break;
	case ARRAY_BOOL_AND:
		printf((__constant char *)"ARRAY_BOOL_AND");
		break;
	case ARRAY_BOOL_ELEMENT:
		printf((__constant char *)"ARRAY_BOOL_ELEMENT");
		break;
	case ARRAY_BOOL_OR:
		printf((__constant char *)"ARRAY_BOOL_OR");
		break;
	case ARRAY_BOOL_XOR:
		printf((__constant char *)"ARRAY_BOOL_XOR");
		break;
	case ARRAY_INT_ELEMENT:
		printf((__constant char *)"ARRAY_INT_ELEMENT");
		break;
	case ARRAY_VAR_INT_ELEMENT:
		printf((__constant char *)"ARRAY_VAR_INT_ELEMENT");
		break;
	case AT_LEAST:
		printf((__constant char *)"AT_LEAST");
		break;
	case AT_MOST:
		printf((__constant char *)"AT_MOST");
		break;
	case AT_MOST_ONE:
		printf((__constant char *)"AT_MOST_ONE");
		break;
	case BOOL_AND:
		printf((__constant char *)"BOOL_AND");
		break;
	case BOOL_CLAUSE:
		printf((__constant char *)"BOOL_CLAUSE");
		break;
	case BOOL_EQ:
		printf((__constant char *)"BOOL_EQ");
		break;
	case BOOL_LE:
		printf((__constant char *)"BOOL_LE");
		break;
	case BOOL_LIN_EQ:
		printf((__constant char *)"BOOL_LIN_EQ");
		break;
	case BOOL_LIN_LE:
		printf((__constant char *)"BOOL_LIN_LE");
		break;
	case BOOL_LT:
		printf((__constant char *)"BOOL_LT");
		break;
	case BOOL_NOT:
		printf((__constant char *)"BOOL_NOT");
		break;
	case BOOL_OR:
		printf((__constant char *)"BOOL_OR");
		break;
	case BOOL_XOR:
		printf((__constant char *)"BOOL_XOR");
		break;
	case BOOL2INT:
		printf((__constant char *)"BOOL2INT");
		break;
	case ELEMENT:
		printf((__constant char *)"ELEMENT");
		break;
	case EXACTLY:
		printf((__constant char *)"EXACTLY");
		break;
	case EXACTLY_VAR:
		printf((__constant char *)"EXACTLY_VAR");
		break;
	case INT_DIV:
		printf((__constant char *)"INT_DIV");
		break;
	case INT_EQ:
		printf((__constant char *)"INT_EQ");
		break;
	case INT_EQ_C:
		printf((__constant char *)"INT_EQ_C");
		break;
	case INT_LE:
		printf((__constant char *)"INT_LE");
		break;
	case INT_LIN_EQ:
		printf((__constant char *)"INT_LIN_EQ");
		break;
	case INT_LIN_LE:
		printf((__constant char *)"INT_LIN_LE");
		break;
	case INT_LIN_NE:
		printf((__constant char *)"INT_LIN_NE");
		break;
	case INT_LIN_VAR:
		printf((__constant char *)"INT_LIN_VAR");
		break;
	case INT_LT:
		printf((__constant char *)"INT_LT");
		break;
	case INT_MAX_:
		printf((__constant char *)"INT_MAX_");
		break;
	case INT_MIN_:
		printf((__constant char *)"INT_MIN_");
		break;
	case INT_MOD:
		printf((__constant char *)"INT_MOD");
		break;
	case INT_NE:
		printf((__constant char *)"INT_NE");
		break;
	case INT_PLUS:
		printf((__constant char *)"INT_PLUS");
		break;
	case INT_TIMES:
		printf((__constant char *)"INT_TIMES");
		break;
	case MAXIMIZE:
		printf((__constant char *)"MAXIMIZE");
		break;
	case MINIMIZE:
		printf((__constant char *)"MINIMIZE");
		break;
	case MINUS_EQ:
		printf((__constant char *)"MINUS_EQ");
		break;
	case MINUS_NE:
		printf((__constant char *)"MINUS_NE");
		break;
	case SUM:
		printf((__constant char *)"SUM");
		break;
	case SUM_PROD:
		printf((__constant char *)"SUM_PROD");
		break;
	case SUM_VAR:
		printf((__constant char *)"SUM_VAR");
		break;
	case VAR_EQ_MINUS:
		printf((__constant char *)"VAR_EQ_MINUS");
		break;
	case VAR_EQ_MINUS_ABS:
		printf((__constant char *)"VAR_EQ_MINUS_ABS");
		break;
	default:
		printf((__constant char *)"NOT_RECOGNIZED");
		break;
	}

	if (cs->reified) {
		printf((__constant char *)"_REIF");
	}
}

/*
 * Print the name of the heuristic used for selecting the next variable to label
 * l - ENUM of the labeling heuristic
 */
CUDA_FUNC void print_label_heur_device(char l) {
	switch (l) {
	case CL_ANTI_FIRST_FAIL:
		printf((__constant char *)"Anti_first_fail");
		break;
	case CL_FIRST_FAIL:
		printf((__constant char *)"First_fail");
		break;
	case CL_INPUT_ORDER:
		printf((__constant char *)"Input_order");
		break;
	case CL_LARGEST:
		printf((__constant char *)"Largest");
		break;
	case CL_MAX_REGRET:
		printf((__constant char *)"Max_regret");
		break;
	case CL_MOST_CONSTRAINED:
		printf((__constant char *)"Most_constrained");
		break;
	case CL_OCCURRENCE:
		printf((__constant char *)"Occurrence");
		break;
	case CL_SMALLEST:
		printf((__constant char *)"Smallest");
		break;
	default:
		printf((__constant char *)"UNKNOWN");
		break;
	}
}

/*
 * Print the name of the heuristic used for selecting the next value to assign
 * a - ENUM of the labeling heuristic
 */
CUDA_FUNC void print_assign_heur_device(char a) {
	switch (a) {
	case CL_INDOMAIN_INTERVAL:
		printf((__constant char *)"Indomain_interval");
		break;
	case CL_INDOMAIN_MAX:
		printf((__constant char *)"Indomain_max");
		break;
	case CL_INDOMAIN_MEDIAN:
		printf((__constant char *)"Indomain_median");
		break;
	case CL_INDOMAIN_MIDDLE:
		printf((__constant char *)"Indomain_middle");
		break;
	case CL_INDOMAIN_MIN:
		printf((__constant char *)"Indomain_min");
		break;
	case CL_INDOMAIN_REVERSE_SPLIT:
		printf((__constant char *)"Indomain_reverse_split");
		break;
	case CL_INDOMAIN_SPLIT:
		printf((__constant char *)"Indomain_split");
		break;
	default:
		printf((__constant char *)"UNKNOWN");
		break;
	}
}

/*
 * Print all the CSP variables and constraints, including the variables values and ID and
 * the constraints ID and the ID of the variables that they constrain
 * vs - CSP variables
 * cs - CSP constraints
 * cs_per_v_idx - vector with all the constraints ID that constrain each variable, per variable ID order
 * vs_per_c_idx - vector with all constrained variables ID per constraint, per constraint ID order
 * c_consts - vector with all the constant values of a CSP
 * b_ds - original domain of the variables when using bitmaps
 */
CUDA_FUNC void print_CSP_device(CL_VS_MEM VARS* vs, CL_CS_MEM cl_constr* cs, CL_INTS_MEM int* cs_per_v_idx, CL_INTS_MEM int* vs_per_c_idx
#if CS_AT_LEAST == 1 || CS_AT_MOST == 1 || CS_AT_MOST_ONE == 1 || CS_EXACTLY == 1 || CS_INT_LIN_EQ == 1 || CS_INT_LIN_LE == 1 || CS_INT_LIN_NE == 1 || CS_INT_LIN_VAR == 1 || CS_ARRAY_INT_ELEMENT == 1  || CS_BOOL_LIN_EQ == 1 || CS_BOOL_LIN_LE == 1
		, CL_INTS_MEM int* c_consts
#endif
#if CL_D_TYPE == CL_BITMAP
		, CL_B_DS_MEM cl_bitmap* b_ds
#endif
) {

	unsigned int prev_val;
	unsigned int new_val;
	unsigned int cntr;
	int d_vals[CL_D_MAX + 1];
	int n_vals, max;
	CL_INTS_MEM int* vs_per_c_idx_;
	CL_INTS_MEM int* cs_per_v_idx_;
	DOMAIN_ d;
	unsigned int i;
	int j;

#if CS_AT_LEAST == 1 || CS_AT_MOST == 1 || CS_AT_MOST_ONE == 1 || CS_EXACTLY == 1 || CS_INT_LIN_EQ == 1 || CS_INT_LIN_LE == 1 || CS_INT_LIN_NE == 1 || CS_INT_LIN_VAR == 1 || CS_ARRAY_INT_ELEMENT == 1  || CS_BOOL_LIN_EQ == 1 || CS_BOOL_LIN_LE == 1
	CL_INTS_MEM int* c_consts_;
#endif

	printf((__constant char *)"\n\n--------------------------------\n");
	printf((__constant char *)"CSP as received by the device:\n");

	printf((__constant char *)"\nVariables:\n");
	for (i = 0; i < CL_N_VS; i++) {
		printf((__constant char *)"   ID=%u:  Values={", i);

#if CL_D_TYPE == CL_BITMAP
#if CL_N_WORDS == 1
		d = b_ds[i];
#else
		for (j = 0; j < CL_N_WORDS; j++) {
			CHECK_TTL(ttl_ctr, 117)
					d[j] = b_ds[i][j];
		}
#endif

		cl_d_cnt_vals_n(&d, &n_vals);
		cl_d_calc_max_val_n(&max, &d);
		cl_d_get_nth_vals_n(&d, 1, n_vals, d_vals TTL_CTR_V);

		j = 0;

		prev_val = convert_uint(d_vals[j++]);
		new_val = prev_val;
		printf((__constant char *)"%u", prev_val);
		while (new_val < (uint)max) {

			cntr = 0;
			while ((new_val = convert_uint(d_vals[j++])) == prev_val + 1 && new_val < (uint)max) {
				prev_val = new_val;
				cntr++;
			}

			if (cntr == 0) {
				printf((__constant char *)",%u", new_val);
			} else {
				if (new_val == (uint)max && new_val == prev_val + 1) {
					printf((__constant char *)"-%u", new_val);
				} else if (cntr == 1) {
					printf((__constant char *)",%u,%u", prev_val, new_val);
				} else {
					printf((__constant char *)"-%u,%u", prev_val, new_val);
				}
			}
			prev_val = new_val;
		}

#else
		printf((__constant char *)"%u,%u", vs[i].domain.s0, vs[i].domain.s1);
#endif

		if (vs[i].to_label) {
			printf((__constant char *)"}  Label=true");
		} else {
			printf((__constant char *)"}  Label=false");
		}

		if (vs[i].boolean) {
			printf((__constant char *)"  boolean=true");
		} else {
			printf((__constant char *)"  boolean=false");
		}

#if CL_FZN_SEQ && CL_FZN_SEQ_N_LABELS > 1
		if (vs[i].to_label) {
			printf("  label_h=");
			print_label_heur_device(vs[i].label_h);
			printf("  assign_hs=");
			print_assign_heur_device(vs[i].assign_h);
		}
#endif

		if (vs[i].expanded) {
			printf((__constant char *)"  expanded");
		}

		if (vs[i].n_cs > 0) {
			printf((__constant char *)"  Constraints={");

			cs_per_v_idx_ = &cs_per_v_idx[vs[i].c_idx];

			for (j = 0; j < vs[i].n_cs - 1; j++) {
				printf((__constant char *)"%u,", cs_per_v_idx_[j]);
			}
			if (vs[i].n_cs > 0) {
				printf((__constant char *)"%u}\n", cs_per_v_idx_[j]);
			} else {
				printf((__constant char *)"\n");
			}
		} else {
			printf((__constant char *)"\n");
		}
	}

	printf((__constant char *)"Constraints:\n");
	for (i = 0; i < CL_N_CS; i++) {

		vs_per_c_idx_ = &vs_per_c_idx[cs[i].v_idx];

#if CS_AT_LEAST == 1 || CS_AT_MOST == 1 || CS_AT_MOST_ONE == 1 || CS_EXACTLY == 1 || CS_INT_LIN_EQ == 1 || CS_INT_LIN_LE == 1 || CS_INT_LIN_NE == 1 || CS_INT_LIN_VAR == 1 || CS_ARRAY_INT_ELEMENT == 1  || CS_BOOL_LIN_EQ == 1 || CS_BOOL_LIN_LE == 1
		c_consts_ = &c_consts[cs[i].const_idx];
#endif

		printf((__constant char *)"   ID=%u:  Type=", i);
		cs_print_type_device(&cs[i]);
		printf((__constant char *)"  Variables={");
		for (j = 0; j < cs[i].n_c_vs - 1; j++) {
			printf((__constant char *)"%u,", vs_per_c_idx_[j]);
		}
		printf((__constant char *)"%u}", vs_per_c_idx_[j]);

		if (cs[i].n_c_consts > 0) {

#if CS_AT_LEAST == 1 || CS_AT_MOST == 1 || CS_AT_MOST_ONE == 1 || CS_EXACTLY == 1 || CS_INT_LIN_EQ == 1 || CS_INT_LIN_LE == 1 || CS_INT_LIN_NE == 1 || CS_INT_LIN_VAR == 1 || CS_ARRAY_INT_ELEMENT == 1  || CS_BOOL_LIN_EQ == 1 || CS_BOOL_LIN_LE == 1
			printf((__constant char *)"  Constants={");
			for (j = 0; j < cs[i].n_c_consts - 1; j++) {
				printf((__constant char *)"%d,", c_consts_[j]);
			}

			if (cs[i].kind == INT_LIN_EQ || cs[i].kind == INT_LIN_NE || cs[i].kind == INT_LIN_LE || cs[i].kind == BOOL_LIN_LE) {

				printf((__constant char *)"%d, %d}", c_consts_[j], cs[i].constant_val);
			} else {
				printf((__constant char *)"%d}", c_consts_[j]);
			}
#endif

		} else if (cs[i].kind == ELEMENT || cs[i].kind == EXACTLY_VAR || cs[i].kind == INT_LIN_EQ || cs[i].kind == INT_LIN_NE || cs[i].kind == MINUS_EQ
				|| cs[i].kind == MINUS_NE || cs[i].kind == SUM_PROD || cs[i].kind == SUM || cs[i].kind == INT_LIN_LE || cs[i].kind == ARRAY_INT_ELEMENT
				|| cs[i].kind == INT_EQ_C) {
			printf((__constant char *)"  Constants={%d}", cs[i].constant_val);
		}

		if (cs[i].boolean) {
			printf("  boolean");
		}

		if (cs[i].reified) {
			printf((__constant char *)"  reif_var_ID=%u\n", cs[i].reif_var_id);
		} else {
			printf((__constant char *)"\n");
		}
	}
	printf((__constant char *)"\n");
	printf((__constant char *)"--------------------------------\n\n");
}
#endif

/*
 * place the next unexplored sub-search space available on hist or place CL_N_VS on prop_v_id if none
 * atoms - counters and stores enumeration
 * vs - all CSP variables with the original domains
 * hist - current work-item history vector
 * vs_prop_ - vector with all CSP variables
 * v_id_to_prop - id of the variable to propagate
 * hist_tree_level - level of the backtracking
 * hist_labeleds_id - list of the ID of the variables that were labeled for each backtracking history level
 * b_ds - original domains of the CSP variables if using bitmaps
 * val_to_opt_g - value to optimize
 * ss_aux_mem - auxiliary buffer
 */
CUDA_FUNC void get_new_str( __global unsigned int *atoms, CL_VS_MEM VARS *vs, __global DOMAIN_ *hist, CL_MEMORY VARS_PROP *vs_prop_,
		CL_MEMORY unsigned short *vs_id_to_prop_, int *hist_tree_level, __global int *hist_labeleds_id, __global int *hist_labeleds_n_vals,
		unsigned int *prop_v_id
#if CL_D_TYPE == CL_BITMAP
	, CL_B_DS_MEM cl_bitmap *b_ds
#endif
#if (CS_MAXIMIZE == 1 || CS_MINIMIZE == 1) && CL_WORK == CL_OPT
	, __global unsigned int *val_to_opt_g
#endif
	, __global int *ss_aux_mem TTL_CTR) {

// atoms
__global unsigned int *str_to_expl = atoms;	// first available store index
unsigned int str_last = atoms[1];	// last available store index
unsigned int n_ss = atoms[2];		// total number of generated sub-search spaces (n_ss)
unsigned int depth = atoms[3];		// level of tree expansion needed to create the required number of sub-search spaces
__global unsigned int *exp_values = atoms + 5;	// each variable number of values expanded

// to find which values of each variable to domain to place in each store
unsigned int prev_repeat = 0;	// number of times that each value of the previous domain was repeated to generate all stores
unsigned int curr_repeat = 0;	// number of times that each value of the current domain must be repeated to generate all stores
unsigned int join_n_vals;		// number of values of the current domain that must be repeated in each store
unsigned int join_more_times;	// number of values that must be distributed among some of the stores as the reminder was not 0

unsigned int rel_store_to_synt;		// Number of the next store to generate, when multiplying stores in the device
unsigned int store_to_synt = atomic_inc(str_to_expl);	// Number of the next store to generate
int first_nth;	// index of the first value to get from domain (begin at 1)
int last_nth;	// index of the last value to get from domain (begin at 1)
bool first_expand = true;
unsigned int i;

*prop_v_id = CL_N_VS;

if (store_to_synt < str_last) {

	for (i = 0; i < depth; i++) {
		CHECK_TTL(ttl_ctr, 4)

		if (exp_values[i] == 0) {
#if CL_D_TYPE == CL_BITMAP
			cl_d_copy_mbd(&vs_prop_[i].prop_d, &b_ds[i] TTL_CTR_V);
#else
			cl_d_copy_mvs(&vs_prop_[i].prop_d, &vs[i].domain TTL_CTR_V);
#endif

		} else {

			if (first_expand) {
				prev_repeat = n_ss;
				rel_store_to_synt = store_to_synt;
				first_expand = false;
			} else {
				rel_store_to_synt = store_to_synt % prev_repeat;
			}
			curr_repeat = prev_repeat / exp_values[i];

			join_n_vals = convert_uint (vs[i].n_vals) / exp_values[i];
			if (join_n_vals == 0) {
				join_n_vals = 1;
			}
			join_more_times = (convert_uint (vs[i].n_vals) % exp_values[i]) * curr_repeat;

			first_nth = convert_int (1 + (rel_store_to_synt / curr_repeat) * join_n_vals);

			if (join_more_times > 0) {
				if (rel_store_to_synt > join_more_times) {
					first_nth += convert_int (join_more_times / curr_repeat);
				} else {
					first_nth += convert_int (rel_store_to_synt / curr_repeat);
				}
			}

			last_nth = first_nth + convert_int (join_n_vals);
			if (rel_store_to_synt < join_more_times) {
				last_nth++;
			}

			prev_repeat = curr_repeat;

#if CL_D_TYPE == CL_BITMAP
			cl_d_get_nth_vals_bd(&b_ds[i], first_nth, last_nth - 1, ss_aux_mem TTL_CTR_V);
#else
			cl_d_get_nth_vals_vsg(&vs[i].domain, first_nth, last_nth - 1, ss_aux_mem TTL_CTR_V);
#endif
			cl_d_new_vals_mg(&vs_prop_[i].prop_d, ss_aux_mem, last_nth - first_nth TTL_CTR_V);
		}
	}

	for (i = depth; i < CL_N_VS; i++) {
		CHECK_TTL(ttl_ctr, 6)

#if CL_D_TYPE == CL_BITMAP
		cl_d_copy_mbd(&vs_prop_[i].prop_d, &b_ds[i] TTL_CTR_V);
#else
			cl_d_copy_mvs(&vs_prop_[i].prop_d, &vs[i].domain TTL_CTR_V);
#endif
	}

#if CL_WORK == CL_OPT
	unsigned int val_to_opt_aux = atomic_add(val_to_opt_g, 0);
	bool changed = 0;

	vs_prop_[CL_VAR_ID_TO_OPT].to_prop = 0;
#if CL_USE_BOOLEAN_VS
	vs_prop_[CL_VAR_ID_TO_OPT].boolean = vs[CL_VAR_ID_TO_OPT].boolean;
#endif
	cl_v_calc_min_val_m(&vs_prop_[CL_VAR_ID_TO_OPT] TTL_CTR_V);
	cl_v_calc_max_val_m(&vs_prop_[CL_VAR_ID_TO_OPT] TTL_CTR_V);
	cl_v_cnt_vals_m(&vs_prop_[CL_VAR_ID_TO_OPT] TTL_CTR_V);

#if CS_MINIMIZE == 1
	cl_v_del_gt_m(&changed, &vs_prop_[CL_VAR_ID_TO_OPT], convert_int (val_to_opt_aux) TTL_CTR_V);
#else
		cl_v_del_lt_m(&changed, &vs_prop_[CL_VAR_ID_TO_OPT], convert_int(val_to_opt_aux) TTL_CTR_V);
#endif
#endif

	for (i = 0; i < CL_N_VS; i++) {
		CHECK_TTL(ttl_ctr, 7)

		cl_d_copy_gm(&hist[i], &vs_prop_[i].prop_d TTL_CTR_V);

		vs_prop_[i].to_prop = 0;
#if CL_USE_BOOLEAN_VS
		vs_prop_[i].boolean = vs[i].boolean;
#endif
		cl_v_calc_min_val_m(&vs_prop_[i] TTL_CTR_V);
		cl_v_calc_max_val_m(&vs_prop_[i] TTL_CTR_V);
		cl_v_cnt_vals_m(&vs_prop_[i] TTL_CTR_V);
	}

	*prop_v_id = 0;
	// needed to test expanded values
	for (i = 0; i < depth; i++) {
		CHECK_TTL(ttl_ctr, 8)

		if (vs[i].to_label || vs[i].expanded) {
			*prop_v_id = i;
			i = depth;
		}
	}

	hist_labeleds_id[0] = convert_int (*prop_v_id);
	hist_labeleds_n_vals[0] = 0;
	(*hist_tree_level) = 1; // reset hist current level

	// reset the indexes of the array that contains the IDs of the variables to propagate
	vs_id_to_prop_[0] = 2;
	vs_id_to_prop_[1] = 2;

	// if optimizing set variable to optimize for being propagated to update its domain
#if CL_WORK == CL_OPT
	v_add_to_prop(vs_id_to_prop_, vs_prop_, convert_int (*prop_v_id));
	*prop_v_id = CL_VAR_ID_TO_OPT;
#endif

	// Mark variables already expanded to be propagated to check if this sub-search space is already inconsistent
	for (i = 0; i < CL_N_VS; i++) {
		CHECK_TTL(ttl_ctr, 9)

#if CL_FILTERING == 0
		if (i != *prop_v_id && (vs[i].expanded || (i < depth && exp_values[i] > 0))) {
#endif
			v_add_to_prop(vs_id_to_prop_, vs_prop_, convert_int (i));

#if CL_FILTERING == 0
				}
#endif
		}

#if CL_CHECK_ERRORS
		int l;
		for (l = 0; l < CL_N_VS; l++) {

			bool empty;
#if CL_N_WORDS == 1
			empty = (vs_prop_[l].prop_d == 0);
#else
			int m;
			empty = 1;
			for (m = 0; m < CL_N_WORDS; m++) {
				CHECK_TTL(ttl_ctr, 115)
						if (vs_prop_[l].prop_d[m] != 0) {
							empty = 0;
							m = CL_N_WORDS;
						}
			}
#endif
			if (empty || vs_prop_[l].n_vals > vs_prop_[l].max + 1 || vs_prop_[l].min > vs_prop_[l].max || vs_prop_[l].max > CL_D_MAX) {
				printf((__constant char *)"\n###error 74\n");
				printf((__constant char *)"v_id=%d, empty=%d, vs_prop_[l].n_vals=%u, vs_prop_[l].min=%u, vs_prop_[l].max=%u\n",
						l, empty, vs_prop_[l].n_vals, vs_prop_[l].min, vs_prop_[l].max);
			}
		}
#endif
	}
}