/*
 * vars.c
 *
 *  Created on: 23/08/2014
 *      Author: Pedro
 */

#include "variables.h"

#include <stdio.h>
#include <stdlib.h>

#include "CL/cl_platform.h"
#include "bitmaps.h"
#include "intervals.h"
#include "config.h"
#include "kernels/cl_constraints.h"

/*
 * Create a new variable without constraints and with the received value on its domain and return its ID
 * val - value to set on the domain
 */
unsigned int v_new_val(unsigned int val) {
	return v_new_vals(&val, 1, false);
}

/*
 * Create a new variable without constraints and with the received values on its domain and return its ID
 * vals - vector with all the domain values
 * n_vals - Number of values in the vals vector
 * to_label - true if this variable should be labeled
 */
unsigned int v_new_vals(unsigned int *vals, unsigned int n_vals, bool to_label) {

	// avoid creating more than one variable with the same and only value on the domain
	if (n_vals == 1 && CONST_VS_ID[*vals] != -1) {
		return (unsigned int) CONST_VS_ID[*vals];

	} else {
		if (n_vals == 1) {
			CONST_VS_ID[vals[0]] = (int) V_ID_CNTR;
		}
		unsigned int i, j;

		// if more variables are needed, allocate a new vector and updates the constraints pointers
		if (V_ID_CNTR == N_VS) {
			VS_AUX = (var*) malloc(N_VS * 2 * (sizeof(var)));

			vs_copy(VS_AUX, VS, N_VS);

			for (i = 0; i < C_ID_CNTR; i++) {
				for (j = 0; j < CS[i].n_c_vs; j++) {
					CS[i].c_vs[j] = &VS_AUX[CS[i].c_vs[j]->v_id];
				}
			}

			free(VS);
			VS = VS_AUX;

			N_VS *= 2;

			if (WORK == OPT) {
				free(VS_LOCK);
				free(VS_LOCK_BEST);
				VS_LOCK = (var*) malloc(N_VS * (sizeof(var)));
				VS_LOCK_BEST = (var*) malloc(N_VS * (sizeof(var)));
			}
		}

		b_new_vals(&VS[V_ID_CNTR].domain_b, vals, n_vals);
		VS[V_ID_CNTR].min = (unsigned short) b_get_min_val(&VS[V_ID_CNTR].domain_b);
		VS[V_ID_CNTR].max = (unsigned short) b_get_max_val(&VS[V_ID_CNTR].domain_b);
		VS[V_ID_CNTR].n_vals = (unsigned short) n_vals;
		VS[V_ID_CNTR].v_id = (unsigned short) V_ID_CNTR;
		VS[V_ID_CNTR].v_id_print = (unsigned short) V_ID_CNTR;
		VS[V_ID_CNTR].cs = NULL;
		VS[V_ID_CNTR].n_cs = 0;
		VS[V_ID_CNTR].to_prop = false;

#if FZN_SEQ
		VS[V_ID_CNTR].assign_h = ASSIGN_MODE_D;
		VS[V_ID_CNTR].label_h = LABEL_MODE_D;
#endif

		if (VS[V_ID_CNTR].min == VS[V_ID_CNTR].max) {
			VS[V_ID_CNTR].to_label = false;
		} else {
			VS[V_ID_CNTR].to_label = to_label;
		}

#if USE_BOOLEAN_VS
		if (VS[V_ID_CNTR].max <= 1) {
			VS[V_ID_CNTR].boolean = true;
			BOOLEAN_VS = true;
		} else {
			VS[V_ID_CNTR].boolean = false;
		}
#else
		VS[V_ID_CNTR].boolean = false;
		BOOLEAN_VS = false;
#endif

		VS[V_ID_CNTR].reif = false;

		if (VS[V_ID_CNTR].n_vals != VS[V_ID_CNTR].max - VS[V_ID_CNTR].min + 1) {
			CAN_USE_INTERVALS = false;
		}

		return V_ID_CNTR++;
	}
}

/*
 * Create a new variable without constraints and with all the values between min and max (inclusive) on its domain and return its ID
 * min - minimum value of the domain
 * max - maximum value of the domain
 * to_label - true if this variable should be labeled
 */
