/*
 * 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

}

/*
 * Return the next variable to propagate by selecting the first one on vs_id_to_prop_ vector, or CL_N_VS if none
 * vs_id_to_prop_ - circular vector with the ids of the variables to propagate
 * vs_prop_ - vector with all CSP variables
 * vs - vector with all CSP variables common to all work-items (not used with this heuristic)
 */
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_FIRST_FAIL
/*
 * Return the next variable to label 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
 */
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 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 (vs[i].to_label && n_vals > 1 && n_vals < vals_cnt) {
			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;
			}
		}
	}

#if CL_TO_LABEL_THRESHOLD > 0
	if (v_idx == CL_N_VS) {
		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 35\n");
			}
#endif

			n_vals = V_N_VALS(vs_prop_[i]);
			if (!vs[i].to_label && n_vals > 1 && n_vals < vals_cnt) {
				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;
				}
			}
		}
	}
#endif

	*prop_v_id = convert_ushort(v_idx);
}

#elif CL_LABEL_M == CL_INPUT_ORDER
/*
 * Return the next variable to label 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
 */
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 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 (vs[i].to_label && V_N_VALS(vs_prop_[i]) > 1) {
			v_idx = i;
			i = CL_N_VS;
		}
	}

#if CL_TO_LABEL_THRESHOLD > 0
	if (v_idx == CL_N_VS) {
		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 37\n");
		}
#endif

			if (!vs[i].to_label && V_N_VALS(vs_prop_[i]) > 1) {
				v_idx = i;
				i = CL_N_VS;
			}
		}
	}
#endif

	*prop_v_id = convert_ushort(v_idx);
}

#elif CL_LABEL_M == CL_OCCURRENCE
/*
 * Return the next variable to label 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
 */
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 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 (vs[i].to_label && vs[i].n_cs > max_cs_cnt && V_N_VALS(vs_prop_[i]) > 1) {
			max_cs_cnt = vs[i].n_cs;

			v_idx = i;
		}
	}

#if CL_TO_LABEL_THRESHOLD > 0
	if (v_idx == CL_N_VS) {
		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 39\n");
			}
#endif

			if (!vs[i].to_label && vs[i].n_cs > max_cs_cnt && V_N_VALS(vs_prop_[i]) > 1) {
				max_cs_cnt = vs[i].n_cs;

				v_idx = i;
			}
		}
	}
#endif

	*prop_v_id = convert_ushort(v_idx);
}

#elif CL_LABEL_M == CL_MAX_REGRET
/*
 * Return the next variable to label 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
 */
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 diff_aux;
	int diff = 0;
	int v_idx = CL_N_VS;
	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 (vs[i].to_label && V_N_VALS(vs_prop_[i]) > 1) {

			v_get_max_regret_diff_m(&diff_aux, &vs_prop_[i]);

			if (diff_aux > diff) {

				diff = diff_aux;
				v_idx = i;
			}
		}
	}

#if CL_TO_LABEL_THRESHOLD > 0
	if (v_idx == CL_N_VS) {
		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 41\n");
			}
#endif

			if (!vs[i].to_label && V_N_VALS(vs_prop_[i]) > 1) {

				v_get_max_regret_diff_m(&diff_aux, &vs_prop_[i]);

				if (diff_aux > diff) {

					diff = diff_aux;
					v_idx = i;
				}
			}
		}
	}
#endif

	*prop_v_id = v_idx;
}
#endif

#if CL_LABEL_M == CL_SMALLEST
/*
 * Return the next variable to label 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
 */
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 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 (vs[i].to_label && V_N_VALS(vs_prop_[i]) > 1 && V_MIN(vs_prop_[i]) < min) {

			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;
			}
		}
	}

#if CL_TO_LABEL_THRESHOLD > 0
	if (v_idx == CL_N_VS) {
		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 43\n");
			}
#endif

			if (!vs[i].to_label && V_N_VALS(vs_prop_[i]) > 1 && V_MIN(vs_prop_[i]) < min) {

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

				// If the minimum value is 0, stop searching
				if (min == 0) {
					break;
				}
			}
		}
	}
#endif

	*prop_v_id = v_idx;
}
#endif

#if CL_ASSIGN_M == CL_MIN_VAL
/*
 * 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
 */
CUDA_FUNC void v_assign(CL_MEMORY VARS_PROP* v, __global DOMAIN_* hist, __global int* hist_labeleds_n_vals TTL_CTR) {

#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);
	}
}

#elif CL_ASSIGN_M == CL_MAX_VAL
/*
 * 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
 */
CUDA_FUNC void v_assign(CL_MEMORY VARS_PROP* v, __global DOMAIN_* hist, __global int* hist_labeleds_n_vals) {

#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);
	}
}

#elif CL_ASSIGN_M == CL_SPLIT_VALS
/*
 * 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
 */
