/*
 * var_eq_minus_abs.c
 *
 *  Created on: 16/12/2014
 *      Author: pedro
 */

#ifndef __OPENCL_VERSION__

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

#include "var_eq_minus_abs.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 var_eq_minus_abs type and return the constraint ID
 * x = |y − z|
 * x_id - ID of variable x
 * y_id - ID of variable y
 * z_id - ID of variable z
 */
unsigned int c_var_eq_minus_abs(unsigned int x_id, unsigned int y_id, unsigned int z_id) {

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

	unsigned int c_vs[3];
	c_vs[0] = x_id;
	c_vs[1] = y_id;
	c_vs[2] = z_id;

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

	// variable to select from x = y − z or x = z − y
	unsigned int v_id = v_new_range(0, 1, false);

	// pointers to this type of constraint functions
	CS[c_id].kind = VAR_EQ_MINUS_ABS;
	CS[c_id].check_sol_f = &var_eq_minus_abs_check;
	CS[c_id].constant_val = (int)v_id;

	return c_id;
}

/*
 * Creates a new constraint of the var_eq_minus_abs type and return the constraint ID
 * x = |y − z|
 * x_id - ID of variable x
 * y_id - ID of variable y
 * z_id - ID of variable z
 * reif_v_id - ID of the reification variable
 */
unsigned int c_var_eq_minus_var_eq_minus_abs_reif(unsigned int x_id, unsigned int y_id, unsigned int z_id, int reif_v_id) {

	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 VAR_EQ_MINUS_ABS_REIF makes model inconsistent at creation:\n");
			exit(-1);
		}
	}

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

	unsigned int c_vs[3];
	c_vs[0] = x_id;
	c_vs[1] = y_id;
	c_vs[2] = z_id;

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

	// variable to select from x = y − z or x = z − y
	unsigned int v_id = v_new_range(0, 1, false);

	// pointers to this type of constraint functions
	CS[c_id].kind = VAR_EQ_MINUS_ABS;
	CS[c_id].check_sol_f = &var_eq_minus_abs_check;
	CS[c_id].constant_val = (int)v_id;

	return c_id;
}

