/*
 * element.c
 *
 *  Created on: 26/01/2017
 *      Author: pedro
 */

#ifndef __OPENCL_VERSION__

#include <stddef.h>
#include <stdio.h>

#include "element.h"

#include "../bitmaps.h"
#include "../config.h"
#include "../variables.h"

#endif

#include "../kernels/cl_aux_functions.h"
#if CL_D_TYPE == CL_BITMAP
#include "../kernels/cl_bitmaps.h"
#elif CL_D_TYPE == CL_INTERVAL
#include  "../kernels/cl_intervals.h"
#endif
#include "../kernels/cl_constraints.h"
#include "../kernels/cl_variables.h"
#include "../kernels/cl_ttl.h"

#ifndef __OPENCL_VERSION__

/*
 * Creates a new constraint of the element type and return the constraint ID
 * 1 ≤ y <= n ∧ X[y] = k
 * X_ids - vector with the ID of the variables that may be in the domain of y_id variable
 * n_vs - maximum number of variables in X vector
 * y_id - ID of the variable whose domain are the index of the variables in X_ids vector
 * k - Value that should be in X_ids[y_id] domain
 */
unsigned int c_element(unsigned int* X_ids, unsigned int n_vs, unsigned int y_id, unsigned int k) {
	var* y = &VS[y_id];
	unsigned int i;

	if (y->max > n_vs) {
		v_del_gt(y, (int)n_vs);
		if (y->n_vals == 0) {
			fprintf(stderr, "\nError: Constraint ELEMENT makes model inconsistent at creation:\n");
			exit(-1);
		}
	}

	if (y->min == 0) {
		v_del_val(y, 0);
		if (y->n_vals == 0) {
			fprintf(stderr, "\nError: Constraint ELEMENT makes model inconsistent at creation:\n");
			exit(-1);
		}
	}

	// set to include in kernel compilation
	USE_CS[ELEMENT] = 1;
	USE_NON_CS_REIFI[ELEMENT] = 1;
	REV = 1;

	unsigned int* c_vs = malloc((n_vs + 1) * sizeof(unsigned int));

	for (i = 0; i < n_vs; i++) {
		c_vs[i] = X_ids[i];
	}

	c_vs[n_vs] = y_id;

	// creates a new generic constraint
	unsigned int c_id = c_new(c_vs, n_vs + 1, NULL, 0, -1);

	// pointers to this type of constraint functions
	CS[c_id].kind = ELEMENT;
	CS[c_id].check_sol_f = &element_check;
	CS[c_id].constant_val = (int)k;
	free(c_vs);

	return c_id;
}

/*
 * Creates a new reified constraint of the element type and return the constraint ID
 * 1 ≤ y <= n ∧ X[y] = k
 * X_ids - vector with the ID of the variables that may be in the domain of y_id variable
 * n_vs - maximum number of variables in X vector
 * y_id - ID of the variable whose domain are the index of the variables in X_ids vector
 * k - Value that should be in X_ids[y_id] domain
 * reif_v_id - ID of the reification variable
 */
unsigned int c_element_reif(unsigned int* X_ids, unsigned int n_vs, unsigned int y_id, unsigned int k, int reif_v_id) {
	var* y = &VS[y_id];
	unsigned int i;

	if (VS[reif_v_id].max > 1) {
		v_del_gt(&VS[reif_v_id], 1);

		if (VS[reif_v_id].n_vals == 0) {
			fprintf(stderr, "\nError: Constraint ELEMENT_REIF makes model inconsistent at creation:\n");
			exit(-1);
		}
	}

	if (y->max > n_vs) {
		v_del_gt(y, (int)n_vs);
		if (y->n_vals == 0) {
			fprintf(stderr, "\nError: Constraint ELEMENT_REIF makes model inconsistent at creation:\n");
			exit(-1);
		}
	}

	if (y->min == 0) {
		v_del_val(y, 0);
		if (y->n_vals == 0) {
			fprintf(stderr, "\nError: Constraint ELEMENT_REIF makes model inconsistent at creation:\n");
			exit(-1);
		}
	}

	// set to include in kernel compilation
	USE_CS[ELEMENT] = 1;
	USE_CS_REIFI[ELEMENT] = 1;
	REV = 1;

	unsigned int* c_vs = malloc((n_vs + 1) * sizeof(unsigned int));

	for (i = 0; i < n_vs; i++) {
		c_vs[i] = X_ids[i];
	}

	c_vs[n_vs] = y_id;

	// creates a new generic constraint
	unsigned int c_id = c_new(c_vs, n_vs + 1, NULL, 0, reif_v_id);

	// pointers to this type of constraint functions
	CS[c_id].kind = ELEMENT;
	CS[c_id].check_sol_f = &element_check;
	CS[c_id].constant_val = (int)k;

	free(c_vs);

	return c_id;
}