unsigned int v_new_range(unsigned int min, unsigned int max, bool to_label) {

	// avoid creating more than one variable with the same and only value on the domain
	if (min == max && CONST_VS_ID[min] != -1) {
		return (unsigned int) CONST_VS_ID[min];

	} else {
		if (min == max) {
			CONST_VS_ID[min] = (int) V_ID_CNTR;
		}

		unsigned int i, j;

		// if more constraints are needed, allocate a new vector and updates the variables pointers
		if (V_ID_CNTR == N_VS) {
			VS_AUX = (var*) malloc(N_VS * 2 * (sizeof(var)));

			vs_copy(VS_AUX, VS, N_VS);

			for (i = 0; i < C_ID_CNTR; i++) {
				for (j = 0; j < CS[i].n_c_vs; j++) {
					CS[i].c_vs[j] = &VS_AUX[CS[i].c_vs[j]->v_id];
				}
			}

			free(VS);
			VS = VS_AUX;

			N_VS *= 2;

			if (WORK == OPT) {
				free(VS_LOCK);
				free(VS_LOCK_BEST);
				VS_LOCK = (var*) malloc(N_VS * (sizeof(var)));
				VS_LOCK_BEST = (var*) malloc(N_VS * (sizeof(var)));
			}
		}

		b_new_range(&VS[V_ID_CNTR].domain_b, min, max);
		VS[V_ID_CNTR].min = (unsigned short) min;
		VS[V_ID_CNTR].max = (unsigned short) max;
		VS[V_ID_CNTR].n_vals = (unsigned short) (max - min + 1);
		VS[V_ID_CNTR].v_id = (unsigned short) V_ID_CNTR;
		VS[V_ID_CNTR].v_id_print = (unsigned short) V_ID_CNTR;
		VS[V_ID_CNTR].cs = NULL;
		VS[V_ID_CNTR].n_cs = 0;
		VS[V_ID_CNTR].to_prop = false;

#if FZN_SEQ
		VS[V_ID_CNTR].assign_h = ASSIGN_MODE_D;
		VS[V_ID_CNTR].label_h = LABEL_MODE_D;
#endif

		if (VS[V_ID_CNTR].min == VS[V_ID_CNTR].max) {
			VS[V_ID_CNTR].to_label = false;
		} else {
			VS[V_ID_CNTR].to_label = to_label;
		}

#if USE_BOOLEAN_VS
		if (VS[V_ID_CNTR].max <= 1) {
			VS[V_ID_CNTR].boolean = true;
			BOOLEAN_VS = true;
		} else {
			VS[V_ID_CNTR].boolean = false;
		}
#else
		VS[V_ID_CNTR].boolean = false;
		BOOLEAN_VS = false;
#endif

		VS[V_ID_CNTR].reif = false;

		return V_ID_CNTR++;
	}
}

/*
 * Return true if variable v contains val and false if not.
 * v - variable to check if contains val
 * val - value to check if contained (from 0 to D_MAX)
 */
bool v_contains_val(var *v, unsigned int val) {
	return b_contains_val(&v->domain_b, val);
}

/*
 * Copy values from variable v_src to variable v_dest.
 * v_dest - variable to copy values to
 * v_src - variable to copy values from
 * n_vs - number of variables to copy
 */
void vs_copy(var *v_dest, var *v_src, unsigned int n_vs) {
	unsigned int i;

	for (i = 0; i < n_vs; i++) {
		v_dest[i].boolean = v_src[i].boolean;
		v_dest[i].expanded = v_src[i].expanded;
		v_dest[i].max = v_src[i].max;
		v_dest[i].min = v_src[i].min;
		v_dest[i].n_cs = v_src[i].n_cs;
		v_dest[i].n_vals = v_src[i].n_vals;
		v_dest[i].reif = v_src[i].reif;
		v_dest[i].to_label = v_src[i].to_label;
		v_dest[i].to_prop = v_src[i].to_prop;
		v_dest[i].v_id = v_src[i].v_id;
		v_dest[i].v_id_print = v_src[i].v_id_print;

#if FZN_SEQ
		v_dest[i].label_h = v_src[i].label_h;
		v_dest[i].assign_h = v_src[i].assign_h;
#endif

		b_copy(&v_dest[i].domain_b, &v_src[i].domain_b);
		i_copy(&v_dest[i].domain_i, &v_src[i].domain_i);

		v_dest[i].cs = v_src[i].cs;
	}
}

/*
 * set the variable as empty (n_vals == 0)
 * v - variable to clear
 */
void v_clear(var *v) {
	v->n_vals = 0;
}

/*
 * Clear all variables memory
 */
void vs_clear() {

	unsigned int i;

	for (i = 0; i < N_VS; i++) {
		free(VS[i].cs);
	}
}

/*
 * Do operation v1 = v1 & v2
 * Return true if variable changed and false if not
 * v1 - variable to save operation
 * v2 - variable to do AND with
 */
bool v_intersect_v(var *v1, var *v2) {
	if (b_intersect_b(&v1->domain_b, &v2->domain_b)) {
		v1->n_vals = (unsigned short) b_cnt_vals(&v1->domain_b);
		v1->min = (unsigned short) b_get_min_val(&v1->domain_b);
		v1->max = (unsigned short) b_get_max_val(&v1->domain_b);

		return true;
	}
	return false;
}

/*
 * Do operation v1 = v1 | v2
 * Return true if variable changed and false if not
 * v1 - variable to save operation
 * v2 - variable to do AND with
 */
bool v_union_v(var *v1, var *v2) {
	if (b_union_b(&v1->domain_b, &v2->domain_b)) {
		v1->n_vals = (unsigned short) b_cnt_vals(&v1->domain_b);
		v1->min = (unsigned short) b_get_min_val(&v1->domain_b);
		v1->max = (unsigned short) b_get_max_val(&v1->domain_b);

		return true;
	}
	return false;
}

/*
 * remove value from variable domain
 * Return true if domain changed and false if not
 * v - variable to remove value from
 * val - value to remove from variable
 */