/*
 * Return true if the var_eq_minus_abs constraint is respected or false if not
 * x = |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 var_eq_minus_abs_check(constr* c, bool explored) {

	// check if any variable inside same a_eq_b_minus_c constraint has domain 0, more than one value
	// or if the sum is not correct. If so, return false. Else return true.
	if (
#if CHECK_SOL_N_VALS
			(c->c_vs[0]->to_label && c->c_vs[0]->n_vals != 1) || (c->c_vs[1]->to_label && c->c_vs[1]->n_vals != 1) ||
			(c->c_vs[2]->to_label && c->c_vs[2]->n_vals != 1) || (VS[c->constant_val].to_label && VS[c->constant_val].n_vals != 1) ||
#endif
			((VS[c->constant_val].min == 0 && c->c_vs[0]->min != c->c_vs[1]->min - c->c_vs[2]->min)
			|| (VS[c->constant_val].min == 1 && c->c_vs[0]->min != c->c_vs[2]->min - c->c_vs[1]->min))) {

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

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

	return true;
}

#endif

#if CS_VAR_EQ_MINUS_ABS == 1
/*
 * Propagate the domain of the variable with the ID prop_v_id through all the other variables on the same c_numb ID var_eq_minus_abs constraint
 * x = |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
 * 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 var_eq_minus_abs_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 TTL_CTR) {

	int x_id = vs_per_c_idx[0];
	int y_id = vs_per_c_idx[1];
	int z_id = vs_per_c_idx[2];
	int v_id = current_cs->constant_val;	// variable used to flag the constraint (x = y − z or x = z − y) that should be propagated
	VARS_PROP x;
	VARS_PROP y;
	VARS_PROP z;
	bool changed;
	bool changed_x1;
	bool changed_y1;
	bool changed_z1;
	bool changed_x2;
	bool changed_y2;
	bool changed_z2;
	int i;

	// if no choice made, try to remove x = y − z
	if (V_N_VALS(vs_prop_[v_id]) == 2) {
		cl_v_copy_pm(&x, &vs_prop_[x_id] TTL_CTR_V);
		cl_v_copy_pm(&y, &vs_prop_[y_id] TTL_CTR_V);
		cl_v_copy_pm(&z, &vs_prop_[z_id] TTL_CTR_V);

		for (i = 0; i < 1; i++) {
			if (prop_v_id == (unsigned int)x_id) {

				cl_v_del_lt_n(&changed_y1, &y, V_MIN(x) + V_MIN(z) TTL_CTR_V);
				if (changed_y1) {
					if (V_IS_EMPTY(y)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
						break;
					}
				}
				cl_v_del_gt_n(&changed_y2, &y, V_MAX(x) + V_MAX(z) TTL_CTR_V);
				if (changed_y2) {
					if (V_IS_EMPTY(y)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
						break;
					}
				}
				cl_v_del_lt_n(&changed_z1, &z, V_MIN(y) - V_MAX(x) TTL_CTR_V);
				if (changed_z1) {
					if (V_IS_EMPTY(z)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
						break;
					}
				}
				cl_v_del_gt_n(&changed_z2, &z, V_MAX(y) - V_MIN(x) TTL_CTR_V);
				if (changed_z2) {
					if (V_IS_EMPTY(z)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
						break;
					}
				}
				break;
			}

			if (prop_v_id == (unsigned int)y_id) {
				cl_v_del_lt_n(&changed_x1, &x, V_MIN(y) - V_MAX(z) TTL_CTR_V);
				if (changed_x1) {
					if (V_IS_EMPTY(x)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
						break;
					}
				}
				cl_v_del_gt_n(&changed_x2, &x, V_MAX(y) - V_MIN(z) TTL_CTR_V);
				if (changed_x2) {
					if (V_IS_EMPTY(x)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
						break;
					}
				}
				cl_v_del_lt_n(&changed_z1, &z, V_MIN(y) - V_MAX(x) TTL_CTR_V);
				if (changed_z1) {
					if (V_IS_EMPTY(z)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
						break;
					}
				}
				cl_v_del_gt_n(&changed_z2, &z, V_MAX(y) - V_MIN(x) TTL_CTR_V);
				if (changed_z2) {
					if (V_IS_EMPTY(z)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
						break;
					}
				}
				break;
			}

			// prop_v_id == z_id
			cl_v_del_lt_n(&changed_x1, &x, V_MIN(y) - V_MAX(z) TTL_CTR_V);
			if (changed_x1) {
				if (V_IS_EMPTY(x)) {
					cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
					break;
				}
			}
			cl_v_del_gt_n(&changed_x2, &x, V_MAX(y) - V_MIN(z) TTL_CTR_V);
			if (changed_x2) {
				if (V_IS_EMPTY(x)) {
					cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
					break;
				}
			}
			cl_v_del_lt_n(&changed_y1, &y, V_MIN(x) + V_MIN(z) TTL_CTR_V);
			if (changed_y1) {
				if (V_IS_EMPTY(y)) {
					cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
					break;
				}
			}
			cl_v_del_gt_n(&changed_y2, &y, V_MAX(x) + V_MAX(z) TTL_CTR_V);
			if (changed_y2) {
				if (V_IS_EMPTY(y)) {
					cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
					break;
				}
			}
			break;
		}
	}

	// if no choice made yet, try to remove x = z − y
	if (V_N_VALS(vs_prop_[v_id]) == 2) {

		y_id = vs_per_c_idx[2];
		z_id = vs_per_c_idx[1];

		cl_v_copy_pm(&x, &vs_prop_[x_id] TTL_CTR_V);
		cl_v_copy_pm(&y, &vs_prop_[y_id] TTL_CTR_V);
		cl_v_copy_pm(&z, &vs_prop_[z_id] TTL_CTR_V);

		for (i = 0; i < 1; i++) {
			if (prop_v_id == (unsigned int)x_id) {

				cl_v_del_lt_n(&changed_y1, &y, V_MIN(x) + V_MIN(z) TTL_CTR_V);
				if (changed_y1) {
					if (V_IS_EMPTY(y)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
						break;
					}
				}
				cl_v_del_gt_n(&changed_y2, &y, V_MAX(x) + V_MAX(z) TTL_CTR_V);
				if (changed_y2) {
					if (V_IS_EMPTY(y)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
						break;
					}
				}
				cl_v_del_lt_n(&changed_z1, &z, V_MIN(y) - V_MAX(x) TTL_CTR_V);
				if (changed_z1) {
					if (V_IS_EMPTY(z)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
						break;
					}
				}
				cl_v_del_gt_n(&changed_z2, &z, V_MAX(y) - V_MIN(x) TTL_CTR_V);
				if (changed_z2) {
					if (V_IS_EMPTY(z)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
						break;
					}
				}
				break;
			}

			if (prop_v_id == (unsigned int)y_id) {
				cl_v_del_lt_n(&changed_x1, &x, V_MIN(y) - V_MAX(z) TTL_CTR_V);
				if (changed_x1) {
					if (V_IS_EMPTY(x)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
						break;
					}
				}
				cl_v_del_gt_n(&changed_x2, &x, V_MAX(y) - V_MIN(z) TTL_CTR_V);
				if (changed_x2) {
					if (V_IS_EMPTY(x)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
						break;
					}
				}
				cl_v_del_lt_n(&changed_z1, &z, V_MIN(y) - V_MAX(x) TTL_CTR_V);
				if (changed_z1) {
					if (V_IS_EMPTY(z)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
						break;
					}
				}
				cl_v_del_gt_n(&changed_z2, &z, V_MAX(y) - V_MIN(x) TTL_CTR_V);
				if (changed_z2) {
					if (V_IS_EMPTY(z)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
						break;
					}
				}
				break;
			}

			// prop_v_id == z_id
			cl_v_del_lt_n(&changed_x1, &x, V_MIN(y) - V_MAX(z) TTL_CTR_V);
			if (changed_x1) {
				if (V_IS_EMPTY(x)) {
					cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
					break;
				}
			}
			cl_v_del_gt_n(&changed_x2, &x, V_MAX(y) - V_MIN(z) TTL_CTR_V);
			if (changed_x2) {
				if (V_IS_EMPTY(x)) {
					cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
					break;
				}
			}
			cl_v_del_lt_n(&changed_y1, &y, V_MIN(x) + V_MIN(z) TTL_CTR_V);
			if (changed_y1) {
				if (V_IS_EMPTY(y)) {
					cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
					break;
				}
			}
			cl_v_del_gt_n(&changed_y2, &y, V_MAX(x) + V_MAX(z) TTL_CTR_V);
			if (changed_y2) {
				if (V_IS_EMPTY(y)) {
					cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
					break;
				}
			}
			break;
		}
	}

	// Propagate the one selected
	if (V_N_VALS(vs_prop_[v_id]) == 1) {

		if (V_MIN(vs_prop_[v_id]) == 0) {
			y_id = vs_per_c_idx[1];
			z_id = vs_per_c_idx[2];
		} else {
			y_id = vs_per_c_idx[2];
			z_id = vs_per_c_idx[1];
		}

		if (prop_v_id == (unsigned int)x_id) {

			cl_v_del_lt_m(&changed_y1, &vs_prop_[y_id], V_MIN(vs_prop_[x_id]) + V_MIN(vs_prop_[z_id]) TTL_CTR_V);
			if (changed_y1) {
				if (V_IS_EMPTY(vs_prop_[y_id])) {
					*prop_ok = 0;
					return;
				}
			}
			cl_v_del_gt_m(&changed_y2, &vs_prop_[y_id], V_MAX(vs_prop_[x_id]) + V_MAX(vs_prop_[z_id]) TTL_CTR_V);
			if (changed_y2) {
				if (V_IS_EMPTY(vs_prop_[y_id])) {
					*prop_ok = 0;
					return;
				}
			}
			cl_v_del_lt_m(&changed_z1, &vs_prop_[z_id], V_MIN(vs_prop_[y_id]) - V_MAX(vs_prop_[x_id]) TTL_CTR_V);
			if (changed_z1) {
				if (V_IS_EMPTY(vs_prop_[z_id])) {
					*prop_ok = 0;
					return;
				}
			}
			cl_v_del_gt_m(&changed_z2, &vs_prop_[z_id], V_MAX(vs_prop_[y_id]) - V_MIN(vs_prop_[x_id]) TTL_CTR_V);
			if (changed_z2) {
				if (V_IS_EMPTY(vs_prop_[z_id])) {
					*prop_ok = 0;
					return;
				}
			}

			if (changed_y1 || changed_y2) {
				v_add_to_prop(vs_id_to_prop_, vs_prop_, y_id);
			}
			if (changed_z1 || changed_z2) {
				v_add_to_prop(vs_id_to_prop_, vs_prop_, z_id);
			}
			return;
		}

		if (prop_v_id == (unsigned int)y_id) {
			cl_v_del_lt_m(&changed_x1, &vs_prop_[x_id], V_MIN(vs_prop_[y_id]) - V_MAX(vs_prop_[z_id]) TTL_CTR_V);
			if (changed_x1) {
				if (V_IS_EMPTY(vs_prop_[x_id])) {
					*prop_ok = 0;
					return;
				}
			}
			cl_v_del_gt_m(&changed_x2, &vs_prop_[x_id], V_MAX(vs_prop_[y_id]) - V_MIN(vs_prop_[z_id]) TTL_CTR_V);
			if (changed_x2) {
				if (V_IS_EMPTY(vs_prop_[x_id])) {
					*prop_ok = 0;
					return;
				}
			}
			cl_v_del_lt_m(&changed_z1, &vs_prop_[z_id], V_MIN(vs_prop_[y_id]) - V_MAX(vs_prop_[x_id]) TTL_CTR_V);
			if (changed_z1) {
				if (V_IS_EMPTY(vs_prop_[z_id])) {
					*prop_ok = 0;
					return;
				}
			}
			cl_v_del_gt_m(&changed_z2, &vs_prop_[z_id], V_MAX(vs_prop_[y_id]) - V_MIN(vs_prop_[x_id]) TTL_CTR_V);
			if (changed_z2) {
				if (V_IS_EMPTY(vs_prop_[z_id])) {
					*prop_ok = 0;
					return;
				}
			}

			if (changed_x1 || changed_x2) {
				v_add_to_prop(vs_id_to_prop_, vs_prop_, x_id);
			}
			if (changed_z1 || changed_z2) {
				v_add_to_prop(vs_id_to_prop_, vs_prop_, z_id);
			}
			return;
		}

		// prop_v_id == z_id
		cl_v_del_lt_m(&changed_x1, &vs_prop_[x_id], V_MIN(vs_prop_[y_id]) - V_MAX(vs_prop_[z_id]) TTL_CTR_V);
		if (changed_x1) {
			if (V_IS_EMPTY(vs_prop_[x_id])) {
				*prop_ok = 0;
				return;
			}
		}
		cl_v_del_gt_m(&changed_x2, &vs_prop_[x_id], V_MAX(vs_prop_[y_id]) - V_MIN(vs_prop_[z_id]) TTL_CTR_V);
		if (changed_x2) {
			if (V_IS_EMPTY(vs_prop_[x_id])) {
				*prop_ok = 0;
				return;
			}
		}
		cl_v_del_lt_m(&changed_y1, &vs_prop_[y_id], V_MIN(vs_prop_[x_id]) + V_MIN(vs_prop_[z_id]) TTL_CTR_V);
		if (changed_y1) {
			if (V_IS_EMPTY(vs_prop_[y_id])) {
				*prop_ok = 0;
				return;
			}
		}
		cl_v_del_gt_m(&changed_y2, &vs_prop_[y_id], V_MAX(vs_prop_[x_id]) + V_MAX(vs_prop_[z_id]) TTL_CTR_V);
		if (changed_y2) {
			if (V_IS_EMPTY(vs_prop_[y_id])) {
				*prop_ok = 0;
				return;
			}
		}

		if (changed_x1 || changed_x2) {
			v_add_to_prop(vs_id_to_prop_, vs_prop_, x_id);
		}
		if (changed_y1 || changed_y2) {
			v_add_to_prop(vs_id_to_prop_, vs_prop_, y_id);
		}

		y_id = vs_per_c_idx[2];
		z_id = vs_per_c_idx[1];
	}
}

#if  CS_R_VAR_EQ_MINUS_ABS == 1
/*
 * Validate var_eq_minus_abs constraint to be normally propagated, when reified
 * x = |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 var_eq_minus_abs_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 x_id = vs_per_c_idx[0];
	int y_id = vs_per_c_idx[1];
	int z_id = vs_per_c_idx[2];
	int v_id = current_cs->constant_val;	// variable used to flag the constraint (x = y − z or x = z − y) that should be propagated
	VARS_PROP x;
	VARS_PROP y;
	VARS_PROP z;
	bool changed;
	bool changed_x1;
	bool changed_y1;
	bool changed_z1;
	bool changed_x2;
	bool changed_y2;
	bool changed_z2;
	int i;

	// constraint already fixed
	if (V_N_VALS(vs_prop_[x_id]) == 1 && V_N_VALS(vs_prop_[y_id]) == 1 && V_N_VALS(vs_prop_[z_id]) == 1) {
		if (V_MIN(vs_prop_[x_id]) == V_MIN(vs_prop_[y_id]) - V_MIN(vs_prop_[z_id])) {

			// Signal x=y-z case as the one
			cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);

			// select this as the VAR_EQ_MINUS_ABS to propagate
			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;
		}
		if (V_MIN(vs_prop_[x_id]) == V_MIN(vs_prop_[z_id]) - V_MIN(vs_prop_[y_id])) {

			// Signal x=z-y case as the one
			cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);

			// select this as the VAR_EQ_MINUS_ABS to propagate
			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;
		}
	}

	// if no choice made, try to remove x = y − z
	if (V_N_VALS(vs_prop_[v_id]) == 2) {
		cl_v_copy_pm(&x, &vs_prop_[x_id] TTL_CTR_V);
		cl_v_copy_pm(&y, &vs_prop_[y_id] TTL_CTR_V);
		cl_v_copy_pm(&z, &vs_prop_[z_id] TTL_CTR_V);

		for (i = 0; i < 1; i++) {
			if (prop_v_id == (unsigned int)x_id) {

				cl_v_del_lt_n(&changed_y1, &y, V_MIN(x) + V_MIN(z) TTL_CTR_V);
				if (changed_y1) {
					if (V_IS_EMPTY(y)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
						break;
					}
				}
				cl_v_del_gt_n(&changed_y2, &y, V_MAX(x) + V_MAX(z) TTL_CTR_V);
				if (changed_y2) {
					if (V_IS_EMPTY(y)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
						break;
					}
				}
				cl_v_del_lt_n(&changed_z1, &z, V_MIN(y) - V_MAX(x) TTL_CTR_V);
				if (changed_z1) {
					if (V_IS_EMPTY(z)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
						break;
					}
				}
				cl_v_del_gt_n(&changed_z2, &z, V_MAX(y) - V_MIN(x) TTL_CTR_V);
				if (changed_z2) {
					if (V_IS_EMPTY(z)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
						break;
					}
				}
				break;
			}

			if (prop_v_id == (unsigned int)y_id) {
				cl_v_del_lt_n(&changed_x1, &x, V_MIN(y) - V_MAX(z) TTL_CTR_V);
				if (changed_x1) {
					if (V_IS_EMPTY(x)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
						break;
					}
				}
				cl_v_del_gt_n(&changed_x2, &x, V_MAX(y) - V_MIN(z) TTL_CTR_V);
				if (changed_x2) {
					if (V_IS_EMPTY(x)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
						break;
					}
				}
				cl_v_del_lt_n(&changed_z1, &z, V_MIN(y) - V_MAX(x) TTL_CTR_V);
				if (changed_z1) {
					if (V_IS_EMPTY(z)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
						break;
					}
				}
				cl_v_del_gt_n(&changed_z2, &z, V_MAX(y) - V_MIN(x) TTL_CTR_V);
				if (changed_z2) {
					if (V_IS_EMPTY(z)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
						break;
					}
				}
				break;
			}

			// prop_v_id == z_id
			cl_v_del_lt_n(&changed_x1, &x, V_MIN(y) - V_MAX(z) TTL_CTR_V);
			if (changed_x1) {
				if (V_IS_EMPTY(x)) {
					cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
					break;
				}
			}
			cl_v_del_gt_n(&changed_x2, &x, V_MAX(y) - V_MIN(z) TTL_CTR_V);
			if (changed_x2) {
				if (V_IS_EMPTY(x)) {
					cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
					break;
				}
			}
			cl_v_del_lt_n(&changed_y1, &y, V_MIN(x) + V_MIN(z) TTL_CTR_V);
			if (changed_y1) {
				if (V_IS_EMPTY(y)) {
					cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
					break;
				}
			}
			cl_v_del_gt_n(&changed_y2, &y, V_MAX(x) + V_MAX(z) TTL_CTR_V);
			if (changed_y2) {
				if (V_IS_EMPTY(y)) {
					cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
					break;
				}
			}
			break;
		}
	}

	// if no choice made yet, try to remove x = z − y
	if (V_N_VALS(vs_prop_[v_id]) == 2) {

		y_id = vs_per_c_idx[2];
		z_id = vs_per_c_idx[1];

		cl_v_copy_pm(&x, &vs_prop_[x_id] TTL_CTR_V);
		cl_v_copy_pm(&y, &vs_prop_[y_id] TTL_CTR_V);
		cl_v_copy_pm(&z, &vs_prop_[z_id] TTL_CTR_V);

		for (i = 0; i < 1; i++) {
			if (prop_v_id == (unsigned int)x_id) {

				cl_v_del_lt_n(&changed_y1, &y, V_MIN(x) + V_MIN(z) TTL_CTR_V);
				if (changed_y1) {
					if (V_IS_EMPTY(y)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
						break;
					}
				}
				cl_v_del_gt_n(&changed_y2, &y, V_MAX(x) + V_MAX(z) TTL_CTR_V);
				if (changed_y2) {
					if (V_IS_EMPTY(y)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
						break;
					}
				}
				cl_v_del_lt_n(&changed_z1, &z, V_MIN(y) - V_MAX(x) TTL_CTR_V);
				if (changed_z1) {
					if (V_IS_EMPTY(z)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
						break;
					}
				}
				cl_v_del_gt_n(&changed_z2, &z, V_MAX(y) - V_MIN(x) TTL_CTR_V);
				if (changed_z2) {
					if (V_IS_EMPTY(z)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
						break;
					}
				}
				break;
			}

			if (prop_v_id == (unsigned int)y_id) {
				cl_v_del_lt_n(&changed_x1, &x, V_MIN(y) - V_MAX(z) TTL_CTR_V);
				if (changed_x1) {
					if (V_IS_EMPTY(x)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
						break;
					}
				}
				cl_v_del_gt_n(&changed_x2, &x, V_MAX(y) - V_MIN(z) TTL_CTR_V);
				if (changed_x2) {
					if (V_IS_EMPTY(x)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
						break;
					}
				}
				cl_v_del_lt_n(&changed_z1, &z, V_MIN(y) - V_MAX(x) TTL_CTR_V);
				if (changed_z1) {
					if (V_IS_EMPTY(z)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
						break;
					}
				}
				cl_v_del_gt_n(&changed_z2, &z, V_MAX(y) - V_MIN(x) TTL_CTR_V);
				if (changed_z2) {
					if (V_IS_EMPTY(z)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
						break;
					}
				}
				break;
			}

			// prop_v_id == z_id
			cl_v_del_lt_n(&changed_x1, &x, V_MIN(y) - V_MAX(z) TTL_CTR_V);
			if (changed_x1) {
				if (V_IS_EMPTY(x)) {
					cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
					break;
				}
			}
			cl_v_del_gt_n(&changed_x2, &x, V_MAX(y) - V_MIN(z) TTL_CTR_V);
			if (changed_x2) {
				if (V_IS_EMPTY(x)) {
					cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
					break;
				}
			}
			cl_v_del_lt_n(&changed_y1, &y, V_MIN(x) + V_MIN(z) TTL_CTR_V);
			if (changed_y1) {

				int x_id = vs_per_c_idx[0];
				int y_id = vs_per_c_idx[1];
				int z_id = vs_per_c_idx[2];
				int v_id = current_cs->constant_val;	// variable used to flag the constraint (x = y − z or x = z − y) that should be propagated
				VARS_PROP x;
				VARS_PROP y;
				VARS_PROP z;
				bool changed;
				bool changed_x1;
				bool changed_y1;
				bool changed_z1;
				bool changed_x2;
				bool changed_y2;
				bool changed_z2;
				int i;

				if (V_N_VALS(vs_prop_[x_id]) == 1 && V_N_VALS(vs_prop_[y_id]) == 1 && V_N_VALS(vs_prop_[z_id]) == 1) {
					if (V_MIN(vs_prop_[x_id]) == V_MIN(vs_prop_[y_id]) - V_MIN(vs_prop_[z_id])) {

						// Signal x=y-z case as the one
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);

						// select this as the VAR_EQ_MINUS_ABS to propagate
						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;
					}
					if (V_MIN(vs_prop_[x_id]) == V_MIN(vs_prop_[z_id]) - V_MIN(vs_prop_[y_id])) {

						// Signal x=z-y case as the one
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);

						// select this as the VAR_EQ_MINUS_ABS to propagate
						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;
					}
				}

				// if no choice made, try to remove x = y − z
				if (V_N_VALS(vs_prop_[v_id]) == 2) {
					cl_v_copy_pm(&x, &vs_prop_[x_id] TTL_CTR_V);
					cl_v_copy_pm(&y, &vs_prop_[y_id] TTL_CTR_V);
					cl_v_copy_pm(&z, &vs_prop_[z_id] TTL_CTR_V);

					for (i = 0; i < 1; i++) {
						if (prop_v_id == (unsigned int)x_id) {

							cl_v_del_lt_n(&changed_y1, &y, V_MIN(x) + V_MIN(z) TTL_CTR_V);
							if (changed_y1) {
								if (V_IS_EMPTY(y)) {
									cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
									break;
								}
							}
							cl_v_del_gt_n(&changed_y2, &y, V_MAX(x) + V_MAX(z) TTL_CTR_V);
							if (changed_y2) {
								if (V_IS_EMPTY(y)) {
									cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
									break;
								}
							}
							cl_v_del_lt_n(&changed_z1, &z, V_MIN(y) - V_MAX(x) TTL_CTR_V);
							if (changed_z1) {
								if (V_IS_EMPTY(z)) {
									cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
									break;
								}
							}
							cl_v_del_gt_n(&changed_z2, &z, V_MAX(y) - V_MIN(x) TTL_CTR_V);
							if (changed_z2) {
								if (V_IS_EMPTY(z)) {
									cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
									break;
								}
							}
							break;
						}

						if (prop_v_id == (unsigned int)y_id) {
							cl_v_del_lt_n(&changed_x1, &x, V_MIN(y) - V_MAX(z) TTL_CTR_V);
							if (changed_x1) {
								if (V_IS_EMPTY(x)) {
									cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
									break;
								}
							}
							cl_v_del_gt_n(&changed_x2, &x, V_MAX(y) - V_MIN(z) TTL_CTR_V);
							if (changed_x2) {
								if (V_IS_EMPTY(x)) {
									cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
									break;
								}
							}
							cl_v_del_lt_n(&changed_z1, &z, V_MIN(y) - V_MAX(x) TTL_CTR_V);
							if (changed_z1) {
								if (V_IS_EMPTY(z)) {
									cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
									break;
								}
							}
							cl_v_del_gt_n(&changed_z2, &z, V_MAX(y) - V_MIN(x) TTL_CTR_V);
							if (changed_z2) {
								if (V_IS_EMPTY(z)) {
									cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
									break;
								}
							}
							break;
						}

						// prop_v_id == z_id
						cl_v_del_lt_n(&changed_x1, &x, V_MIN(y) - V_MAX(z) TTL_CTR_V);
						if (changed_x1) {
							if (V_IS_EMPTY(x)) {
								cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
								break;
							}
						}
						cl_v_del_gt_n(&changed_x2, &x, V_MAX(y) - V_MIN(z) TTL_CTR_V);
						if (changed_x2) {
							if (V_IS_EMPTY(x)) {
								cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
								break;
							}
						}
						cl_v_del_lt_n(&changed_y1, &y, V_MIN(x) + V_MIN(z) TTL_CTR_V);
						if (changed_y1) {
							if (V_IS_EMPTY(y)) {
								cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
								break;
							}
						}
						cl_v_del_gt_n(&changed_y2, &y, V_MAX(x) + V_MAX(z) TTL_CTR_V);
						if (changed_y2) {
							if (V_IS_EMPTY(y)) {
								cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
								break;
							}
						}
						break;
					}
				}

				// if no choice made yet, try to remove x = z − y
				if (V_N_VALS(vs_prop_[v_id]) == 2) {

					y_id = vs_per_c_idx[2];
					z_id = vs_per_c_idx[1];

					cl_v_copy_pm(&x, &vs_prop_[x_id] TTL_CTR_V);
					cl_v_copy_pm(&y, &vs_prop_[y_id] TTL_CTR_V);
					cl_v_copy_pm(&z, &vs_prop_[z_id] TTL_CTR_V);

					for (i = 0; i < 1; i++) {
						if (prop_v_id == (unsigned int)x_id) {

							cl_v_del_lt_n(&changed_y1, &y, V_MIN(x) + V_MIN(z) TTL_CTR_V);
							if (changed_y1) {
								if (V_IS_EMPTY(y)) {
									cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
									break;
								}
							}
							cl_v_del_gt_n(&changed_y2, &y, V_MAX(x) + V_MAX(z) TTL_CTR_V);
							if (changed_y2) {
								if (V_IS_EMPTY(y)) {
									cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
									break;
								}
							}
							cl_v_del_lt_n(&changed_z1, &z, V_MIN(y) - V_MAX(x) TTL_CTR_V);
							if (changed_z1) {
								if (V_IS_EMPTY(z)) {
									cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
									break;
								}
							}
							cl_v_del_gt_n(&changed_z2, &z, V_MAX(y) - V_MIN(x) TTL_CTR_V);
							if (changed_z2) {
								if (V_IS_EMPTY(z)) {
									cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
									break;
								}
							}
							break;
						}

						if (prop_v_id == (unsigned int)y_id) {
							cl_v_del_lt_n(&changed_x1, &x, V_MIN(y) - V_MAX(z) TTL_CTR_V);
							if (changed_x1) {
								if (V_IS_EMPTY(x)) {
									cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
									break;
								}
							}
							cl_v_del_gt_n(&changed_x2, &x, V_MAX(y) - V_MIN(z) TTL_CTR_V);
							if (changed_x2) {
								if (V_IS_EMPTY(x)) {
									cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
									break;
								}
							}
							cl_v_del_lt_n(&changed_z1, &z, V_MIN(y) - V_MAX(x) TTL_CTR_V);
							if (changed_z1) {
								if (V_IS_EMPTY(z)) {
									cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
									break;
								}
							}
							cl_v_del_gt_n(&changed_z2, &z, V_MAX(y) - V_MIN(x) TTL_CTR_V);
							if (changed_z2) {
								if (V_IS_EMPTY(z)) {
									cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
									break;
								}
							}
							break;
						}

						// prop_v_id == z_id
						cl_v_del_lt_n(&changed_x1, &x, V_MIN(y) - V_MAX(z) TTL_CTR_V);
						if (changed_x1) {
							if (V_IS_EMPTY(x)) {
								cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
								break;
							}
						}
						cl_v_del_gt_n(&changed_x2, &x, V_MAX(y) - V_MIN(z) TTL_CTR_V);
						if (changed_x2) {
							if (V_IS_EMPTY(x)) {
								cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
								break;
							}
						}
						cl_v_del_lt_n(&changed_y1, &y, V_MIN(x) + V_MIN(z) TTL_CTR_V);
						if (changed_y1) {
							if (V_IS_EMPTY(y)) {
								cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
								break;
							}
						}
						cl_v_del_gt_n(&changed_y2, &y, V_MAX(x) + V_MAX(z) TTL_CTR_V);
						if (changed_y2) {
							if (V_IS_EMPTY(y)) {
								cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
								break;
							}
						}
						break;
					}
				}

				// Reify the one selected
				if (V_N_VALS(vs_prop_[v_id]) == 1) {

					if (V_MIN(vs_prop_[v_id]) == 0) {
						y_id = vs_per_c_idx[1];
						z_id = vs_per_c_idx[2];
					} else {
						y_id = vs_per_c_idx[2];
						z_id = vs_per_c_idx[1];
					}

					if (prop_v_id == (unsigned int)x_id) {
							VARS_PROP y;
							cl_v_copy_pm(&y, &vs_prop_[y_id] TTL_CTR_V);

							cl_v_del_lt_n(&changed, &y, V_MIN(vs_prop_[x_id]) + V_MIN(vs_prop_[z_id]) 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;
							}
							cl_v_del_gt_n(&changed, &y, V_MAX(vs_prop_[x_id]) + V_MAX(vs_prop_[z_id]) 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;
							}

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

							cl_v_del_lt_n(&changed, &z, V_MIN(y) - V_MAX(vs_prop_[x_id]) TTL_CTR_V);
							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;
							}
							cl_v_del_gt_n(&changed, &z, V_MAX(y) - V_MIN(vs_prop_[x_id]) TTL_CTR_V);
							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;
						}

						if (prop_v_id == (unsigned int)y_id) {

							VARS_PROP x;
							cl_v_copy_pm(&x, &vs_prop_[x_id] TTL_CTR_V);

							cl_v_del_lt_n(&changed, &x, V_MIN(vs_prop_[y_id]) - V_MAX(vs_prop_[z_id]) TTL_CTR_V);
							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;
							}
							cl_v_del_gt_n(&changed, &x, V_MAX(vs_prop_[y_id]) - V_MIN(vs_prop_[z_id]) TTL_CTR_V);
							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;
							}

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

							cl_v_del_lt_n(&changed, &z, V_MIN(vs_prop_[y_id]) - V_MAX(x) TTL_CTR_V);
							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;
							}
							cl_v_del_gt_n(&changed, &z, V_MAX(vs_prop_[y_id]) - V_MIN(x) TTL_CTR_V);
							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;
							}
							return;
						}

						// if prop_v_id == z_id
						VARS_PROP x;
						cl_v_copy_pm(&x, &vs_prop_[x_id] TTL_CTR_V);

						cl_v_del_lt_n(&changed, &x, V_MIN(vs_prop_[y_id]) - V_MAX(vs_prop_[z_id]) TTL_CTR_V);
						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;
						}
						cl_v_del_gt_n(&changed, &x, V_MAX(vs_prop_[y_id]) - V_MIN(vs_prop_[z_id]) TTL_CTR_V);
						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;
						}

						VARS_PROP y;
						cl_v_copy_pm(&y, &vs_prop_[y_id] TTL_CTR_V);

						cl_v_del_lt_n(&changed, &y, V_MIN(x) + V_MIN(vs_prop_[z_id]) 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;
						}
						cl_v_del_gt_n(&changed, &y, V_MAX(x) + V_MAX(vs_prop_[z_id]) 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));
						}


				}

				if (V_IS_EMPTY(y)) {
					cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
					break;
				}
			}
			cl_v_del_gt_n(&changed_y2, &y, V_MAX(x) + V_MAX(z) TTL_CTR_V);
			if (changed_y2) {
				if (V_IS_EMPTY(y)) {
					cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
					break;
				}
			}
			break;
		}
	}

	// Reify the one selected
	if (V_N_VALS(vs_prop_[v_id]) == 1) {

		if (V_MIN(vs_prop_[v_id]) == 0) {
			y_id = vs_per_c_idx[1];
			z_id = vs_per_c_idx[2];
		} else {
			y_id = vs_per_c_idx[2];
			z_id = vs_per_c_idx[1];
		}

		if (prop_v_id == (unsigned int)x_id) {
			VARS_PROP y;
			cl_v_copy_pm(&y, &vs_prop_[y_id] TTL_CTR_V);

			cl_v_del_lt_n(&changed, &y, V_MIN(vs_prop_[x_id]) + V_MIN(vs_prop_[z_id]) 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;
			}
			cl_v_del_gt_n(&changed, &y, V_MAX(vs_prop_[x_id]) + V_MAX(vs_prop_[z_id]) 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;
			}

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

			cl_v_del_lt_n(&changed, &z, V_MIN(y) - V_MAX(vs_prop_[x_id]) TTL_CTR_V);
			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;
			}
			cl_v_del_gt_n(&changed, &z, V_MAX(y) - V_MIN(vs_prop_[x_id]) TTL_CTR_V);
			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;
		}

		if (prop_v_id == (unsigned int)y_id) {

			VARS_PROP x;
			cl_v_copy_pm(&x, &vs_prop_[x_id] TTL_CTR_V);

			cl_v_del_lt_n(&changed, &x, V_MIN(vs_prop_[y_id]) - V_MAX(vs_prop_[z_id]) TTL_CTR_V);
			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;
			}
			cl_v_del_gt_n(&changed, &x, V_MAX(vs_prop_[y_id]) - V_MIN(vs_prop_[z_id]) TTL_CTR_V);
			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;
			}

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

			cl_v_del_lt_n(&changed, &z, V_MIN(vs_prop_[y_id]) - V_MAX(x) TTL_CTR_V);
			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;
			}
			cl_v_del_gt_n(&changed, &z, V_MAX(vs_prop_[y_id]) - V_MIN(x) TTL_CTR_V);
			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;
			}
			return;
		}

		// if prop_v_id == z_id
		VARS_PROP x;
		cl_v_copy_pm(&x, &vs_prop_[x_id] TTL_CTR_V);

		cl_v_del_lt_n(&changed, &x, V_MIN(vs_prop_[y_id]) - V_MAX(vs_prop_[z_id]) TTL_CTR_V);
		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;
		}
		cl_v_del_gt_n(&changed, &x, V_MAX(vs_prop_[y_id]) - V_MIN(vs_prop_[z_id]) TTL_CTR_V);
		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;
		}

		VARS_PROP y;
		cl_v_copy_pm(&y, &vs_prop_[y_id] TTL_CTR_V);

		cl_v_del_lt_n(&changed, &y, V_MIN(x) + V_MIN(vs_prop_[z_id]) 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;
		}
		cl_v_del_gt_n(&changed, &y, V_MAX(x) + V_MAX(vs_prop_[z_id]) 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));
		}
	}
}

/*
 * Propagate the domain of the variable with the ID prop_v_id through all the other variables on the same c_numb ID var_eq_minus_abs opposite constraint
 * x != |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
 * 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 var_eq_minus_abs_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 TTL_CTR) {

	int x_id = vs_per_c_idx[0];
	int y_id = vs_per_c_idx[1];
	int z_id = vs_per_c_idx[2];
	int v_id = current_cs->constant_val;	// variable used to flag the constraint (x != y − z or x != z − y) that should be propagated
	VARS_PROP x;
	VARS_PROP y;
	VARS_PROP z;
	bool changed;
	bool changed_x1;
	bool changed_y1;
	bool changed_z1;
	bool changed_x2;
	bool changed_y2;
	bool changed_z2;
	int i;

	// if no choice made, try to set x != y − z
	if (V_N_VALS(vs_prop_[v_id]) == 2) {
		cl_v_copy_pm(&x, &vs_prop_[x_id] TTL_CTR_V);
		cl_v_copy_pm(&y, &vs_prop_[y_id] TTL_CTR_V);
		cl_v_copy_pm(&z, &vs_prop_[z_id] TTL_CTR_V);

		for (i = 0; i < 1; i++) {
			if (prop_v_id == (unsigned int)x_id) {

				cl_v_del_lt_n(&changed_y1, &y, V_MIN(x) + V_MIN(z) TTL_CTR_V);
				if (changed_y1) {
					if (V_IS_EMPTY(y)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
						break;
					}
				}
				cl_v_del_gt_n(&changed_y2, &y, V_MAX(x) + V_MAX(z) TTL_CTR_V);
				if (changed_y2) {
					if (V_IS_EMPTY(y)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
						break;
					}
				}
				cl_v_del_lt_n(&changed_z1, &z, V_MIN(y) - V_MAX(x) TTL_CTR_V);
				if (changed_z1) {
					if (V_IS_EMPTY(z)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
						break;
					}
				}
				cl_v_del_gt_n(&changed_z2, &z, V_MAX(y) - V_MIN(x) TTL_CTR_V);
				if (changed_z2) {
					if (V_IS_EMPTY(z)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
						break;
					}
				}
				break;
			}

			if (prop_v_id == (unsigned int)y_id) {
				cl_v_del_lt_n(&changed_x1, &x, V_MIN(y) - V_MAX(z) TTL_CTR_V);
				if (changed_x1) {
					if (V_IS_EMPTY(x)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
						break;
					}
				}
				cl_v_del_gt_n(&changed_x2, &x, V_MAX(y) - V_MIN(z) TTL_CTR_V);
				if (changed_x2) {
					if (V_IS_EMPTY(x)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
						break;
					}
				}
				cl_v_del_lt_n(&changed_z1, &z, V_MIN(y) - V_MAX(x) TTL_CTR_V);
				if (changed_z1) {
					if (V_IS_EMPTY(z)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
						break;
					}
				}
				cl_v_del_gt_n(&changed_z2, &z, V_MAX(y) - V_MIN(x) TTL_CTR_V);
				if (changed_z2) {
					if (V_IS_EMPTY(z)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
						break;
					}
				}
				break;
			}

			// prop_v_id == z_id
			cl_v_del_lt_n(&changed_x1, &x, V_MIN(y) - V_MAX(z) TTL_CTR_V);
			if (changed_x1) {
				if (V_IS_EMPTY(x)) {
					cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
					break;
				}
			}
			cl_v_del_gt_n(&changed_x2, &x, V_MAX(y) - V_MIN(z) TTL_CTR_V);
			if (changed_x2) {
				if (V_IS_EMPTY(x)) {
					cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
					break;
				}
			}
			cl_v_del_lt_n(&changed_y1, &y, V_MIN(x) + V_MIN(z) TTL_CTR_V);
			if (changed_y1) {
				if (V_IS_EMPTY(y)) {
					cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
					break;
				}
			}
			cl_v_del_gt_n(&changed_y2, &y, V_MAX(x) + V_MAX(z) TTL_CTR_V);
			if (changed_y2) {
				if (V_IS_EMPTY(y)) {
					cl_v_del_val_m(&changed, &vs_prop_[v_id], 1 TTL_CTR_V);
					break;
				}
			}
			break;
		}
	}

	// if no choice made yet, try to set x != z − y
	if (V_N_VALS(vs_prop_[v_id]) == 2) {

		y_id = vs_per_c_idx[2];
		z_id = vs_per_c_idx[1];

		cl_v_copy_pm(&x, &vs_prop_[x_id] TTL_CTR_V);
		cl_v_copy_pm(&y, &vs_prop_[y_id] TTL_CTR_V);
		cl_v_copy_pm(&z, &vs_prop_[z_id] TTL_CTR_V);

		for (i = 0; i < 1; i++) {
			if (prop_v_id == (unsigned int)x_id) {

				cl_v_del_lt_n(&changed_y1, &y, V_MIN(x) + V_MIN(z) TTL_CTR_V);
				if (changed_y1) {
					if (V_IS_EMPTY(y)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
						break;
					}
				}
				cl_v_del_gt_n(&changed_y2, &y, V_MAX(x) + V_MAX(z) TTL_CTR_V);
				if (changed_y2) {
					if (V_IS_EMPTY(y)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
						break;
					}
				}
				cl_v_del_lt_n(&changed_z1, &z, V_MIN(y) - V_MAX(x) TTL_CTR_V);
				if (changed_z1) {
					if (V_IS_EMPTY(z)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
						break;
					}
				}
				cl_v_del_gt_n(&changed_z2, &z, V_MAX(y) - V_MIN(x) TTL_CTR_V);
				if (changed_z2) {
					if (V_IS_EMPTY(z)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
						break;
					}
				}
				break;
			}

			if (prop_v_id == (unsigned int)y_id) {
				cl_v_del_lt_n(&changed_x1, &x, V_MIN(y) - V_MAX(z) TTL_CTR_V);
				if (changed_x1) {
					if (V_IS_EMPTY(x)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
						break;
					}
				}
				cl_v_del_gt_n(&changed_x2, &x, V_MAX(y) - V_MIN(z) TTL_CTR_V);
				if (changed_x2) {
					if (V_IS_EMPTY(x)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
						break;
					}
				}
				cl_v_del_lt_n(&changed_z1, &z, V_MIN(y) - V_MAX(x) TTL_CTR_V);
				if (changed_z1) {
					if (V_IS_EMPTY(z)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
						break;
					}
				}
				cl_v_del_gt_n(&changed_z2, &z, V_MAX(y) - V_MIN(x) TTL_CTR_V);
				if (changed_z2) {
					if (V_IS_EMPTY(z)) {
						cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
						break;
					}
				}
				break;
			}

			// prop_v_id == z_id
			cl_v_del_lt_n(&changed_x1, &x, V_MIN(y) - V_MAX(z) TTL_CTR_V);
			if (changed_x1) {
				if (V_IS_EMPTY(x)) {
					cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
					break;
				}
			}
			cl_v_del_gt_n(&changed_x2, &x, V_MAX(y) - V_MIN(z) TTL_CTR_V);
			if (changed_x2) {
				if (V_IS_EMPTY(x)) {
					cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
					break;
				}
			}
			cl_v_del_lt_n(&changed_y1, &y, V_MIN(x) + V_MIN(z) TTL_CTR_V);
			if (changed_y1) {
				if (V_IS_EMPTY(y)) {
					cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
					break;
				}
			}
			cl_v_del_gt_n(&changed_y2, &y, V_MAX(x) + V_MAX(z) TTL_CTR_V);
			if (changed_y2) {
				if (V_IS_EMPTY(y)) {
					cl_v_del_val_m(&changed, &vs_prop_[v_id], 0 TTL_CTR_V);
					break;
				}
			}
			break;
		}
	}

	// Propagate the one selected
	if (V_N_VALS(vs_prop_[v_id]) == 1) {

		// x!= y - z
		if (V_MIN(vs_prop_[v_id]) == 0) {
			y_id = vs_per_c_idx[1];
			z_id = vs_per_c_idx[2];
		// x!= z - y
		} else {
			y_id = vs_per_c_idx[2];
			z_id = vs_per_c_idx[1];
		}

		if (V_N_VALS(vs_prop_[x_id]) == 1 && V_N_VALS(vs_prop_[y_id]) == 1) {

			cl_v_del_val_m(&changed, &vs_prop_[z_id], V_MIN(vs_prop_[y_id]) - V_MIN(vs_prop_[x_id]) TTL_CTR_V);

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

		if (V_N_VALS(vs_prop_[x_id]) == 1 && V_N_VALS(vs_prop_[z_id]) == 1) {

			cl_v_del_val_m(&changed, &vs_prop_[y_id], V_MIN(vs_prop_[x_id]) + V_MIN(vs_prop_[z_id]) TTL_CTR_V);

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

		if (V_N_VALS(vs_prop_[y_id]) == 1 && V_N_VALS(vs_prop_[z_id]) == 1) {

			cl_v_del_val_m(&changed, &vs_prop_[x_id], V_MIN(vs_prop_[y_id]) - V_MIN(vs_prop_[z_id]) TTL_CTR_V);

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

CUDA_FUNC void var_eq_minus_abs_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 TTL_CTR) {

#if CS_R_VAR_EQ_MINUS_ABS == 0
	var_eq_minus_abs_prop(vs_per_c_idx, vs_prop_, prop_v_id, current_cs, vs_id_to_prop_, prop_ok TTL_CTR_V);
#if CL_STATS == 1
	*propagated = true;
#endif
#elif CS_R_VAR_EQ_MINUS_ABS == 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) {
				var_eq_minus_abs_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) {
					var_eq_minus_abs_prop(vs_per_c_idx, vs_prop_, prop_v_id, current_cs, vs_id_to_prop_, prop_ok TTL_CTR_V);
				} else {
					var_eq_minus_abs_prop_opposite(vs_per_c_idx, vs_prop_, prop_v_id, current_cs, vs_id_to_prop_, prop_ok TTL_CTR_V);
				}
#if CL_STATS == 1
				*propagated = true;
#endif
			}
		}
	} else {
		var_eq_minus_abs_prop(vs_per_c_idx, vs_prop_, prop_v_id, current_cs, vs_id_to_prop_, prop_ok TTL_CTR_V);
#if CL_STATS == 1
		*propagated = true;
#endif
	}
#endif
}

#endif