/*
 * Return true if the element constraint is respected or false if not
 * 1 ≤ y <= n ∧ X[y] = k
 * c - constraint to check if is respected
 * explored - if the CSP was already explored, which mean that all the variables must already be singletons
 * */
bool element_check(constr* c, bool explored) {
	var** X = c->c_vs;
	var* y = c->c_vs[c->n_c_vs - 1];

	// y variable
#if CHECK_SOL_N_VALS
	if (y->to_label && y->n_vals != 1) {
		return false;
	}
#endif

	// X[y] variable
	if (
#if CHECK_SOL_N_VALS
			(X[y->min - 1]->to_label && X[y->min - 1]->n_vals != 1) ||
#endif
			X[y->min - 1]->min != c->constant_val) {

		if (explored) {
			fprintf(stderr, "\nError: Constraint ELEMENT (%d) not respected:\n", c->c_id);

			fprintf(stderr, "Variable ID=%u -> minimum=%u, maximum=%u, number of values=%u\n\n", X[y->min - 1]->v_id, b_get_min_val(&X[y->min - 1]->domain_b),
					b_get_max_val(&X[y->min - 1]->domain_b), b_cnt_vals(&X[y->min - 1]->domain_b));
			fprintf(stderr, "Variable ID=%u -> minimum=%u, maximum=%u, number of values=%u\n\n", y->v_id, b_get_min_val(&y->domain_b), b_get_max_val(&y->domain_b),
					b_cnt_vals(&y->domain_b));
		}
		return false;
	}

	return true;
}

