/*
 * linear_var.c
 *
 *  Created on: 07/12/2016
 *      Author: pedro
 */

#ifndef __OPENCL_VERSION__

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

#include "linear_var.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 linear_var type and return the constraint ID
 *  K · Y = z
 * K - constant unsigned integers for this constraint
 * Y_ids - IDs of the variables constrained by this constraint
 * n - number of constants (or variables)
 * z_id - ID of variable z
 */
unsigned int c_linear_var(int* K, unsigned int* Y_ids, unsigned int n, unsigned int z_id) {
	unsigned int i;

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

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

	for (i = 0; i < n; i++) {
		c_vs[i] = Y_ids[i];
	}
	c_vs[n] = z_id;

	// creates a new generic constraint
	unsigned int c_id = c_new(c_vs, n + 1, K, n, -1);

	// pointers to this type of constraint functions
	CS[c_id].kind = LINEAR_VAR;
	CS[c_id].check_sol_f = &linear_var_check;
	CS[c_id].constant_val = 0;

	free(c_vs);

	return c_id;
}

/*
 * Creates a new reified constraint of the linear_var type and return the constraint ID
 *  K · Y = z
 * K - constant unsigned integers for this constraint
 * Y_ids - IDs of the variables constrained by this constraint
 * n - number of constants (or variables)
 * z_id - ID of variable z
 * reif_v_id - ID of the reification variable
 */
unsigned int c_linear_var_reif(int* K, unsigned int* Y_ids, unsigned int n, unsigned int z_id, int reif_v_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 LINEAR_VAR_REIF makes model inconsistent at creation:\n");
			exit(-1);
		}
	}

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

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

	for (i = 0; i < n; i++) {
		c_vs[i] = Y_ids[i];
	}
	c_vs[n] = z_id;

	// creates a new generic constraint
	unsigned int c_id = c_new(c_vs, n + 1, K, n, reif_v_id);

	// pointers to this type of constraint functions
	CS[c_id].kind = LINEAR_VAR;
	CS[c_id].check_sol_f = &linear_var_check;
	CS[c_id].constant_val = 0;

	free(c_vs);

	return c_id;
}