bool v_del_val(var *v, int val) {
	if (val < v->min || val > v->max) {
		return false;
	}

	if (b_del_val(&v->domain_b, (unsigned int) val)) {
		v->n_vals--;
		v->min = (unsigned short) b_get_min_val(&v->domain_b);
		v->max = (unsigned short) b_get_max_val(&v->domain_b);

		return true;
	}
	return false;
}

/*
 * Remove the minimum value of the variable singl_v domain from the domain of the v variable
 * Return true if domain changed and false if not
 * v_to_chg - variable to remove value from
 * singl_v - variable with the minimum value to remove from the domain of variable v
 * */
bool v_del_singl_val(var *v_to_chg, var *singl_v) {

	if (singl_v->min < v_to_chg->min || singl_v->min > singl_v->max) {
		return false;
	}
	if (b_del_singl_val(&v_to_chg->domain_b, &singl_v->domain_b)) {
		v_to_chg->n_vals--;
		v_to_chg->min = (unsigned short) b_get_min_val(&v_to_chg->domain_b);
		v_to_chg->max = (unsigned short) b_get_max_val(&v_to_chg->domain_b);

		return true;
	}
	return false;
}

/*
 * Remove values lower than val from v domain
 * Return true if domain changed and false if not
 * v - variable with domain to remove values from
 * val - minimum value to keep at domain
 */
bool v_del_lt(var *v, int val) {
	if (val > v->max) {
		v_clear(v);
		return true;
	}
	if (val > v->min) {
		if (b_del_lt(&v->domain_b, (unsigned int) val)) {
			v->n_vals = (unsigned short) b_cnt_vals(&v->domain_b);
			v->min = (unsigned short) b_get_min_val(&v->domain_b);
			v->max = (unsigned short) b_get_max_val(&v->domain_b);

			return true;

		}
	}
	return false;
}

/*
 * Remove values lower or equal to val from v domain
 * Return true if domain changed and false if not
 * v - variable with domain to remove values from
 * val - bottom value to remove from domain
 */
bool v_del_le(var *v, int val) {
	return v_del_lt(v, ++val);
}

/*
 * Remove values greater than val from v domain
 * Return true if domain changed and false if not
 * v - variable with domain to remove values from
 * val - maximum value to keep at domain
 */
bool v_del_gt(var *v, int val) {
	if (val < v->min) {
		v_clear(v);
		return true;
	}
	if (val < v->max) {
		if (b_del_gt(&v->domain_b, (unsigned int) val)) {
			v->n_vals = (unsigned short) b_cnt_vals(&v->domain_b);
			v->min = (unsigned short) b_get_min_val(&v->domain_b);
			v->max = (unsigned short) b_get_max_val(&v->domain_b);

			return true;
		}
	}
	return false;
}

/*
 * Remove values greater or equal to val from v domain
 * Return true if domain changed and false if not
 * v - variable with domain to remove values from
 * val - top value to remove from the domain
 */
bool v_del_ge(var *v, int val) {
	return v_del_gt(v, --val);
}

/*
 * Clear all values from the domain of the variable v, except val if present
 * Return true if domain changed and false if not
 * v - variable to clear all values except val
 * val - value to keep on variable domain if present
 */
bool v_del_all_except_val(var *v, int val) {
	if (val < v->min || val > v->max) {
		v_clear(v);
		return true;
	}
	if (b_del_all_except_val(&v->domain_b, (unsigned int) val)) {
		if (!b_is_empty(&v->domain_b)) {
			v->n_vals = 1;
			v->min = (unsigned short) val;
			v->max = (unsigned short) val;
		} else {
			v->n_vals = 0;
		}
		return true;
	}
	return false;
}

/*
 * Copy bitmaps with H_BITS size from host_vs to dev_bs with size H_BITS
 * host_vs - variables where to copy bitmaps from
 * dev_bs - bitmaps to copy to
 * n_bs - number of bitmaps to copy
 */