#endif
//
//#if CS_ELEMENT == 1
///*
// * Propagate the domain of the variable with the ID prop_v_id through all the other variables on the same c_numb ID element constraint
// * 1 ≤ y <= n ∧ X[y] = k
// * prop_ok will be set to 1 if success or to 0 if any domain became empty
// * vs_per_c_idx - vector with all constrained variables ID per constraint, per constraint ID order
// * vs_prop_ - all CSP variables with current step values
// * prop_v_id - variable ID to propagate
// * current_cs - constraint that should be propagated for the variable with prop_v_id ID
// * vs_id_to_prop_ - circular vector with the ids of the variables to propagate
// */
//CUDA_FUNC void element_prop(CL_INTS_MEM int* vs_per_c_idx, CL_MEMORY VARS_PROP* vs_prop_, unsigned int prop_v_id, CL_CS_MEM cl_constr* current_cs, CL_MEMORY unsigned short* vs_id_to_prop_,
//		bool* prop_ok CS_IGNORE_FUNC TTL_CTR) {
//
//	int y_id = vs_per_c_idx[current_cs->n_c_vs - 1];	// ID of the variable whose domain are the index of the variables in elements vector
//	int k = current_cs->constant_val;
//	int x_id;
//	bool contains;
//	bool changed = 0;
//	int i;
//
//	// if y is singleton
//	if (V_N_VALS(vs_prop_[y_id]) == 1) {
//		x_id = vs_per_c_idx[V_MIN(vs_prop_[y_id]) - 1];
//
//		cl_v_del_all_except_val_m(&changed, &vs_prop_[x_id], k TTL_CTR_V);
//		if (changed) {
//
//			// if X[i] doesn't contain k
//			if (V_IS_EMPTY(vs_prop_[x_id])) {
//				*prop_ok = 0;
//				return;
//			}
//			v_add_to_prop(vs_id_to_prop_, vs_prop_, x_id);
//		}
//#if CL_CS_IGNORE
//		cs_ignore[current_cs->c_id] = 1;
//#endif
//		return;
//	}
//
//	// if y is not singleton and an x is to be propagated
//	if (prop_v_id != (unsigned int)y_id) {
//
//		cl_v_contains_val_m(&contains, &vs_prop_[prop_v_id], k TTL_CTR_V);
//		if (!contains) {
//			for (i = V_MIN(vs_prop_[y_id]); i <= V_MAX(vs_prop_[y_id]); i++) {
//				CHECK_TTL(ttl_ctr, 53)
//
//				if ((unsigned int)vs_per_c_idx[i - 1] == prop_v_id) {
//
//					cl_v_del_val_m(&changed, &vs_prop_[y_id], i TTL_CTR_V);
//					if (changed) {
//
//						if (V_IS_EMPTY(vs_prop_[y_id])) {
//							*prop_ok = 0;
//							return;
//						}
//
//						// if y was set singleton
//						if (V_N_VALS(vs_prop_[y_id]) == 1) {
//
//							x_id = vs_per_c_idx[V_MIN(vs_prop_[y_id]) - 1];
//							cl_v_del_all_except_val_m(&changed, &vs_prop_[x_id], k TTL_CTR_V);
//							if (changed) {
//
//								// if X[i] doesn't contain k
//								if (V_IS_EMPTY(vs_prop_[x_id])) {
//									*prop_ok = 0;
//									return;
//								}
//								v_add_to_prop(vs_id_to_prop_, vs_prop_, x_id);
//							}
//#if CL_CS_IGNORE
//							cs_ignore[current_cs->c_id] = 1;
//#endif
//						}
//						v_add_to_prop(vs_id_to_prop_, vs_prop_, y_id);
//					}
//					return;
//				}
//			}
//		}
//	}
//}
//
//#if CS_R_ELEMENT == 1
///*
// * Validate element constraint to be normally propagated, when reified
// * 1 ≤ y <= n ∧ X[y] = k
// * vs_per_c_idx - vector with all constrained variables ID per constraint, per constraint ID order
// * vs_prop_ - all CSP variables with current step values
// * current_cs - constraint that should be propagated for the variable with prop_v_id ID
// * vs_id_to_prop_ - circular vector with the ids of the variables to propagate
// */
//CUDA_FUNC void element_reif( CL_INTS_MEM int* vs_per_c_idx, CL_MEMORY VARS_PROP* vs_prop_, unsigned int prop_v_id, CL_CS_MEM cl_constr* current_cs, CL_MEMORY unsigned short* vs_id_to_prop_ TTL_CTR) {
//
//	int y_id = vs_per_c_idx[current_cs->n_c_vs - 1];	// ID of the variable whose domain are the index of the variables in elements vector
//	VARS_PROP y;
//	int x_id;
//	VARS_PROP x;
//	bool contains;
//	bool changed = 0;
//	int i;
//
//	// if y is singleton and x doesn't contain k is inconsistent
//	if (prop_v_id == (unsigned int)y_id && V_N_VALS(vs_prop_[y_id]) == 1) {
//
//		x_id = vs_per_c_idx[V_MIN(vs_prop_[y_id]) - 1];
//		cl_v_copy_pm(&x, &vs_prop_[x_id] TTL_CTR_V);
//
//		cl_v_del_all_except_val_n(&changed, &x, current_cs->constant_val TTL_CTR_V);
//
//		// if X[i] doesn't contain k
//		if (V_IS_EMPTY(x)) {
//			cl_v_bool_del_val_m(&vs_prop_[current_cs->reif_var_id], 1 TTL_CTR_V);
//			v_add_to_prop(vs_id_to_prop_, vs_prop_, convert_int(current_cs->reif_var_id));
//		}
//
//		// constraint already fixed
//		if (V_N_VALS(vs_prop_[x_id]) == 1) {
//			cl_v_bool_del_val_m(&vs_prop_[current_cs->reif_var_id], 0 TTL_CTR_V);
//			v_add_to_prop(vs_id_to_prop_, vs_prop_, convert_int(current_cs->reif_var_id));
//		}
//		return;
//	}
//
//	// remove x from y if x doesn't contain k
//	for (i = V_MIN(vs_prop_[y_id]); i <= V_MAX(vs_prop_[y_id]); i++) {
//		CHECK_TTL(ttl_ctr, 210)
//		x_id = vs_per_c_idx[i - 1];
//		if ((unsigned int)x_id == prop_v_id) {
//
//			cl_v_contains_val_m(&contains, &vs_prop_[x_id], current_cs->constant_val TTL_CTR_V);
//			if (!contains) {
//				cl_v_copy_pm(&y, &vs_prop_[y_id] TTL_CTR_V);
//
//				cl_v_del_val_n(&changed, &y, i TTL_CTR_V);
//				if (V_IS_EMPTY(y)) {
//					cl_v_bool_del_val_m(&vs_prop_[current_cs->reif_var_id], 1 TTL_CTR_V);
//					v_add_to_prop(vs_id_to_prop_, vs_prop_, convert_int(current_cs->reif_var_id));
//					return;
//				}
//			}
//			break;
//		}
//	}
//
//	// if y is singleton and x doesn't contain k is inconsistent
//	if (V_N_VALS(vs_prop_[y_id]) == 1) {
//
//		x_id = vs_per_c_idx[V_MIN(vs_prop_[y_id]) - 1];
//		cl_v_copy_pm(&x, &vs_prop_[x_id] TTL_CTR_V);
//
//		cl_v_del_all_except_val_n(&changed, &x, current_cs->constant_val TTL_CTR_V);
//		// if X[i] doesn't contain k
//		if (V_IS_EMPTY(x)) {
//			cl_v_bool_del_val_m(&vs_prop_[current_cs->reif_var_id], 1 TTL_CTR_V);
//			v_add_to_prop(vs_id_to_prop_, vs_prop_, convert_int(current_cs->reif_var_id));
//			return;
//		}
//
//		// constraint already fixed
//		if (V_N_VALS(vs_prop_[x_id]) == 1) {
//			cl_v_bool_del_val_m(&vs_prop_[current_cs->reif_var_id], 0 TTL_CTR_V);
//			v_add_to_prop(vs_id_to_prop_, vs_prop_, convert_int(current_cs->reif_var_id));
//		}
//	}
//}
//
///*
// * Propagate the domain of the variable with the ID prop_v_id through all the other variables on the same c_numb ID element opposite constraint
// * 1 ≤ y <= n ∧ X[y] != k
// * vs_per_c_idx - vector with all constrained variables ID per constraint, per constraint ID order
// * vs_prop_ - all CSP variables with current step values
// * prop_v_id - variable ID to propagate
// * current_cs - constraint that should be propagated for the variable with prop_v_id ID
// * vs_id_to_prop_ - circular vector with the ids of the variables to propagate
// */
//CUDA_FUNC void element_prop_opposite(CL_INTS_MEM int* vs_per_c_idx, CL_MEMORY VARS_PROP* vs_prop_, unsigned int prop_v_id, CL_CS_MEM cl_constr* current_cs, CL_MEMORY unsigned short* vs_id_to_prop_,
//		bool* prop_ok CS_IGNORE_FUNC TTL_CTR) {
//
//	int y_id = vs_per_c_idx[current_cs->n_c_vs - 1];	// ID of the variable whose domain are the index of the variables in elements vector
//	int x_id;
//	bool changed = 0;
//
//	// if y is singleton and x doesn't contain k is inconsistent
//	if (prop_v_id == (unsigned int)y_id && V_N_VALS(vs_prop_[y_id]) == 1) {
//
//		x_id = vs_per_c_idx[V_MIN(vs_prop_[y_id]) - 1];
//
//		cl_v_del_val_m(&changed, &vs_prop_[x_id], current_cs->constant_val TTL_CTR_V);
//		if (changed) {
//
//			// if X[i] doesn't contain k
//			if (V_IS_EMPTY(vs_prop_[x_id])) {
//				*prop_ok = 0;
//				return;
//			}
//			v_add_to_prop(vs_id_to_prop_, vs_prop_, x_id);
//		}
//#if CL_CS_IGNORE
//		cs_ignore[current_cs->c_id] = 1;
//#endif
//	}
//}
//
//#endif
//
//CUDA_FUNC void element_propagate(CL_INTS_MEM int* vs_per_c_idx, CL_MEMORY VARS_PROP* vs_prop_, unsigned int prop_v_id, CL_CS_MEM cl_constr* current_cs, CL_MEMORY unsigned short* vs_id_to_prop_,
//		bool* prop_ok PROPAGATED_FUNC CS_IGNORE_FUNC TTL_CTR) {
//
//#if CS_R_ELEMENT == 0
//	element_prop(vs_per_c_idx, vs_prop_, prop_v_id, current_cs, vs_id_to_prop_, prop_ok CS_IGNORE_CALL TTL_CTR_V);
//#if CL_STATS == 1
//	*propagated = true;
//#endif
//#elif CS_R_ELEMENT == 1
//	if (current_cs->reified == 1) {
//		if (prop_v_id != current_cs->reif_var_id) {
//			if (V_N_VALS(vs_prop_[current_cs->reif_var_id]) > 1) {
//				element_reif(vs_per_c_idx, vs_prop_, prop_v_id, current_cs, vs_id_to_prop_ TTL_CTR_V);
//			}
//			if (V_N_VALS(vs_prop_[current_cs->reif_var_id]) == 1) {
//				if (V_MIN(vs_prop_[current_cs->reif_var_id]) == 1) {
//					element_prop(vs_per_c_idx, vs_prop_, prop_v_id, current_cs, vs_id_to_prop_, prop_ok CS_IGNORE_CALL TTL_CTR_V);
//				} else {
//					element_prop_opposite(vs_per_c_idx, vs_prop_, prop_v_id, current_cs, vs_id_to_prop_, prop_ok CS_IGNORE_CALL TTL_CTR_V);
//				}
//#if CL_STATS == 1
//				*propagated = true;
//#endif
//			}
//		}
//	} else {
//		element_prop(vs_per_c_idx, vs_prop_, prop_v_id, current_cs, vs_id_to_prop_, prop_ok CS_IGNORE_CALL TTL_CTR_V);
//#if CL_STATS == 1
//		*propagated = true;
//#endif
//	}
//#endif
//}
//
//#endif
//