CUDA_FUNC void v_assign(CL_MEMORY VARS_PROP* v, __global DOMAIN_* hist, __global int* hist_labeleds_n_vals) {

#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_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 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 - CSP variables
 * 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 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

#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 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 ELEMENT:
			printf((__constant char *)"ELEMENT");
			break;
		case ELEMENT_INT_VAR:
			printf((__constant char *)"ELEMENT_INT_VAR");
			break;
		case ELEMENT_VAR:
			printf((__constant char *)"ELEMENT_VAR");
			break;
		case EQ:
			printf((__constant char *)"EQ");
			break;
		case EQ_VAR:
			printf((__constant char *)"EQ_VAR");
			break;
		case EXACTLY:
			printf((__constant char *)"EXACTLY");
			break;
		case EXACTLY_VAR:
			printf((__constant char *)"EXACTLY_VAR");
			break;
		case LE:
			printf((__constant char *)"LE");
			break;
		case LINEAR:
			printf((__constant char *)"LINEAR");
			break;
		case LINEAR_VAR:
			printf((__constant char *)"LINEAR_VAR");
			break;
		case LT:
			printf((__constant char *)"LT");
			break;
		case MAX:
			printf((__constant char *)"MAX");
			break;
		case MAXIMIZE:
			printf((__constant char *)"MAXIMIZE");
			break;
		case MIN:
			printf((__constant char *)"MIN");
			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 NE:
			printf((__constant char *)"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_PLUS:
			printf((__constant char *)"VAR_EQ_PLUS");
			break;
		case VAR_EQ_TIMES:
			printf((__constant char *)"VAR_EQ_TIMES");
			break;
		case VAR_EQ_MINUS_ABS:
			printf((__constant char *)"VAR_EQ_MINUS_ABS");
			break;
		case LINEAR_NE:
			printf((__constant char *)"LINEAR_NE");
			break;
		case LINEAR_LT:
			printf((__constant char *)"LINEAR_LT");
			break;
		case BOOL_OR:
			printf((__constant char *)"BOOL_OR");
			break;
		case BOOL_AND:
			printf((__constant char *)"BOOL_AND");
			break;
		case BOOL_CLAUSE:
			printf((__constant char *)"BOOL_CLAUSE");
			break;
		case BOOL2INT:
			printf((__constant char *)"BOOL2INT");
			break;
		default:
			printf((__constant char *)"NOT_RECOGNIZED");
			break;
	}

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

/*
 * 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
 */
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_LINEAR == 1 || CS_LINEAR_LT == 1 || CS_LINEAR_NE == 1 || CS_LINEAR_VAR == 1 || CS_ELEMENT_INT_VAR == 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_LINEAR == 1 || CS_LINEAR_LT == 1 || CS_LINEAR_NE == 1 || CS_LINEAR_VAR == 1 || CS_ELEMENT_INT_VAR == 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].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_LINEAR == 1 || CS_LINEAR_LT == 1 || CS_LINEAR_NE == 1 || CS_LINEAR_VAR == 1 || CS_ELEMENT_INT_VAR == 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_LINEAR == 1 || CS_LINEAR_LT == 1 || CS_LINEAR_NE == 1 || CS_LINEAR_VAR == 1 || CS_ELEMENT_INT_VAR == 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 == LINEAR || cs[i].kind == LINEAR_NE || cs[i].kind == LINEAR_LT) {

				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 == LINEAR || cs[i].kind == LINEAR_NE || cs[i].kind == MINUS_EQ
				|| cs[i].kind == MINUS_NE || cs[i].kind == SUM_PROD || cs[i].kind == SUM || cs[i].kind == LINEAR_LT || cs[i].kind == ELEMENT_INT_VAR
				|| cs[i].kind == EQ) {
			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

// strs:
// 0...CL_N_VS - strs
// repeat n_strs times
//
// hists:
// 0 - labeled variable for the next level
// 1 - remaining number of values on the labeled variable
// 2...CL_N_VS - level domains
// 2+CL_N_VS - labeled variable for the next level
// 3+CL_N_VS...3+CL_N_VS+CL_N_VS - level domains
// ...
/*
 * place the next unexplored sub-search space available on hist and return 1 if succeeded or 0 if not
 * strs - vector with all stores
 * str_first - index of the next store to pick
 * vs - all CSP variables with the original domains
 * hist - current work-item history vector
 * n_ss - number of sub-search spaces (stores) in strs
 * depth - main search space exploration depth needed to fill all stores
 */
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

	unsigned int prev_repeat = 0;
	unsigned int curr_repeat = 0;
	unsigned int rel_store_to_synt;
	unsigned int store_to_synt = atomic_inc(str_to_expl);	// increase the next store to pick index
	unsigned int join_n_vals;
	unsigned int join_more_times;
	int first_nth;
	int last_nth;
	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 = vs[i].n_vals / exp_values[i];
					if (join_n_vals == 0) {
						join_n_vals = 1;
					}
					join_more_times = (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_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_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;
		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
	}
}