void vs_copy_host_to_dev(void **dev_bs, var *host_vs, unsigned int n_bs) {
	unsigned int i;

	if (CL_N_WORDS_ == 1) {
		if (CL_WORD_ == 32) {
			unsigned int *dev_domains = (unsigned int*) dev_bs;
#if H_N_WORDS == 1	// host bitmaps are one unsigned int or cl_ulong and device bitmaps are one unsigned int
			for (i = 0; i < n_bs; i++) {
				dev_domains[i] = (unsigned int)host_vs[i].domain_b;
			}
#else	// host bitmaps are an array of unsigned int or cl_ulong and device bitmaps are one unsigned int
			for (i = 0; i < n_bs; i++) {
				dev_domains[i] = (unsigned int) host_vs[i].domain_b[0];
			}
#endif
		} else {
			cl_ulong *dev_domains = (cl_ulong*) dev_bs;
#if H_N_WORDS == 1	// host bitmaps are one cl_ulong and device bitmaps are one cl_ulong
			for (i = 0; i < n_bs; i++) {
				dev_domains[i] = host_vs[i].domain_b;
			}
#else
			if (H_WORD == 32) {	// host bitmaps are an array of unsigned int and device bitmaps are one cl_ulong
				for (i = 0; i < n_bs; i++) {
					dev_domains[i] = ((cl_ulong) host_vs[i].domain_b[1] << 32) | ((cl_ulong) host_vs[i].domain_b[0]);
				}
			} else {	// host bitmaps are an array of cl_ulong and device bitmaps are one cl_ulong
				for (i = 0; i < n_bs; i++) {
					dev_domains[i] = host_vs[i].domain_b[0];
				}
			}
#endif
		}
	} else {
		if (CL_WORD_ == 32) {
#if H_N_WORDS == 1 && H_WORD == 64	// host bitmaps are one cl_ulong and device bitmaps are two unsigned int
			unsigned int* dev_domains = (unsigned int*)dev_bs;
			for (i = 0; i < n_bs; i++) {
				dev_domains[i * 2 + 1] = (unsigned int)(host_vs[i].domain_b >> 32);
				dev_domains[i * 2] = (unsigned int)(host_vs[i].domain_b);
			}
#elif H_N_WORDS > 1 && H_WORD == 32	// host and device bitmaps are an array of unsigned int
			unsigned int* dev_domains = (unsigned int*)dev_bs;
			unsigned int j;
			for (i = 0; i < n_bs; i++) {
				for (j = 0; j < CL_N_WORDS_; j++) {
					dev_domains[i * CL_N_WORDS_ + j] = host_vs[i].domain_b[j];
				}
			}
#elif H_N_WORDS > 1 && H_WORD == 64	// host bitmaps are an array of cl_ulong and device bitmaps are an array of unsigned int
			unsigned int *dev_domains = (unsigned int*) dev_bs;
			unsigned int j;
			for (i = 0; i < n_bs; i++) {
				for (j = 0; j < CL_N_WORDS_ / 2; j++) {
					dev_domains[i * CL_N_WORDS_ + j * 2 + 1] = (unsigned int) (host_vs[i].domain_b[j] >> 32);
					dev_domains[i * CL_N_WORDS_ + j * 2] = (unsigned int) (host_vs[i].domain_b[j]);
				}
			}
			// if device bitmaps are an odd array of unsigned int add the last one
			if (CL_N_WORDS_ % 2 != 0) {
				for (i = 0; i < n_bs; i++) {
					dev_domains[i * CL_N_WORDS_ + j] = (unsigned int) (host_vs[i].domain_b[j]);
				}
			}
#endif
		} else {
#if H_N_WORDS > 1
			unsigned int j;
			cl_ulong *dev_domains = (cl_ulong*) dev_bs;
#if H_WORD == 32	// host bitmaps are an array of unsigned int and device bitmaps are an array of cl_ulong
			for (i = 0; i < n_bs; i++) {
				for (j = 0; j < CL_N_WORDS_; j++) {
					dev_domains[i * CL_N_WORDS_ + j] = ((cl_ulong)host_vs[i].domain_b[j * 2 + 1] << 32) | ((cl_ulong)host_vs[i].domain_b[j * 2]);
				}
			}
#else	// host and device bitmaps are an array of cl_ulong
			for (i = 0; i < n_bs; i++) {
				for (j = 0; j < CL_N_WORDS_; j++) {
					dev_domains[i * CL_N_WORDS_ + j] = host_vs[i].domain_b[j];
				}
			}
#endif
#endif
		}
	}
}

/*
 * Copy bitmaps with CL_BITS size from dev_bs to the variables in host_vs that contains domains with size CL_BITS
 * host_vs - variables that contains the bitmaps to copy to
 * dev_bs - bitmaps to copy from
 * n_bs - number of bitmaps to copy
 */