#if CS_ELEMENT == 1
/*
 * Propagate the domain of the variable with the ID prop_v_id through all the other variables on the same c_numb ID element constraint
 * 1 ≤ y <= n ∧ X[y] = k
 * prop_ok will be set to 1 if success or to 0 if any domain became empty
 * vs_per_c_idx - vector with all constrained variables ID per constraint, per constraint ID order
 * vs_prop_ - all CSP variables with current step values
 * prop_v_id - variable ID to propagate
 * current_cs - constraint that should be propagated for the variable with prop_v_id ID
 * vs_id_to_prop_ - circular vector with the ids of the variables to propagate
 */
CUDA_FUNC void element_prop(CL_INTS_MEM int* vs_per_c_idx, CL_MEMORY VARS_PROP* vs_prop_, unsigned int prop_v_id, CL_CS_MEM cl_constr* current_cs, CL_MEMORY unsigned short* vs_id_to_prop_,
		bool* prop_ok CS_IGNORE_FUNC TTL_CTR) {

	int y_id = vs_per_c_idx[current_cs->n_c_vs - 1];	// ID of the variable whose domain are the index of the variables in elements vector
	int k = current_cs->constant_val;
	int x_id;
	bool contains;
	bool changed = 0;
	int i;

	// if y is singleton
	if (V_N_VALS(vs_prop_[y_id]) == 1) {
		x_id = vs_per_c_idx[V_MIN(vs_prop_[y_id]) - 1];

		cl_v_del_all_except_val_m(&changed, &vs_prop_[x_id], k TTL_CTR_V);
		if (changed) {

			// if X[i] doesn't contain k
			if (V_IS_EMPTY(vs_prop_[x_id])) {
				*prop_ok = 0;
				return;
			}
			v_add_to_prop(vs_id_to_prop_, vs_prop_, x_id);
		}
#if CL_CS_IGNORE
		cs_ignore[current_cs->c_id] = 1;
#endif
		return;
	}

	// if y is not singleton and an x is to be propagated
	if (prop_v_id != (unsigned int)y_id) {

		cl_v_contains_val_m(&contains, &vs_prop_[prop_v_id], k TTL_CTR_V);
		if (!contains) {
			for (i = V_MIN(vs_prop_[y_id]); i <= V_MAX(vs_prop_[y_id]); i++) {
				CHECK_TTL(ttl_ctr, 53)

				if ((unsigned int)vs_per_c_idx[i - 1] == prop_v_id) {

					cl_v_del_val_m(&changed, &vs_prop_[y_id], i TTL_CTR_V);
					if (changed) {

						if (V_IS_EMPTY(vs_prop_[y_id])) {
							*prop_ok = 0;
							return;
						}

						// if y was set singleton
						if (V_N_VALS(vs_prop_[y_id]) == 1) {

							x_id = vs_per_c_idx[V_MIN(vs_prop_[y_id]) - 1];
							cl_v_del_all_except_val_m(&changed, &vs_prop_[x_id], k TTL_CTR_V);
							if (changed) {

								// if X[i] doesn't contain k
								if (V_IS_EMPTY(vs_prop_[x_id])) {
									*prop_ok = 0;
									return;
								}
								v_add_to_prop(vs_id_to_prop_, vs_prop_, x_id);
							}
#if CL_CS_IGNORE
							cs_ignore[current_cs->c_id] = 1;
#endif
						}
						v_add_to_prop(vs_id_to_prop_, vs_prop_, y_id);
					}
					return;
				}
			}
		}
	}
}