/*
 * Return true if the linear_var constraint is respected or false if not
 *  K · Y = z
 * 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 linear_var_check(constr* c, bool explored) {
	unsigned int n = c->n_c_consts;		// number of constants and variables constrained by this constraint
	int* K = c->c_consts;	// constants constrained by this constraint
	var** Y = c->c_vs;	// variables constrained by this constraint
	var* z = c->c_vs[n];	// variable that should contain all the values resultant from the equations
	unsigned int equat_result = 0;
	bitmap d;
	unsigned int i;

	// if variable z has more than one value or is empty
#if CHECK_SOL_N_VALS
	if (z->to_label && z->n_vals != 1) {

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

			for (i = 0; i < c->n_c_vs; i++) {
				fprintf(stderr, "Variable ID=%u -> minimum=%u, maximum=%u, number of values=%u\n\n", c->c_vs[i]->v_id, b_get_min_val(&c->c_vs[i]->domain_b),
						b_get_max_val(&c->c_vs[i]->domain_b), b_cnt_vals(&c->c_vs[i]->domain_b));
			}
		}
		return false;
	}
#endif

	// if any other variable has more than one value or is empty
#if CHECK_SOL_N_VALS
	for (i = 0; i < n; i++) {
		if (Y[i]->to_label && Y[i]->n_vals != 1) {

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

				for (i = 0; i < c->n_c_vs; i++) {
					fprintf(stderr, "Variable ID=%u -> minimum=%u, maximum=%u, number of values=%u\n\n", c->c_vs[i]->v_id, b_get_min_val(&c->c_vs[i]->domain_b),
							b_get_max_val(&c->c_vs[i]->domain_b), b_cnt_vals(&c->c_vs[i]->domain_b));
				}
			}
			return false;
		}
	}
#endif

	for (i = 0; i < n; i++) {
		equat_result += (unsigned int)K[i] * Y[i]->min;
	}

	b_new_vals(&d, &equat_result, 1);

	if (!bs_eq(&z->domain_b, &d)) {

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

			for (i = 0; i < c->n_c_vs; i++) {
				fprintf(stderr, "Variable ID=%u -> minimum=%u, maximum=%u, number of values=%u\n\n", c->c_vs[i]->v_id, b_get_min_val(&c->c_vs[i]->domain_b),
						b_get_max_val(&c->c_vs[i]->domain_b), b_cnt_vals(&c->c_vs[i]->domain_b));
			}
		}
		return false;
	}

	return true;
}

#endif

#if CS_LINEAR_VAR == 1
/*
 * Propagate the domain of the variable with the ID prop_v_id through all the other variables on the same c_numb ID linear_var constraint
 *  K · Y = z
 * 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
 * c_consts - vector with all constrained constants 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 linear_var_prop(CL_INTS_MEM int* vs_per_c_idx, CL_INTS_MEM int* c_consts, CL_MEMORY VARS_PROP* vs_prop_, CL_CS_MEM cl_constr* current_cs,
		CL_MEMORY unsigned short* vs_id_to_prop_, bool* prop_ok, __global int* terms_mem CS_IGNORE_FUNC TTL_CTR) {

	int terms = current_cs->n_c_consts;	// number of constants and variables constrained by this constraint
	CL_INTS_MEM int* K = c_consts;	// constants constrained by this constraint
	int z_id = vs_per_c_idx[terms];	// variable that should contain all the values resultant from the equations
	int y_id;
	__global int* mins = terms_mem;
	__global int* maxs = &terms_mem[current_cs->n_c_consts];
	int lb, ub;
	int vl, vh;
	int min, max;
	int xmin, xmax;
	bool changed = 0;
	bool changed1 = 0;
	int c;
	int i;

	min = 0;
	max = 0;
	for (i = 0; i < terms; ++i) {
		CHECK_TTL(ttl_ctr, 23)

		y_id = vs_per_c_idx[i];
		if (K[i] > 0) {
			vl = mins[i] = V_MIN(vs_prop_[y_id]);
			vh = maxs[i] = V_MAX(vs_prop_[y_id]);
		} else {
			vl = maxs[i] = V_MAX(vs_prop_[y_id]);
			vh = mins[i] = V_MIN(vs_prop_[y_id]);
		}

		min += K[i] * vl;
		max += K[i] * vh;
	}

	lb = V_MIN(vs_prop_[z_id]);
	ub = V_MAX(vs_prop_[z_id]);
	if (min > ub || max < lb) {
		*prop_ok = 0;

	} else {

		if (min > lb) {
			cl_v_del_lt_m(&changed1, &vs_prop_[z_id], min TTL_CTR_V);
		} else if (max < ub) {
			cl_v_del_gt_m(&changed, &vs_prop_[z_id], max TTL_CTR_V);
		}

		if (changed1 || changed) {

			if (V_IS_EMPTY(vs_prop_[z_id])) {
				*prop_ok = 0;

			} else {
				v_add_to_prop(vs_id_to_prop_, vs_prop_, z_id);

				lb = V_MIN(vs_prop_[z_id]);
				ub = V_MAX(vs_prop_[z_id]);
			}
		}

		if (*prop_ok != 0 && min != max) {

			// poor man's propagation
			if (min == ub) {
				for (i = 0; i < terms; ++i) {
					CHECK_TTL(ttl_ctr, 24)

					y_id = vs_per_c_idx[i];
					c = K[i];

					if (V_N_VALS(vs_prop_[y_id]) > 1) {
						if (c != 0 && mins[i] != maxs[i]) {
							if (c > 0) {

								cl_v_del_gt_m(&changed, &vs_prop_[y_id], mins[i] TTL_CTR_V);
								if (changed) {
									if (V_IS_EMPTY(vs_prop_[y_id])) {
										*prop_ok = 0;

									} else {
										v_add_to_prop(vs_id_to_prop_, vs_prop_, y_id);
									}
								}
							} else {

								cl_v_del_lt_m(&changed, &vs_prop_[y_id], maxs[i] TTL_CTR_V);
								if (changed) {
									if (V_IS_EMPTY(vs_prop_[y_id])) {
										*prop_ok = 0;

									} else {
										v_add_to_prop(vs_id_to_prop_, vs_prop_, y_id);
									}
								}
							}
						}
					}
				}
				if (V_N_VALS(vs_prop_[z_id]) > 1) {
					cl_v_del_all_except_val_m(&changed, &vs_prop_[z_id], ub TTL_CTR_V);
					v_add_to_prop(vs_id_to_prop_, vs_prop_, z_id);
				}

#if CL_CS_IGNORE
				cs_ignore[current_cs->c_id] = 1;
#endif

			} else if (max == lb) {
				for (i = 0; i < terms; ++i) {
					CHECK_TTL(ttl_ctr, 25)

					y_id = vs_per_c_idx[i];
					c = K[i];
					if (V_N_VALS(vs_prop_[y_id]) > 1) {
						if (c != 0 && mins[i] != maxs[i]) {
							if (c > 0) {

								cl_v_del_lt_m(&changed, &vs_prop_[y_id], maxs[i] TTL_CTR_V);
								if (changed) {
									if (V_IS_EMPTY(vs_prop_[y_id])) {
										*prop_ok = 0;

									} else {
										v_add_to_prop(vs_id_to_prop_, vs_prop_, y_id);
									}
								}
							} else {

								cl_v_del_gt_m(&changed, &vs_prop_[y_id], mins[i] TTL_CTR_V);
								if (changed) {
									if (V_IS_EMPTY(vs_prop_[y_id])) {
										*prop_ok = 0;

									} else {
										v_add_to_prop(vs_id_to_prop_, vs_prop_, y_id);
									}
								}
							}
						}
					}
				}
				if (V_N_VALS(vs_prop_[z_id]) > 1) {
					cl_v_del_all_except_val_m(&changed, &vs_prop_[z_id], lb TTL_CTR_V);
					v_add_to_prop(vs_id_to_prop_, vs_prop_, z_id);
				}

#if CL_CS_IGNORE
				cs_ignore[current_cs->c_id] = 1;
#endif
			} else if (max > ub) {
				for (i = 0; i < terms; ++i) {
					CHECK_TTL(ttl_ctr, 26)

					y_id = vs_per_c_idx[i];
					c = K[i];
					xmin = mins[i];
					xmax = maxs[i];

					if (V_N_VALS(vs_prop_[y_id]) > 1) {
						if (c > 0) {
							if ((xmax - xmin) * c > ub - min) {
								xmax = (ub - min) / c + xmin;

								cl_v_del_gt_m(&changed, &vs_prop_[y_id], xmax TTL_CTR_V);
								if (changed) {
									if (V_IS_EMPTY(vs_prop_[y_id])) {
										*prop_ok = 0;

									} else {
										v_add_to_prop(vs_id_to_prop_, vs_prop_, y_id);
									}
								}
							}
						} else if (c < 0) {
							if ((xmin - xmax) * c > ub - min) {
								xmin = convert_int(ceil((ub - min * 1.0) / c + xmax));

								cl_v_del_lt_m(&changed, &vs_prop_[y_id], xmin TTL_CTR_V);
								if (changed) {
									if (V_IS_EMPTY(vs_prop_[y_id])) {
										*prop_ok = 0;

									} else {
										v_add_to_prop(vs_id_to_prop_, vs_prop_, y_id);
									}
								}
							}
						}
					}
				}

			} else	if (min < lb) {
				for (i = 0; i < terms; ++i) {
					CHECK_TTL(ttl_ctr, 27)

					y_id = vs_per_c_idx[i];
					c = K[i];
					xmin = mins[i];
					xmax = maxs[i];

					if (V_N_VALS(vs_prop_[y_id]) > 1) {
						if (c > 0) {
							if ((xmax - xmin) * c > max - lb) {
								xmin = convert_int(ceil((lb - max * 1.0) / c + xmax));

								cl_v_del_lt_m(&changed, &vs_prop_[y_id], xmin TTL_CTR_V);
								if (changed) {
									if (V_IS_EMPTY(vs_prop_[y_id])) {
										*prop_ok = 0;

									} else {
										v_add_to_prop(vs_id_to_prop_, vs_prop_, y_id);
									}
								}
							}
						}
						if (c < 0) {
							if ((xmax - xmin) * c < lb - max) {
								xmax = (lb - max) / c + xmin;

								cl_v_del_gt_m(&changed, &vs_prop_[y_id], xmax TTL_CTR_V);
								if (changed) {
									if (V_IS_EMPTY(vs_prop_[y_id])) {
										*prop_ok = 0;

									} else {
										v_add_to_prop(vs_id_to_prop_, vs_prop_, y_id);
									}
								}
							}
						}
					}
				}
			}
		}
	}
}

#if CS_R_LINEAR_VAR == 1
/*
 * Validate linear_var constraint to be normally propagated, when reified
 *  K · Y = z
 * 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 linear_var_reif( CL_INTS_MEM int* vs_per_c_idx, CL_INTS_MEM int* c_consts, CL_MEMORY VARS_PROP* vs_prop_, CL_CS_MEM cl_constr* current_cs,
		CL_MEMORY unsigned short* vs_id_to_prop_, __global int* terms_mem CS_IGNORE_FUNC TTL_CTR) {

	int terms = current_cs->n_c_consts;	// number of constants and variables constrained by this constraint
	CL_INTS_MEM int* K = c_consts;	// constants constrained by this constraint
	int z_id = vs_per_c_idx[terms];	// variable that should contain all the values resultant from the equations
	VARS_PROP z;
	int y_id;
	VARS_PROP y;
	__global int* mins = terms_mem;
	__global int* maxs = &terms_mem[current_cs->n_c_consts];
	int lb, ub;
	int vl, vh;
	int min, max;
	int xmin, xmax;
	int c;
	bool changed = 0;
	bool changed1 = 0;
	int i;

	min = 0;
	max = 0;
	for (i = 0; i < terms; ++i) {
		CHECK_TTL(ttl_ctr, 79)
		y_id = vs_per_c_idx[i];
		if (K[i] > 0) {
			vl = mins[i] = V_MIN(vs_prop_[y_id]);
			vh = maxs[i] = V_MAX(vs_prop_[y_id]);
		} else {
			vl = maxs[i] = V_MAX(vs_prop_[y_id]);
			vh = mins[i] = V_MIN(vs_prop_[y_id]);
		}

		min += K[i] * vl;
		max += K[i] * vh;
	}

	lb = V_MIN(vs_prop_[z_id]);
	ub = V_MAX(vs_prop_[z_id]);
	if (min > ub || max < lb) {
		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));

#if CL_CS_IGNORE
		cs_ignore[current_cs->c_id] = 1;
#endif
		return;
	}

	cl_v_copy_pm(&z, &vs_prop_[z_id] TTL_CTR_V);

	if (min > lb) {
		cl_v_del_lt_n(&changed, &z, min TTL_CTR_V);
	} else if (max < ub) {
		cl_v_del_gt_n(&changed1, &z, max TTL_CTR_V);
	}

	if (changed || changed1) {

		if (V_IS_EMPTY(z)) {
			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;
		}

		lb = V_MIN(z);
		ub = V_MAX(z);
	}

	// constraint already fixed
	if (min == max) {
		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));

#if CL_CS_IGNORE
		cs_ignore[current_cs->c_id] = 1;
#endif
		return;
	}

	// poor man's propagation
	if (min == ub) {
		for (i = 0; i < terms; ++i) {
			CHECK_TTL(ttl_ctr, 80)
			y_id = vs_per_c_idx[i];
			cl_v_copy_pm(&y, &vs_prop_[y_id] TTL_CTR_V);
			c = K[i];

			if (V_N_VALS(vs_prop_[y_id]) > 1) {
				if (c != 0 && mins[i] != maxs[i]) {
					if (c > 0) {
						cl_v_del_gt_n(&changed, &y, mins[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;
						}
					} else {
						cl_v_del_lt_n(&changed, &y, maxs[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;
						}
					}
				}
			}
		}
		return;
	}

	if (max == lb) {
		for (i = 0; i < terms; ++i) {
			CHECK_TTL(ttl_ctr, 81)
			y_id = vs_per_c_idx[i];
			cl_v_copy_pm(&y, &vs_prop_[y_id] TTL_CTR_V);
			c = K[i];

			if (V_N_VALS(vs_prop_[y_id]) > 1) {
				if (c != 0 && mins[i] != maxs[i]) {
					if (c > 0) {
						cl_v_del_lt_n(&changed, &y, maxs[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;
						}
					} else {
						cl_v_del_gt_n(&changed, &y, mins[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;
						}
					}
				}
			}
		}
		return;
	}

	if (max > ub) {
		for (i = 0; i < terms; ++i) {
			CHECK_TTL(ttl_ctr, 82)
			y_id = vs_per_c_idx[i];
			cl_v_copy_pm(&y, &vs_prop_[y_id] TTL_CTR_V);
			c = K[i];
			xmin = mins[i];
			xmax = maxs[i];

			if (V_N_VALS(vs_prop_[y_id]) > 1) {
				if (c > 0) {
					if ((xmax - xmin) * c > ub - min) {
						xmax = (ub - min) / c + xmin;

						cl_v_del_gt_n(&changed, &y, xmax 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;
						}
					}
				}
				if (c < 0) {
					if ((xmin - xmax) * c > ub - min) {
						xmin = convert_int(ceil((ub - min * 1.0) / c + xmax));

						cl_v_del_lt_n(&changed, &y, xmin 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;
						}
					}
				}
			}
		}
	}

	if (min < lb) {
		for (i = 0; i < terms; ++i) {
			CHECK_TTL(ttl_ctr, 83)
			y_id = vs_per_c_idx[i];
			cl_v_copy_pm(&y, &vs_prop_[y_id] TTL_CTR_V);
			c = K[i];
			xmin = mins[i];
			xmax = maxs[i];

			if (V_N_VALS(vs_prop_[y_id]) > 1) {
				if (c > 0) {
					if ((xmax - xmin) * c > max - lb) {
						xmin = convert_int(ceil((lb - max * 1.0) / c + xmax));

						cl_v_del_lt_n(&changed, &y, xmin 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;
						}
					}
				}
				if (c < 0) {
					if ((xmax - xmin) * c < lb - max) {
						xmax = (lb - max) / c + xmin;

						cl_v_del_gt_n(&changed, &y, xmax 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;
						}
					}
				}
			}
		}
	}
}


/*
 * Propagate the domain of the variable with the ID prop_v_id through all the other variables on the same c_numb ID linear_var opposite constraint
 *  K · Y != z
 * vs_per_c_idx - vector with all constrained variables ID per constraint, per constraint ID order
 * c_consts - vector with all constrained constants 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 linear_var_prop_opposite(CL_INTS_MEM int* vs_per_c_idx, CL_INTS_MEM int* c_consts, CL_MEMORY VARS_PROP* vs_prop_, CL_CS_MEM cl_constr* current_cs,
		CL_MEMORY unsigned short* vs_id_to_prop_, bool* prop_ok, __global int* terms_mem CS_IGNORE_FUNC TTL_CTR) {

	int terms = current_cs->n_c_consts;	// number of constants and variables constrained by this constraint
	CL_INTS_MEM int* K = c_consts;	// constants constrained by this constraint
	int z_id = vs_per_c_idx[terms];	// variable that should contain all the values resultant from the equations
	int equat_result;
	int y_id;
	__global int* mins = terms_mem;
	int vl, vh;
	int min, max;
	bool changed = 0;
	int not_singl = 0;
	int not_singl_idx;
	int not_singl_id = -1;
	int val_to_rem;
	int sum = 0;
	int i;

	if (V_N_VALS(vs_prop_[z_id]) > 1) {
		return;
	}
	equat_result = V_MIN(vs_prop_[z_id]);

	min = 0;
	max = 0;
	for (i = 0; i < terms; ++i) {
		CHECK_TTL(ttl_ctr, 69)
		y_id = vs_per_c_idx[i];
		if (K[i] > 0) {
			vl = mins[i] = V_MIN(vs_prop_[y_id]);
			vh = V_MAX(vs_prop_[y_id]);
		} else {
			vl = V_MAX(vs_prop_[y_id]);
			vh = mins[i] = V_MIN(vs_prop_[y_id]);
		}

		if (vl != vh) {
			not_singl_idx = i;
			not_singl_id = y_id;
			not_singl++;
		} else {
			sum += K[i] * mins[i];
		}

		min += K[i] * vl;
		max += K[i] * vh;
	}
	sum -= equat_result;

	if (min > equat_result || max < equat_result) {

#if CL_CS_IGNORE
		cs_ignore[current_cs->c_id] = 1;
#endif
		return;
	}

	if (min == max && min == equat_result) {
		*prop_ok = 0;
		return;
	}

	// if all but one variable are already singleton, remove the only value from the one that is not singleton that would lead to equality
	if (not_singl == 1) {
		val_to_rem = (-1) * (sum / K[not_singl_idx]);

		if (sum % K[not_singl_idx] > 0 || val_to_rem < 0) {
			*prop_ok = 0;
			return;
		}

		cl_v_del_val_m(&changed, &vs_prop_[not_singl_id], val_to_rem TTL_CTR_V);

		if (changed) {
			if (V_IS_EMPTY(vs_prop_[not_singl_id])) {
				*prop_ok = 0;
				return;
			}
			v_add_to_prop(vs_id_to_prop_, vs_prop_, not_singl_id);
		}

#if CL_CS_IGNORE
		cs_ignore[current_cs->c_id] = 1;
#endif
	}
}

#endif

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

#if CS_R_LINEAR_VAR == 0
	linear_var_prop(vs_per_c_idx, c_consts, vs_prop_, current_cs, vs_id_to_prop_, prop_ok, terms_mem CS_IGNORE_CALL TTL_CTR_V);
#if CL_STATS == 1
	*propagated = true;
#endif
#elif CS_R_LINEAR_VAR == 1
	if (current_cs->reified == 1) {
		if (V_N_VALS(vs_prop_[current_cs->reif_var_id]) > 1) {
			linear_var_reif(vs_per_c_idx, c_consts, vs_prop_, current_cs, vs_id_to_prop_, terms_mem CS_IGNORE_CALL 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) {
				linear_var_prop(vs_per_c_idx, c_consts, vs_prop_, current_cs, vs_id_to_prop_, prop_ok, terms_mem CS_IGNORE_CALL TTL_CTR_V);
			} else {
				linear_var_prop_opposite(vs_per_c_idx, c_consts, vs_prop_, current_cs, vs_id_to_prop_, prop_ok, terms_mem CS_IGNORE_CALL TTL_CTR_V);
			}
#if CL_STATS == 1
			*propagated = true;
#endif
		}
	} else {
		linear_var_prop(vs_per_c_idx, c_consts, vs_prop_, current_cs, vs_id_to_prop_, prop_ok, terms_mem CS_IGNORE_CALL TTL_CTR_V);
#if CL_STATS == 1
		*propagated = true;
#endif
	}
#endif
}

#endif