void vs_copy_dev_to_host(var *host_vs, void **dev_bs, unsigned int n_bs) {
	unsigned int i;

	if (CL_N_WORDS_ == 1) {
		if (CL_WORD_ == 32) {
			unsigned int *dev_domains = (unsigned int*) dev_bs;
#if H_N_WORDS == 1	// host bitmaps are one unsigned int or cl_ulong and device bitmaps are one unsigned int
			for (i = 0; i < n_bs; i++) {
				host_vs[i].domain_b = (H_WORD_TYPE)dev_domains[i];
			}
#else	// host bitmaps are an array of unsigned int or cl_ulong and device bitmaps are one unsigned int
			for (i = 0; i < n_bs; i++) {
				host_vs[i].domain_b[0] = (H_WORD_TYPE) dev_domains[i];
			}
#endif
		} else {
			cl_ulong *dev_domains = (cl_ulong*) dev_bs;
#if H_N_WORDS == 1	// host bitmaps are one cl_ulong and device bitmaps are one cl_ulong
			for (i = 0; i < n_bs; i++) {
				host_vs[i].domain_b = dev_domains[i];
			}
#else
			if (H_WORD == 32) {	// host bitmaps are an array of unsigned int and device bitmaps are one cl_ulong
				for (i = 0; i < n_bs; i++) {
					host_vs[i].domain_b[1] = (H_WORD_TYPE) (dev_domains[i] >> 32);
					host_vs[i].domain_b[0] = (H_WORD_TYPE) (dev_domains[i]);
				}
			} else {	// host bitmaps are an array of cl_ulong and device bitmaps are one cl_ulong
				for (i = 0; i < n_bs; i++) {
					host_vs[i].domain_b[0] = dev_domains[i];
				}
			}
#endif
		}
	} else {
		if (CL_WORD_ == 32) {
#if H_N_WORDS == 1 && H_WORD == 64	// host bitmaps are one cl_ulong and device bitmaps are two unsigned int
			unsigned int* dev_domains = (unsigned int*)dev_bs;
			for (i = 0; i < n_bs; i++) {
				host_vs[i].domain_b = ((cl_ulong)dev_domains[i * 2 + 1] << 32) | ((cl_ulong)dev_domains[i * 2]);
			}
#elif H_N_WORDS > 1 && H_WORD == 32	// host and device bitmaps are an array of unsigned int
			unsigned int* dev_domains = (unsigned int*)dev_bs;
			unsigned int j;
			for (i = 0; i < n_bs; i++) {
				for (j = 0; j < CL_N_WORDS_; j++) {
					host_vs[i].domain_b[j] = dev_domains[i * CL_N_WORDS_ + j];
				}
			}
#elif H_N_WORDS > 1 && H_WORD == 64	// host bitmaps are an array of cl_ulong and device bitmaps are an array of unsigned int
			unsigned int *dev_domains = (unsigned int*) dev_bs;
			unsigned int j;
			for (i = 0; i < n_bs; i++) {
				for (j = 0; j < CL_N_WORDS_ / 2; j++) {
					host_vs[i].domain_b[j] = ((cl_ulong) dev_domains[i * CL_N_WORDS_ + j * 2 + 1] << 32) | ((cl_ulong) dev_domains[i * CL_N_WORDS_ + j * 2]);
				}
			}
			// if device bitmaps are an odd array of unsigned int add the last one
			if (CL_N_WORDS_ % 2 != 0) {
				for (i = 0; i < n_bs; i++) {
					host_vs[i].domain_b[j] |= ((cl_ulong) dev_domains[i * CL_N_WORDS_ + j] << 32);
				}
			}
#endif
		} else {
#if H_N_WORDS > 1
			unsigned int j;
			cl_ulong *dev_domains = (cl_ulong*) dev_bs;
#if H_WORD == 32	// host bitmaps are an array of unsigned int and device bitmaps are an array of cl_ulong
			for (i = 0; i < n_bs; i++) {
				for (j = 0; j < CL_N_WORDS_; j++) {
					host_vs[i].domain_b[j * 2 + 1] = (H_WORD_TYPE)(dev_domains[i * CL_N_WORDS_ + j] >> 32);
					host_vs[i].domain_b[j * 2] = (H_WORD_TYPE)(dev_domains[i * CL_N_WORDS_ + j]);
				}
			}
#else	// host and device bitmaps are an array of cl_ulong
			for (i = 0; i < n_bs; i++) {
				for (j = 0; j < CL_N_WORDS_; j++) {
					host_vs[i].domain_b[j] = dev_domains[i * CL_N_WORDS_ + j];
				}
			}
#endif
#endif
		}
	}

	for (i = 0; i < n_bs; i++) {
		host_vs[i].max = (unsigned short) b_get_max_val(&host_vs[i].domain_b);
		host_vs[i].min = (unsigned short) b_get_min_val(&host_vs[i].domain_b);
		host_vs[i].n_vals = (unsigned short) b_cnt_vals(&host_vs[i].domain_b);
	}
}

/*
 * Reset and return the count of the number of variables from vs vector that might be labeled
 * vs - vector of variables to count variables that might be labeled
 * n_vs - number of variables in vs vector
 */
int vs_cnt_vs_to_label(var *vs, unsigned int n_vs) {
	unsigned int i;
	int count = 0;

	for (i = 0; i < n_vs; i++) {
		if (vs[i].to_label && vs[i].n_vals == 1) {
			vs[i].to_label = false;
		}
		if (vs[i].to_label) {
			count++;
		}
	}
	return count;
}

/*
 * Add one more constraint to the received variable
 * v - variable constrained by the received constraint
 * c - constraint that constrain the received variable
 */
void v_add_constr(var *v, constr *c) {
	unsigned int i;

	for (i = 0; i < v->n_cs; i++) {
		if (v->cs[i]->c_id == c->c_id) {
			return;
		}
	}

	int n_cs = v->n_cs + 1;

	constr **cs = (constr**) malloc((unsigned long) n_cs * sizeof(constr*));

	for (i = 0; i < v->n_cs; i++) {
		cs[i] = v->cs[i];
	}
	cs[i] = c;

	v->n_cs = (unsigned short) n_cs;
	free(v->cs);
	v->cs = cs;
}

/*
 * remove constraint from the list of constraints that constrain the variable
 * v - variable constrained by the received constraints
 * cs - list of constraints that constrain the received variable
 */
void v_rem_constr(var *v, constr *cs) {
	constr **old_cs_list = v->cs;
	int ctr = 0;	// number of times the constraint appear in the variable
	int i, j;

	j = 0;
	for (i = 0; i < v->n_cs; i++) {
		if (old_cs_list[i]->c_id == cs->c_id) {

			ctr++;
		}
	}

	v->cs = malloc((unsigned long) (v->n_cs - ctr) * sizeof(constr*));

	j = 0;
	for (i = 0; i < v->n_cs; i++) {
		if (old_cs_list[i]->c_id != cs->c_id) {

			v->cs[j++] = old_cs_list[i];
		}
	}

	free(old_cs_list);
	v->n_cs = (unsigned short) j;
}