#if CS_R_ELEMENT == 1
/*
 * Validate element constraint to be normally propagated, when reified
 * 1 ≤ y <= n ∧ X[y] = k
 * vs_per_c_idx - vector with all constrained variables ID per constraint, per constraint ID order
 * vs_prop_ - all CSP variables with current step values
 * current_cs - constraint that should be propagated for the variable with prop_v_id ID
 * vs_id_to_prop_ - circular vector with the ids of the variables to propagate
 */
CUDA_FUNC void element_reif( CL_INTS_MEM int* vs_per_c_idx, CL_MEMORY VARS_PROP* vs_prop_, unsigned int prop_v_id, CL_CS_MEM cl_constr* current_cs, CL_MEMORY unsigned short* vs_id_to_prop_ TTL_CTR) {

	int y_id = vs_per_c_idx[current_cs->n_c_vs - 1];	// ID of the variable whose domain are the index of the variables in elements vector
	VARS_PROP y;
	int x_id;
	VARS_PROP x;
	bool contains;
	bool changed = 0;
	int i;

	// if y is singleton and x doesn't contain k is inconsistent
	if (prop_v_id == (unsigned int)y_id && V_N_VALS(vs_prop_[y_id]) == 1) {

		x_id = vs_per_c_idx[V_MIN(vs_prop_[y_id]) - 1];
		cl_v_copy_pm(&x, &vs_prop_[x_id] TTL_CTR_V);

		cl_v_del_all_except_val_n(&changed, &x, current_cs->constant_val TTL_CTR_V);

		// if X[i] doesn't contain k
		if (V_IS_EMPTY(x)) {
			cl_v_bool_del_val_m(&vs_prop_[current_cs->reif_var_id], 1 TTL_CTR_V);
			v_add_to_prop(vs_id_to_prop_, vs_prop_, convert_int(current_cs->reif_var_id));
		}

		// constraint already fixed
		if (V_N_VALS(vs_prop_[x_id]) == 1) {
			cl_v_bool_del_val_m(&vs_prop_[current_cs->reif_var_id], 0 TTL_CTR_V);
			v_add_to_prop(vs_id_to_prop_, vs_prop_, convert_int(current_cs->reif_var_id));
		}
		return;
	}

	// remove x from y if x doesn't contain k
	for (i = V_MIN(vs_prop_[y_id]); i <= V_MAX(vs_prop_[y_id]); i++) {
		CHECK_TTL(ttl_ctr, 210)
		x_id = vs_per_c_idx[i - 1];
		if ((unsigned int)x_id == prop_v_id) {

			cl_v_contains_val_m(&contains, &vs_prop_[x_id], current_cs->constant_val TTL_CTR_V);
			if (!contains) {
				cl_v_copy_pm(&y, &vs_prop_[y_id] TTL_CTR_V);

				cl_v_del_val_n(&changed, &y, i TTL_CTR_V);
				if (V_IS_EMPTY(y)) {
					cl_v_bool_del_val_m(&vs_prop_[current_cs->reif_var_id], 1 TTL_CTR_V);
					v_add_to_prop(vs_id_to_prop_, vs_prop_, convert_int(current_cs->reif_var_id));
					return;
				}
			}
			break;
		}
	}

	// if y is singleton and x doesn't contain k is inconsistent
	if (V_N_VALS(vs_prop_[y_id]) == 1) {

		x_id = vs_per_c_idx[V_MIN(vs_prop_[y_id]) - 1];
		cl_v_copy_pm(&x, &vs_prop_[x_id] TTL_CTR_V);

		cl_v_del_all_except_val_n(&changed, &x, current_cs->constant_val TTL_CTR_V);
		// if X[i] doesn't contain k
		if (V_IS_EMPTY(x)) {
			cl_v_bool_del_val_m(&vs_prop_[current_cs->reif_var_id], 1 TTL_CTR_V);
			v_add_to_prop(vs_id_to_prop_, vs_prop_, convert_int(current_cs->reif_var_id));
			return;
		}

		// constraint already fixed
		if (V_N_VALS(vs_prop_[x_id]) == 1) {
			cl_v_bool_del_val_m(&vs_prop_[current_cs->reif_var_id], 0 TTL_CTR_V);
			v_add_to_prop(vs_id_to_prop_, vs_prop_, convert_int(current_cs->reif_var_id));
		}
	}
}