/*
 * Return the count of all constraints that constrain a variables vector
 * vs - vector of variables to count constraints
 * n_vs - number of variables in vs vector
 * */
unsigned int vs_cnt_cs(var *vs, unsigned int n_vs) {
	unsigned int i;
	unsigned int cnt = 0;

	for (i = 0; i < n_vs; i++) {
		cnt += vs[i].n_cs;
	}
	return cnt;
}

/*
 * Sort all the CSP variables, placing first the ones to be labeled
 */
void vs_sort_label_first() {
	VS_AUX = (var*) malloc(N_VS * (sizeof(var)));
	unsigned int *ids = malloc(N_VS * (sizeof(unsigned int)));

	int vs_ctr = 0;
	bool opt_v_id_changed = false;
	unsigned int i, j;

	// sort by labeling
	for (i = 0; i < N_VS; i++) {
		if (VS[i].to_label) {

			if (VS[i].n_vals == 1) {
				VS[i].to_label = false;

			} else {
				vs_copy(&VS_AUX[vs_ctr], &VS[i], 1);
				ids[VS[i].v_id] = (unsigned int) vs_ctr;

				vs_ctr++;
			}
		}
	}
	for (i = 0; i < N_VS; i++) {
		if (!VS[i].to_label) {
			vs_copy(&VS_AUX[vs_ctr], &VS[i], 1);
			ids[VS[i].v_id] = (unsigned int) vs_ctr;

			vs_ctr++;
		}
	}

	// update v_id
	for (i = 0; i < N_VS; i++) {

		if (WORK == OPT && !opt_v_id_changed && VS_AUX[i].v_id_print == VAR_ID_TO_OPT) {
			opt_v_id_changed = true;
			VAR_ID_TO_OPT = i;
		}

		VS_AUX[i].v_id = (unsigned short) i;
	}

	for (i = 0; i < N_CS; i++) {
		for (j = 0; j < CS[i].n_c_vs; j++) {
			CS[i].c_vs[j] = &VS_AUX[ids[CS[i].c_vs[j]->v_id]];
		}
		if (CS[i].reified) {
			CS[i].reif_v_id = ids[VS[CS[i].reif_v_id].v_id];
		}
	}

	free(VS);
	VS = (var*) malloc(N_VS * (sizeof(var)));
	vs_copy(VS, VS_AUX, N_VS);

	for (i = 0; i < N_CS; i++) {
		for (j = 0; j < CS[i].n_c_vs; j++) {
			CS[i].c_vs[j] = &VS[CS[i].c_vs[j]->v_id];
		}
	}

	free(VS_AUX);
	free(ids);
}

/*
 * Sort all the CSP variables, placing first the ones to be labeled and from those, the ones that have more values on their domains
 */
void vs_sort_label_more_vals_first() {
	VS_AUX = (var*) malloc(N_VS * (sizeof(var)));
	VS_AUX2 = (var*) malloc(N_VS * (sizeof(var)));
	unsigned int n_vs_to_label = (unsigned int) vs_cnt_vs_to_label(VS, N_VS);
	unsigned int *ids = malloc(N_VS * (sizeof(unsigned int)));
	int max_vals;
	unsigned int max_vals_v_id = 0;
	bool opt_v_id_changed = false;
	int vs_ctr = 0;
	unsigned int i, j;

	// sort by labeling
	for (i = 0; i < N_VS; i++) {
		if (VS[i].to_label) {
			vs_copy(&VS_AUX[vs_ctr], &VS[i], 1);
			ids[VS[i].v_id] = (unsigned int) vs_ctr;

			vs_ctr++;
		}
	}
	for (i = 0; i < N_VS; i++) {
		if (!VS[i].to_label) {
			vs_copy(&VS_AUX[vs_ctr], &VS[i], 1);
			ids[VS[i].v_id] = (unsigned int) vs_ctr;

			vs_ctr++;
		}
	}

	// sort by less numbers on the domain
	vs_ctr = 0;
	for (i = 0; i < n_vs_to_label; i++) {
		max_vals = -1;
		for (j = 0; j < n_vs_to_label; j++) {
			if (VS_AUX[j].n_vals > max_vals) {
				max_vals = VS_AUX[j].n_vals;
				max_vals_v_id = j;
			}
		}

		vs_copy(&VS_AUX2[vs_ctr], &VS_AUX[max_vals_v_id], 1);
		VS_AUX[max_vals_v_id].n_vals = 0;

		vs_ctr++;
	}
	for (i = n_vs_to_label; i < N_VS; i++) {
		vs_copy(&VS_AUX2[i], &VS_AUX[i], 1);
	}

	// update v_id
	for (i = 0; i < N_VS; i++) {

		if (WORK == OPT && !opt_v_id_changed && VS_AUX[i].v_id_print == VAR_ID_TO_OPT) {
			opt_v_id_changed = true;
			VAR_ID_TO_OPT = i;
		}

		VS_AUX[i].v_id = (unsigned short) i;
	}

	for (i = 0; i < N_CS; i++) {
		for (j = 0; j < CS[i].n_c_vs; j++) {
			CS[i].c_vs[j] = &VS_AUX[ids[CS[i].c_vs[j]->v_id]];
		}
		if (CS[i].reified) {
			CS[i].reif_v_id = ids[VS[CS[i].reif_v_id].v_id];
		}
	}

	free(VS);
	VS = (var*) malloc(N_VS * (sizeof(var)));
	vs_copy(VS, VS_AUX, N_VS);

	for (i = 0; i < N_CS; i++) {
		for (j = 0; j < CS[i].n_c_vs; j++) {
			CS[i].c_vs[j] = &VS[CS[i].c_vs[j]->v_id];
		}
	}

	free(VS_AUX);
	free(ids);
}