/*
 * Propagate the domain of the variable with the ID prop_v_id through all the other variables on the same c_numb ID element opposite constraint
 * 1 ≤ y <= n ∧ X[y] != k
 * vs_per_c_idx - vector with all constrained variables ID per constraint, per constraint ID order
 * vs_prop_ - all CSP variables with current step values
 * prop_v_id - variable ID to propagate
 * current_cs - constraint that should be propagated for the variable with prop_v_id ID
 * vs_id_to_prop_ - circular vector with the ids of the variables to propagate
 */
CUDA_FUNC void element_prop_opposite(CL_INTS_MEM int* vs_per_c_idx, CL_MEMORY VARS_PROP* vs_prop_, unsigned int prop_v_id, CL_CS_MEM cl_constr* current_cs, CL_MEMORY unsigned short* vs_id_to_prop_,
		bool* prop_ok CS_IGNORE_FUNC TTL_CTR) {

	int y_id = vs_per_c_idx[current_cs->n_c_vs - 1];	// ID of the variable whose domain are the index of the variables in elements vector
	int x_id;
	bool changed = 0;

	// if y is singleton and x doesn't contain k is inconsistent
	if (prop_v_id == (unsigned int)y_id && V_N_VALS(vs_prop_[y_id]) == 1) {

		x_id = vs_per_c_idx[V_MIN(vs_prop_[y_id]) - 1];

		cl_v_del_val_m(&changed, &vs_prop_[x_id], current_cs->constant_val TTL_CTR_V);
		if (changed) {

			// if X[i] doesn't contain k
			if (V_IS_EMPTY(vs_prop_[x_id])) {
				*prop_ok = 0;
				return;
			}
			v_add_to_prop(vs_id_to_prop_, vs_prop_, x_id);
		}
#if CL_CS_IGNORE
		cs_ignore[current_cs->c_id] = 1;
#endif
	}
}