/*
 * Sort all the CSP variables, placing first the ones to be labeled and from those, the ones that have less values on their domains
 */
void vs_sort_label_less_vals_first() {
	VS_AUX = (var*) malloc(N_VS * (sizeof(var)));
	VS_AUX2 = (var*) malloc(N_VS * (sizeof(var)));
	unsigned int n_vs_to_label = (unsigned int) vs_cnt_vs_to_label(VS, N_VS);
	unsigned int *ids = malloc(N_VS * (sizeof(unsigned int)));
	int min_vals;
	unsigned int min_vals_v_id = 0;
	bool opt_v_id_changed = false;
	int vs_ctr = 0;
	unsigned int i, j;

	// sort by labeling
	for (i = 0; i < N_VS; i++) {
		if (VS[i].to_label) {
			vs_copy(&VS_AUX[vs_ctr], &VS[i], 1);
			ids[VS[i].v_id] = (unsigned int) vs_ctr;

			vs_ctr++;
		}
	}
	for (i = 0; i < N_VS; i++) {
		if (!VS[i].to_label) {
			vs_copy(&VS_AUX[vs_ctr], &VS[i], 1);
			ids[VS[i].v_id] = (unsigned int) vs_ctr;

			vs_ctr++;
		}
	}

	// sort by less numbers on the domain
	vs_ctr = 0;
	for (i = 0; i < n_vs_to_label; i++) {
		min_vals = (int) D_MAX + 2;
		for (j = 0; j < n_vs_to_label; j++) {
			if (VS_AUX[j].n_vals < min_vals) {
				min_vals = VS_AUX[j].n_vals;
				min_vals_v_id = j;
			}
		}

		vs_copy(&VS_AUX2[vs_ctr], &VS_AUX[min_vals_v_id], 1);
		VS_AUX[min_vals_v_id].n_vals = (unsigned short) (D_MAX + 2);

		vs_ctr++;
	}
	for (i = n_vs_to_label; i < N_VS; i++) {
		vs_copy(&VS_AUX2[i], &VS_AUX[i], 1);
	}

	// update v_id
	for (i = 0; i < N_VS; i++) {

		if (WORK == OPT && !opt_v_id_changed && VS_AUX[i].v_id_print == VAR_ID_TO_OPT) {
			opt_v_id_changed = true;
			VAR_ID_TO_OPT = i;
		}

		VS_AUX[i].v_id = (unsigned short) i;
	}

	for (i = 0; i < N_CS; i++) {
		for (j = 0; j < CS[i].n_c_vs; j++) {
			CS[i].c_vs[j] = &VS_AUX[ids[CS[i].c_vs[j]->v_id]];
		}
		if (CS[i].reified) {
			CS[i].reif_v_id = ids[VS[CS[i].reif_v_id].v_id];
		}
	}

	free(VS);
	VS = (var*) malloc(N_VS * (sizeof(var)));
	vs_copy(VS, VS_AUX, N_VS);

	for (i = 0; i < N_CS; i++) {
		for (j = 0; j < CS[i].n_c_vs; j++) {
			CS[i].c_vs[j] = &VS[CS[i].c_vs[j]->v_id];
		}
	}

	free(VS_AUX);
	free(ids);
}

/*
 * Sort constraints of all variables by the most common type of constraint
 * vs - vector of variables
 * n_vs - number of variables in vs vector
 */
void vs_sort_constr(var *vs, unsigned int n_vs) {
	unsigned int cs_kind_cnt[N_C_TYPES];	// Constraints kind counter
	unsigned int cs_kind_sorted[N_C_TYPES];	// Constraints kind counter
	unsigned int n_c_kind = 0;	// number of constraints of a kind
	unsigned int idx = 0;
	unsigned int i, j;

	for (i = 0; i < N_C_TYPES; i++) {
		cs_kind_cnt[i] = 0;
	}

	for (i = 0; i < n_vs; i++) {
		for (j = 0; j < vs[i].n_cs; j++) {
			cs_kind_cnt[vs[i].cs[j]->kind]++;
		}
	}

	for (i = 0; i < N_C_TYPES; i++) {
		for (j = 0; j < N_C_TYPES; j++) {
			if (cs_kind_cnt[j] > n_c_kind) {
				idx = j;
				n_c_kind = cs_kind_cnt[j];
			}
		}
		cs_kind_sorted[i] = idx;
		cs_kind_cnt[idx] = 0;
		idx = 0;
		n_c_kind = 0;
	}

	unsigned int cs_new_idx = 0;
	unsigned int cs_kind_sorted_idx = 0;
	for (i = 0; i < n_vs; i++) {
		constr **cs_new = (constr**) malloc(vs[i].n_cs * sizeof(constr**));
		cs_new_idx = 0;
		cs_kind_sorted_idx = 0;

		while (cs_new_idx < vs[i].n_cs) {
			for (j = 0; j < vs[i].n_cs; j++) {
				if (vs[i].cs[j]->kind == cs_kind_sorted[cs_kind_sorted_idx]) {
					cs_new[cs_new_idx++] = vs[i].cs[j];
				}
			}
			cs_kind_sorted_idx++;
		}

		free(vs[i].cs);
		vs[i].cs = cs_new;
	}
}

/*
 * Return the single value of the variable with the ID v_id
 * v_id - ID of the variable to return single value from
 */
int v_get_value(unsigned int v_id) {
	return VS[v_id].min;
}

/*
 * Return the minimum value of the variable with the ID v_id
 * v_id - ID of the variable to return minimum value from
 */
int v_get_min(unsigned int v_id) {
	return VS[v_id].min;
}

/*
 * Return the maximum value of the variable with the ID v_id
 * v_id - ID of the variable to return maximum value from
 */
int v_get_max(unsigned int v_id) {
	return VS[v_id].max;
}

/*
 * print the single value of the variable whose ID is vs_id
 * v_id - ID of the variable to print single value
 * offset - value to add to the printed value, considering that the first domain value is always zero
 */
void v_print_single_val(unsigned int v_id, unsigned int offset) {
	printf("%u", VS[v_id].min + offset);
}

/*
 * print the single value of the variables whose ID is in vs_id
 * vs_id - array with the ID of the variables to print single value
 * n_vs_id - number of IDs on vs_id array
 * offset - value to add to the printed values, considering that the first domain value is always zero
 */
void vs_print_single_val(unsigned int *vs_id, unsigned int n_vs_id, unsigned int offset) {
	unsigned int i, j;

	for (i = 0; i < n_vs_id - 1; i++) {
		for (j = 0; j < N_VS; j++) {
			if (VS[j].v_id_print == vs_id[i]) {
				printf("%u, ", VS[j].min + offset);
				break;
			}
		}
	}
	for (j = 0; j < N_VS; j++) {
		if (VS[j].v_id_print == vs_id[i]) {
			printf("%u", VS[j].min + offset);
			break;
		}
	}
}

/*
 * print the minimum value of the variables whose ID is in vs_id
 * vs_id - array with the ID of the variables to print minimum
 * n_vs_id - number of IDs on vs_id array
 * offset - value to add to the printed values, considering that the first domain value is always zero
 */
void vs_print_min(unsigned int *vs_id, unsigned int n_vs_id, unsigned int offset) {
	vs_print_single_val(vs_id, n_vs_id, offset);
}

/*
 * print the maximum value of the variables whose ID is in vs_id
 * vs_id - array with the ID of the variables to print maximumvs_print_result
 * n_vs_id - number of IDs on vs_id array
 * offset - value to add to the printed values, considering that the first domain value is always zero
 */
void vs_print_max(unsigned int *vs_id, unsigned int n_vs_id, unsigned int offset) {
	unsigned int i;

	for (i = 0; i < n_vs_id - 1; i++) {
		printf("%u, ", VS[vs_id[i]].max + offset);
	}
	printf("%u\n", VS[vs_id[i]].max + offset);
}

/*
 * print all the variables in the domain of the variables whose ID is in vs_id
 * vs_id - array with the ID of the variables to print values
 * n_vs_id - number of IDs on vs_id array
 * offset - value to add to the printed values, considering that the first domain value is always zero
 */
void vs_print_vals(unsigned int *vs_id, unsigned int n_vs_id, unsigned int offset) {
	unsigned int i, j;

	for (i = 0; i < n_vs_id; i++) {
		for (j = 1; j < VS[vs_id[i]].n_vals; j++) {
			printf("%u,", b_get_nth_val(&VS[vs_id[i]].domain_b, j) + offset);
		}
		printf("%u\n", b_get_nth_val(&VS[vs_id[i]].domain_b, j) + offset);
	}
}

/*
 * print the value of the variable containing the cost of the optimization problem
 * offset - value to add to the printed values, considering that the first domain value is always zero
 */
void v_print_cost(unsigned int offset) {
	printf("Cost = %u\n", VS[VAR_ID_TO_OPT].min + offset);
}

/*
 * print the domain (bitmap/s) of the variables whose ID is in vs_id
 * vs_id - array with the ID of the variables to print domain
 * n_vs_id - number of IDs on vs_id array
 */
void vs_print_domain(unsigned int *vs_id, unsigned int n_vs_id) {
	unsigned int i;

	for (i = 0; i < n_vs_id; i++) {
		b_print_domain(&VS[vs_id[i]].domain_b);
		printf("\n");
	}
}