#endif

CUDA_FUNC void element_propagate(CL_INTS_MEM int* vs_per_c_idx, CL_MEMORY VARS_PROP* vs_prop_, unsigned int prop_v_id, CL_CS_MEM cl_constr* current_cs, CL_MEMORY unsigned short* vs_id_to_prop_,
		bool* prop_ok PROPAGATED_FUNC CS_IGNORE_FUNC TTL_CTR) {

#if CS_R_ELEMENT == 0
	element_prop(vs_per_c_idx, vs_prop_, prop_v_id, current_cs, vs_id_to_prop_, prop_ok CS_IGNORE_CALL TTL_CTR_V);
#if CL_STATS == 1
	*propagated = true;
#endif
#elif CS_R_ELEMENT == 1
	if (current_cs->reified == 1) {
		if (prop_v_id != current_cs->reif_var_id) {
			if (V_N_VALS(vs_prop_[current_cs->reif_var_id]) > 1) {
				element_reif(vs_per_c_idx, vs_prop_, prop_v_id, current_cs, vs_id_to_prop_ TTL_CTR_V);
			}
			if (V_N_VALS(vs_prop_[current_cs->reif_var_id]) == 1) {
				if (V_MIN(vs_prop_[current_cs->reif_var_id]) == 1) {
					element_prop(vs_per_c_idx, vs_prop_, prop_v_id, current_cs, vs_id_to_prop_, prop_ok CS_IGNORE_CALL TTL_CTR_V);
				} else {
					element_prop_opposite(vs_per_c_idx, vs_prop_, prop_v_id, current_cs, vs_id_to_prop_, prop_ok CS_IGNORE_CALL TTL_CTR_V);
				}
#if CL_STATS == 1
				*propagated = true;
#endif
			}
		}
	} else {
		element_prop(vs_per_c_idx, vs_prop_, prop_v_id, current_cs, vs_id_to_prop_, prop_ok CS_IGNORE_CALL TTL_CTR_V);
#if CL_STATS == 1
		*propagated = true;
#endif
	}
#endif
}

#endif