/*
 * actions.c
 *
 *  Created on: 15/12/2017
 *      Author: pedro
 */

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

// for elapsed time calculation under windows
#if defined(WIN32) || defined(_WIN32) || defined(__WIN32) && !defined(__CYGWIN__)
#include <time.h>
#include <Winsock2.h>
#include <stdint.h>

#else
#include <sys/time.h>
#endif


#include "../../constraints/all_different.h"
#include "../../constraints/at_least.h"
#include "../../constraints/at_most_one.h"
#include "../../constraints/at_most.h"
#include "../../constraints/bool2int.h"
#include "../../constraints/bool_and.h"
#include "../../constraints/bool_clause.h"
#include "../../constraints/bool_or.h"
#include "../../constraints/element_int_var.h"
#include "../../constraints/element_var.h"
#include "../../constraints/element.h"
#include "../../constraints/eq.h"
#include "../../constraints/eq_var.h"
#include "../../constraints/exactly_var.h"
#include "../../constraints/exactly.h"
#include "../../constraints/fake_all_different.h"
#include "../../constraints/ge.h"
#include "../../constraints/gt.h"
#include "../../constraints/le.h"
#include "../../constraints/linear_lt.h"
#include "../../constraints/linear_ne.h"
#include "../../constraints/linear_var.h"
#include "../../constraints/linear.h"
#include "../../constraints/lt.h"
#include "../../constraints/max.h"
#include "../../constraints/maximize.h"
#include "../../constraints/min.h"
#include "../../constraints/minimize.h"
#include "../../constraints/minus_eq.h"
#include "../../constraints/minus_ne.h"
#include "../../constraints/ne.h"
#include "../../constraints/sum_prod.h"
#include "../../constraints/sum_var.h"
#include "../../constraints/sum.h"
#include "../../constraints/var_eq_minus.h"
#include "../../constraints/var_eq_minus_abs.h"
#include "../../constraints/var_eq_plus.h"
#include "../../constraints/var_eq_times.h"
#include "../../constraints.h"
#include "../benchmark.h"
#include "../../config.h"
#include "../../split.h"
#include "../../variables.h"
#include "../../bitmaps.h"


#include "actions.h"

int FZN_OPTIMIZE = 0;	// if the the optimization is for minimize or maximize
int optimize_var_idx;	// Index of the variable to optimize on the array fzn_vars

int search_annot_ctr = 0;	// Number of search annotations already received

int fzn_n_vars = FZN_MAX_ELEMENTS;	// initial maximum number of variables (is extended if needed)
int fzn_n_constrs = FZN_MAX_ELEMENTS;	// initial maximum number of constraints (is extended if needed)
int fzn_n_output_arrays = FZN_MAX_ARRAYS;	// initial maximum number of arrays of variables to print
int fzn_n_arrays = FZN_MAX_ARRAYS;	// initial maximum number of arrays of variables or constants (is extended if needed)
int fzn_n_constr_vals = FZN_MAX_ELEMENTS;	// initial maximum number of values for a constraint (is extended if needed)
int fzn_n_search_annot = FZN_MAX_ELEMENTS;	// initial maximum number of search annotations (is extended if needed)

fzn_object fzn_obj;	// FlatZinc object used until identification as an array, constraint or variable

fzn_var* fzn_vars;	// Flatzinc representation of CSP variables
fzn_var* fzn_vars_aux;	// To extend fzn_vars when needed
int fzn_next_var_posit = 0;	// Index of fzn_vars where to place a new variable

fzn_constr* fzn_constrs;	// Flatzinc representation of a CSP constraint
fzn_constr* fzn_constrs_aux;	// To extend fzn_constrs when needed
int fzn_next_constr_posit = 0;	// Index of fzn_constrs where to place a new flatzinc constraint

fzn_array* fzn_arrays;		// Arrays for storing values that may be the ID of variables or constant values
fzn_array* fzn_arrays_aux;	// To extend fzn_arrays when needed
int fzn_next_array_posit = 0;	// Index of fzn_arrays where to place a new array

fzn_output_array* fzn_output_arrays;	// Arrays for storing the ID of the variables that should be printed
fzn_output_array* fzn_output_arrays_aux;	// To extend fzn_output_arrays when needed
int fzn_next_output_array_posit = 0;	// Index of fzn_output_arrays where to place a new array

fzn_search_annotat* fzn_search_annot;	// For storing the search annotations
fzn_search_annotat* fzn_search_annot_aux;	// To extend fzn_search_annot when needed
int fzn_next_search_annot_posit = 0;	// Index of fzn_search_annot where to place a new one

struct timeval start, end;
char start_time[40];	// for elapse time calculation
char end_time[40];		// for elapse time calculation
char elapsed_time[40];	// for elapse time calculation

/*
 * Translate the flatzinc file to a PHACT representation of a CSP
 */
void parse(char* fzn_file_name) {
	int i;

	gettimeofday(&start, NULL);

	if (!(yyin = fopen(fzn_file_name, "r"))) {
		fprintf(stderr, "The file %s doesn't exist.\n", fzn_file_name);
		exit(-1);
	}

	// create the structures needed for parsing
	fzn_obj.annots = malloc(FZN_MAX_ANNOTATIONS * (sizeof(char*)));
	fzn_obj.elements = malloc(FZN_MAX_ELEMENTS * (sizeof(int)));
	fzn_obj.element_is_var = malloc(FZN_MAX_ELEMENTS * (sizeof(bool)));
	fzn_vars = malloc(fzn_n_vars * sizeof(fzn_var));
	fzn_constrs = malloc(fzn_n_constrs * sizeof(fzn_constr));
	fzn_arrays = malloc(fzn_n_arrays * sizeof(fzn_array));
	fzn_output_arrays = malloc(fzn_n_output_arrays * sizeof(fzn_output_array));
	fzn_search_annot = malloc(fzn_n_search_annot * sizeof(fzn_search_annotat));

	for (i = 0; i < FZN_MAX_ANNOTATIONS; i++) {
		fzn_obj.annots[i] = NULL;
	}

	fzn_obj.element_is_var_aux = NULL;
	fzn_obj.elements_aux = NULL;
	fzn_obj.annots_aux = NULL;
	fzn_obj.next_annot = 0;
	fzn_obj.max_annots = FZN_MAX_ANNOTATIONS;
	fzn_obj.max_elements = FZN_MAX_ELEMENTS;
	fzn_obj.next_element = 0;
	fzn_obj.is_array = false;
	fzn_obj.is_constraint = false;
	fzn_obj.pos_init_2_array = -1;

	if (FZN_VERBOSE) {
		printf("Parsing %s file.\n", fzn_file_name);
	}

	yyparse();

	if (FZN_VERBOSE)
		printf("Finished parsing\n");

	free(fzn_obj.annots);
	free(fzn_obj.elements);
	free(fzn_obj.element_is_var);

	for (i = 0; i < fzn_next_var_posit; i++) {
		if (fzn_vars[i].name != NULL) {
			free(fzn_vars[i].name);
		}
		if (fzn_vars[i].values != NULL) {
			free(fzn_vars[i].values);
		}
	}
	free(fzn_vars);

	for (i = 0; i < fzn_next_constr_posit; i++) {
		if (fzn_constrs[i].next_var_to_add > 0) {
			free(fzn_constrs[i].vars_id);
		}
		if (fzn_constrs[i].next_const_to_add > 0) {
			free(fzn_constrs[i].consts);
		}
		if (fzn_constrs[i].name != NULL) {
			free(fzn_constrs[i].name);
		}
	}

	for (i = 0; i < fzn_next_array_posit; i++) {
		free(fzn_arrays[i].values);

		if (fzn_arrays[i].name != NULL) {
			free(fzn_arrays[i].name);
		}
	}
	free(fzn_arrays);

	for (i = 0; i < fzn_next_output_array_posit; i++) {
		free(fzn_output_arrays[i].vars_id);

		if (fzn_output_arrays[i].name != NULL) {
			free(fzn_output_arrays[i].name);
		}
	}
	free(fzn_output_arrays);

	for (i = 0; i < fzn_next_search_annot_posit; i++) {
		free(fzn_search_annot[i].assign_heur);
		free(fzn_search_annot[i].label_array_name);
		free(fzn_search_annot[i].label_heur);
		free(fzn_search_annot[i].search_strategy);
		free(fzn_search_annot[i].search_type);
	}

	fclose(yyin);
}

/*
 * Explores the CSP to find and print one solution, to count all the solutions or to find and print the best solution
 */
void fzn_solve() {
	unsigned long result = 0;
	bool output_vars;
	int i, j, k;

	N_VS_ORIGINAL = fzn_next_var_posit;
	N_CS_ORIGINAL = fzn_next_constr_posit;

#if FZN_PRINT_CSP
		fzn_print_csp();
#endif

#if FZN_STATS
		fzn_print_stats();
#endif

	// add all the variables marked to be printed to the array of variables to print
	fzn_new_output_array();
	for (i = 0; i < fzn_next_var_posit; i++) {
		if (fzn_vars[i].output_var == true) {
			fzn_add_var_id_to_output_array(i);
		}
	}
	// add all the variables of the arrays marked to be printed to the array of variables to print
	for (i = 0; i < fzn_next_array_posit; i++) {
		if (fzn_arrays[i].output_array) {

			if (fzn_output_arrays[fzn_next_output_array_posit - 1].next_position != 0) {
				fzn_new_output_array();
			}

			if (fzn_arrays[i].name != NULL) {
				if (fzn_output_arrays[fzn_next_output_array_posit - 1].name != NULL) {
					free(fzn_output_arrays[fzn_next_output_array_posit - 1].name);
				}
				fzn_output_arrays[fzn_next_output_array_posit - 1].name = malloc((strlen(fzn_arrays[i].name) + 1) * sizeof(char));
				strcpy(fzn_output_arrays[fzn_next_output_array_posit - 1].name, fzn_arrays[i].name);
			}

			for (j = 0; j < fzn_arrays[i].next_position; j++) {
				fzn_add_var_id_to_output_array(fzn_arrays[i].values[j]);
			}
		}
	}

	// select the variables to label if there is no search annotation in the model and the ones marked for output
	// check if there are any variables set for labeling
	// if none, add all the ones marked for output
	// if none, just add all
	if (fzn_next_search_annot_posit > 0) {

		fzn_init_search_annots();

		for (i = 0; i < fzn_next_var_posit; i++) {

			if (fzn_vars[i].min == fzn_vars[i].max && fzn_vars[i].range == true) {
				fzn_vars[i].to_label = false;

#if FZN_LABEL_DEFINED_VARS
			} else if (fzn_vars[i].is_defined_var) {
				defined_var = true;
				fzn_vars[i].to_label = true;
			}
# else
			}
#endif
		}

#if FZN_LABEL_DEFINED_VARS
		if (defined_var) {
			printf("Some variables marked as \"is_defined_var\" were also set for labeling.\n\n");
		}
#endif

	} else {
		// set output variables for labeling
		output_vars = false;
		for (i = 0; i < fzn_next_var_posit; i++) {

			if (fzn_vars[i].output_var) {
				if (fzn_vars[i].min == fzn_vars[i].max && fzn_vars[i].range == true) {
					fzn_vars[i].to_label = false;

				} else {
					fzn_vars[i].to_label = true;
					output_vars = true;
				}
			}
		}
		for (i = 0; i < fzn_next_array_posit; i++) {

			if (fzn_arrays[i].output_array) {

				for (j = 0; j < fzn_arrays[i].next_position; j++) {

					if (fzn_vars[fzn_arrays[i].values[j]].min == fzn_vars[fzn_arrays[i].values[j]].max && fzn_vars[fzn_arrays[i].values[j]].range == true) {
						fzn_vars[fzn_arrays[i].values[j]].to_label = false;

					} else {
						fzn_vars[fzn_arrays[i].values[j]].to_label = true;
						output_vars = true;
					}
				}
			}
		}

		if (!output_vars) {
			printf("No search annotations and no output variables, so all variables will be set for labeling, which may greatly decrease PHACT performance.\n");

			for (i = 0; i < fzn_next_var_posit; i++) {

				if (fzn_vars[i].min == fzn_vars[i].max && fzn_vars[i].range == true) {
					fzn_vars[i].to_label = false;

				} else {
					fzn_vars[i].to_label = true;
				}
			}

		} else {
			printf("No search annotations, so all the variables marked for output will be set for labeling.\n");
		}
	}

#if FZN_LABEL_ALL_VARS
	fprintf(stderr, "\nSetting all variables for labeling\n");

	for (i = 0; i < fzn_next_var_posit; i++) {

		if (fzn_vars[i].min == fzn_vars[i].max && fzn_vars[i].next_position == 1) {
			fzn_vars[i].to_label = false;
		} else {
			fzn_vars[i].to_label = true;
		}
	}
#endif

	if (FZN_VERBOSE)
			printf("Creating CSP model for PHACT.\n");

	if (WORK == DEFAULT_W) {
		if (FZN_OPTIMIZE == FZN_MINIMIZE || FZN_OPTIMIZE == FZN_MAXIMIZE) {
			WORK = OPT;
			OPTIMIZING = true;
			VS_LOCK = malloc(N_VS * sizeof(var));
			VS_LOCK_BEST = malloc(N_VS * sizeof(var));
		} else {
			COUNTING_SOLUTIONS = true;
			WORK = CNT;
		}
	}

	// Use command line heuristics for labeling and assignment, if existent
	if (LABEL_MODE_COM != DEFAULT_L) {
		LABEL_MODE = LABEL_MODE_COM;
	}
	if (ASSIGN_MODE_COM != DEFAULT_A) {
		ASSIGN_MODE = ASSIGN_MODE_COM;
	}

#if FZN_NE2ALL_DIFF
	int count = 0;
	int first_ne_idx;
	int last_ne_idx;
	bool all_diff = true;
	int l;

	for (i = 0; i < fzn_next_constr_posit; i++) {

		if (strcmp(fzn_constrs[i].name, "int_lin_ne") == 0
				&& fzn_constrs[i].next_const_to_add == 3
				&& fzn_constrs[i].consts[0] == 1
				&& fzn_constrs[i].consts[1] == -1
				&& fzn_constrs[i].consts[2] == 0 ) {

			count = 0;
			for (j = i;
					strcmp(fzn_constrs[j].name, "int_lin_ne") == 0
					&& fzn_constrs[j].next_const_to_add == 3
					&& fzn_constrs[j].consts[0] == 1
					&& fzn_constrs[j].consts[1] == -1
					&& fzn_constrs[j].consts[2] == 0
					&& fzn_constrs[i].vars_id[0] == fzn_constrs[j].vars_id[0]
					; j++) {

				count++;
			}

			// its probably an all different constraint with count + 1 elements
			if (count > 1) {

				count++;
				first_ne_idx = i;
				k = first_ne_idx;

				unsigned int* all_diff_idxs = malloc((count) * sizeof(unsigned int));

				all_diff_idxs[0] = fzn_constrs[k].vars_id[0];
				for (j = 1; j < count; j++) {
					all_diff_idxs[j] = fzn_constrs[k++].vars_id[1];
				}

				l = first_ne_idx;
				for (j = 0; j < count && all_diff; j++) {
					for (k = j + 1; k < count && all_diff; k++) {

						if (strcmp(fzn_constrs[l].name, "int_lin_ne") != 0 || all_diff_idxs[j] != fzn_constrs[l].vars_id[0] || all_diff_idxs[k] != fzn_constrs[l].vars_id[1]) {
							all_diff = false;
						}
						l++;
					}
				}
				last_ne_idx = l;

				if (all_diff) {

					if (FZN_VERBOSE)
							printf("Converting multiple int_lin_ne into an all_different.\n");

					for (j = first_ne_idx; j < last_ne_idx; j++) {
						fzn_constrs[j].ignore = true;
					}

					if (FZN_VERBOSE)
							printf("Creating new all_different (number %d).\n", fzn_next_constr_posit);

					// if the array of constraints is already full, doubles its size
					if (fzn_next_constr_posit == fzn_n_constrs) {

						if (FZN_VERBOSE)
								printf("Extending fzn constraints array.\n");

						fzn_constrs_aux = malloc(fzn_n_constrs * 2 * (sizeof(fzn_constr)));

						fzn_constrs_copy(fzn_constrs_aux, fzn_constrs, fzn_n_constrs);

						free(fzn_constrs);
						fzn_constrs = fzn_constrs_aux;

						fzn_n_constrs *= 2;
					}

					if (FZN_VERBOSE)
						printf("Adding name all_different to constraint.\n");


					// to maintain constraints input order
					free(fzn_constrs[first_ne_idx].vars_id);
					free(fzn_constrs[first_ne_idx].consts);
					free(fzn_constrs[first_ne_idx].name);

					fzn_constrs[first_ne_idx].name = malloc((strlen("all_different") + 1) * sizeof(char));
					strcpy(fzn_constrs[first_ne_idx].name, "all_different");

					fzn_constrs[first_ne_idx].defines_var_idx = -1;
					fzn_constrs[first_ne_idx].boundsR = false;
					fzn_constrs[first_ne_idx].boundsD = false;
					fzn_constrs[first_ne_idx].boundsZ = false;
					fzn_constrs[first_ne_idx].domain = false;
					fzn_constrs[first_ne_idx].priority = false;
					fzn_constrs[first_ne_idx].consts = NULL;
					fzn_constrs[first_ne_idx].vars_id = malloc(count * sizeof(unsigned int));
					fzn_constrs[first_ne_idx].ignore = false;
					fzn_constrs[first_ne_idx].max_consts = 0;
					fzn_constrs[first_ne_idx].max_vars = count;
					fzn_constrs[first_ne_idx].next_const_to_add = 0;
					fzn_constrs[first_ne_idx].next_var_to_add = count;
					fzn_constrs[first_ne_idx].pos_init_2_array = -1;

					for (j = 0; j < count; j++) {

						if (FZN_VERBOSE)
							printf("Adding variable %s to the all_different constraint.\n", fzn_vars[j].name);

						fzn_constrs[first_ne_idx].vars_id[j] = all_diff_idxs[j];
					}

					i = l - 1;
				}
			}
		}
	}
#endif

	// to keep seq_search labeling order
	if (fzn_next_search_annot_posit > 0) {

		for (i = 0; i < fzn_next_search_annot_posit; i++) {

			for (j = 0; j < fzn_next_array_posit; j++) {
				if (fzn_arrays[j].name != NULL && strcmp(fzn_arrays[j].name, fzn_search_annot[i].label_array_name) == 0) {

					for (k = 0; k < fzn_arrays[j].next_position; k++) {
						if (!fzn_vars[fzn_arrays[j].values[k]].ignore && fzn_vars[fzn_arrays[j].values[k]].to_label) {

							fzn_new_csp_var(fzn_arrays[j].values[k]);

						} else if (fzn_vars[fzn_arrays[j].values[k]].ignore) {
							fzn_new_csp_var(fzn_vars[fzn_arrays[j].values[k]].replace_by_v_id);
						}
					}
				}
			}

			for (j = 0; j < fzn_next_var_posit; j++) {
				if (fzn_vars[j].name != NULL && strcmp(fzn_vars[j].name, fzn_search_annot[i].label_array_name) == 0) {

					if (!fzn_vars[j].ignore && fzn_vars[j].to_label) {

						fzn_new_csp_var(j);

					} else if (fzn_vars[j].ignore) {
						fzn_new_csp_var(fzn_vars[j].replace_by_v_id);
					}
				}
			}
		}

		for (i = 0; i < fzn_next_array_posit; i++) {

			if (fzn_arrays[i].output_array) {
				for (j = 0; j < fzn_arrays[i].next_position; j++) {
					if (!fzn_vars[fzn_arrays[i].values[j]].ignore && fzn_vars[fzn_arrays[i].values[j]].to_label) {

						fzn_new_csp_var(fzn_arrays[i].values[j]);

					} else if (fzn_vars[fzn_arrays[i].values[j]].ignore) {
						fzn_new_csp_var(fzn_vars[fzn_arrays[i].values[j]].replace_by_v_id);
					}
				}
			}
		}

		// create the non labeled CSP variables
		for (i = 0; i < fzn_next_var_posit; i++) {
			fzn_new_csp_var(i);
		}

	} else {

		for (i = 0; i < fzn_next_array_posit; i++) {

			if (fzn_arrays[i].output_array) {
				for (j = 0; j < fzn_arrays[i].next_position; j++) {
					if (!fzn_vars[fzn_arrays[i].values[j]].ignore && fzn_vars[fzn_arrays[i].values[j]].to_label) {

						fzn_new_csp_var(fzn_arrays[i].values[j]);

					} else if (fzn_vars[fzn_arrays[i].values[j]].ignore) {
						fzn_new_csp_var(fzn_vars[fzn_arrays[i].values[j]].replace_by_v_id);
					}
				}
			}
		}

		// create the CSP variables
		for (i = 0; i < fzn_next_var_posit; i++) {
			fzn_new_csp_var(i);
		}
	}

	// some duplicated variables are removed, so their links must be updated
	for (i = 0; i < fzn_next_var_posit; i++) {
		if (fzn_vars[i].replace_by_v_id != -1) {
			fzn_vars[i].id = fzn_vars[fzn_vars[i].replace_by_v_id].id;
		}
	}

	// set optimization
	if (FZN_OPTIMIZE == FZN_MINIMIZE) {
		c_minimize(fzn_vars[optimize_var_idx].id);

	} else if (FZN_OPTIMIZE == FZN_MAXIMIZE) {
		c_maximize(fzn_vars[optimize_var_idx].id);
	}

#if FZN_SORT_CONSTR_VARS
	// sort the variables of some constraints for input order
	fzn_sort_constr_vars();
#endif

	// create the CSP constraints
	for (i = 0; i < fzn_next_constr_posit; i++) {
		fzn_new_csp_constr(i);
	}

	if (FZN_VERBOSE) {
		gettimeofday(&end, NULL);
		format_elapsed_time_s_ms(elapsed_time, start.tv_sec, start.tv_usec, end.tv_sec, end.tv_usec);
		format_time_s_ms(start_time, start.tv_sec, start.tv_usec);
		format_time_s_ms(end_time, end.tv_sec, end.tv_usec);
		printf("%s...%s = %s (s.ms) -> CSP model loaded from FlatZinc\n", start_time, end_time, elapsed_time);
	}

	if (FINDING_ONE_SOLUTION) {
		printf("\nFinding one solution for %s.\n", FZN_FILE_NAME);
	} else if (COUNTING_SOLUTIONS) {
		printf("\nCounting all the solutions for %s.\n", FZN_FILE_NAME);
	} else if (OPTIMIZING) {
		printf("\nOptimizing %s.\n", FZN_FILE_NAME);
	}

#if FZN_MAP_FZN2PHACT == 1
	fzn_map_fzn2phact();
#endif

	result = solve_CSP();

	if (FINDING_ONE_SOLUTION && result == 1) {
		printf("Solution:\n");
		for (i = 0; i < fzn_next_output_array_posit; i++) {
			if (fzn_output_arrays[i].name != NULL) {
				printf("%s = {", fzn_output_arrays[i].name);

				for (j = 0; j < fzn_output_arrays[i].next_position - 1; j++) {

					// due to possible variables sorting
					for (k = 0; k < (int)N_VS; k++) {
						if (VS[k].v_id_print == fzn_vars[fzn_output_arrays[i].vars_id[j]].id) {
							v_print_single_val(k, 0);
							break;
						}
					}
					printf(", ");
				}
				// due to possible variables sorting
				for (k = 0; k < (int)N_VS; k++) {
					if (VS[k].v_id_print == fzn_vars[fzn_output_arrays[i].vars_id[j]].id) {
						v_print_single_val(k, 0);
						break;
					}
				}
				printf("}\n");

			} else {
				for (j = 0; j < fzn_output_arrays[i].next_position; j++) {

					// due to possible variables sorting
					for (k = 0; k < (int)N_VS; k++) {

						if (VS[k].v_id_print == fzn_vars[fzn_output_arrays[i].vars_id[j]].id) {

							if (fzn_vars[fzn_output_arrays[i].vars_id[j]].name != NULL) {
								printf("%s = ", fzn_vars[fzn_output_arrays[i].vars_id[j]].name);
							}

							v_print_single_val(k, 0);
							break;
						}
					}
					printf(";\n");
				}
			}
		}

	} else if (COUNTING_SOLUTIONS) {
		printf("%lu solution(s) found\n", result);

	} else if (OPTIMIZING && result == 1) {

		printf("Best solution:\n");
		for (i = 0; i < fzn_next_output_array_posit; i++) {
			if (fzn_output_arrays[i].name != NULL) {
				printf("%s = {", fzn_output_arrays[i].name);

				for (j = 0; j < fzn_output_arrays[i].next_position - 1; j++) {

					// due to possible variables sorting
					for (k = 0; k < (int)N_VS; k++) {
						if (VS[k].v_id_print == fzn_vars[fzn_output_arrays[i].vars_id[j]].id) {
							v_print_single_val(k, 0);
							break;
						}
					}
					printf(", ");
				}
				for (k = 0; k < (int)N_VS; k++) {
					if (VS[k].v_id_print == fzn_vars[fzn_output_arrays[i].vars_id[j]].id) {
						v_print_single_val(k, 0);
						break;
					}
				}
				printf("}\n");
			} else {
				for (j = 0; j < fzn_output_arrays[i].next_position; j++) {

					// due to possible variables sorting
					for (k = 0; k < (int)N_VS; k++) {

						if (VS[k].v_id_print == fzn_vars[fzn_output_arrays[i].vars_id[j]].id) {

							if (fzn_vars[fzn_output_arrays[i].vars_id[j]].name != NULL) {
								printf("%s = ", fzn_vars[fzn_output_arrays[i].vars_id[j]].name);
							}

							v_print_single_val(k, 0);
							break;
						}
					}
					printf(";\n");
				}
			}
		}
		printf("\n");
		v_print_cost(0);

	} else {
		printf("No solution found.\n");
	}
}

/*
 * Add a new value to the current flatzinc object
 * val - value to add
 */
void fzn_add_val_to_object(int val) {

	if (FZN_VERBOSE)
		printf("Adding value %d to element number %d of fzn_obj.\n", val, fzn_obj.next_element);

	fzn_extend_object_elements();

	fzn_obj.elements[fzn_obj.next_element] = val;
	fzn_obj.element_is_var[fzn_obj.next_element] = false;

	fzn_obj.next_element++;
}

/*
 * Add a new variable to the current flatzinc object
 * name - Name of the variable to add to the object
 */
void fzn_add_var_or_array_to_object(char* name) {
	int i, j;

	fzn_extend_object_elements();

	for (i = 0; i < fzn_next_var_posit; i++) {
		if (fzn_vars[i].name != NULL && strcmp(fzn_vars[i].name, name) == 0) {

			if (FZN_VERBOSE)
				printf("Adding variable %s to element number %d fzn_obj.\n", name, fzn_obj.next_element);

			fzn_obj.element_is_var[fzn_obj.next_element] = true;
			fzn_obj.elements[fzn_obj.next_element] = i;
			fzn_obj.next_element++;

			break;
		}
	}

	if (i == fzn_next_var_posit) {
		for (i = 0; i < fzn_next_array_posit; i++) {

			if (fzn_arrays[i].name != NULL && strcmp(fzn_arrays[i].name, name) == 0) {

				if (FZN_VERBOSE)
					printf("Adding array %s to fzn_obj.\n", name);

				if (fzn_arrays[i].var_array) {
					for (j = 0; j < fzn_arrays[i].next_position; j++) {

						fzn_extend_object_elements();

						if (FZN_VERBOSE)
							printf("Adding variable ID %d from array %s to element number %d of fzn_obj.\n", fzn_arrays[i].values[j], name,
									fzn_obj.next_element);

						fzn_obj.element_is_var[fzn_obj.next_element] = true;
						fzn_obj.elements[fzn_obj.next_element] = fzn_arrays[i].values[j];
						fzn_obj.next_element++;
					}
				} else {
					for (j = 0; j < fzn_arrays[i].next_position; j++) {

						fzn_extend_object_elements();

						if (FZN_VERBOSE)
							printf("Adding value %d from array %s to element number %d of fzn_obj.\n", fzn_arrays[i].values[j], name,
									fzn_obj.next_element);

						fzn_obj.element_is_var[fzn_obj.next_element] = false;
						fzn_obj.elements[fzn_obj.next_element] = fzn_arrays[i].values[j];
						fzn_obj.next_element++;
					}
				}
				break;
			}
		}

		if (i == fzn_next_array_posit) {
			fprintf(stderr, "\n Error: variable or array name not found when adding it to a fzn_obj.\n");
			exit(-1);
		}
	}
}

/*
 * Define fzn_obj range as true or false
 */
void fzn_set_fzn_obj_range(bool range) {

	if (FZN_VERBOSE)
		printf("Setting current fzn_obj range as %d.\n", range);

	fzn_obj.range = range;
}

/*
 * Add an annotation to the current flatzinc object
 */
void fzn_add_annot_to_object(char* annot) {
	int i;

	if (fzn_obj.next_annot == fzn_obj.max_annots) {

		if (FZN_VERBOSE)
			printf("Extending annotations array of fzn_obj.\n");

		fzn_obj.annots_aux = malloc(fzn_obj.max_annots * 2 * (sizeof(char*)));

		for (i = 0; i < fzn_obj.next_annot; i++) {
			fzn_obj.annots_aux[i] = fzn_obj.annots[i];
		}

		free(fzn_obj.annots);
		fzn_obj.annots = fzn_obj.annots_aux;

		fzn_obj.max_annots *= 2;
	}

	if (FZN_VERBOSE)
		printf("Adding annotation %s, as the annotation number %d to fzn_obj.\n", annot, fzn_obj.next_annot);

	if (strcmp(annot, "bool") == 0) {

		if (FZN_VERBOSE)
			printf("Setting fzn_obj as bool.\n");

		fzn_obj.is_bool = true;

	} else if (strcmp(annot, "int_search") == 0 || strcmp(annot, "bool_search") == 0) {

		fzn_obj.annots[fzn_obj.next_annot] = malloc((strlen(annot) + 1) * sizeof(char));
		strcpy(fzn_obj.annots[fzn_obj.next_annot], annot);

		fzn_obj.next_annot++;

		fzn_add_fzn_obj_search_annot();

	} else if (strcmp(annot, "float_search") == 0 || strcmp(annot, "set_search") == 0) {
			fprintf(stderr, "PHACT can only work with \"int_search\" or \"bool_search\" annotations (not %s).\n", annot);
			exit(-1);

	} else {
		fzn_obj.annots[fzn_obj.next_annot] = malloc((strlen(annot) + 1) * sizeof(char));
		strcpy(fzn_obj.annots[fzn_obj.next_annot], annot);

		fzn_obj.next_annot++;
	}
}

/*
 * identifies the element on the elements array where the second array of the constraint begins
 */
void fzn_set_2array_init_pos() {
	if (fzn_obj.pos_init_2_array == -1) {

		if (FZN_VERBOSE)
			printf("Begin of second array of elements at element number %d.\n", fzn_obj.next_element);

		fzn_obj.pos_init_2_array = fzn_obj.next_element;
	}
}

/*
 * If the array of object elements is already full, doubles its size
 */
void fzn_extend_object_elements() {
	int i;

	if (fzn_obj.next_element == fzn_obj.max_elements) {

		if (FZN_VERBOSE)
			printf("Extending array of elements of fzn_obj.\n");

		fzn_obj.elements_aux = malloc(fzn_obj.max_elements * 2 * (sizeof(int)));
		fzn_obj.element_is_var_aux = malloc(fzn_obj.max_elements * 2 * (sizeof(bool)));

		for (i = 0; i < fzn_obj.next_element; i++) {
			fzn_obj.elements_aux[i] = fzn_obj.elements[i];
			fzn_obj.element_is_var_aux[i] = fzn_obj.element_is_var[i];
		}

		free(fzn_obj.elements);
		free(fzn_obj.element_is_var);

		fzn_obj.elements = fzn_obj.elements_aux;
		fzn_obj.element_is_var = fzn_obj.element_is_var_aux;

		fzn_obj.max_elements *= 2;
	}
}

/*
 * Reset the flatzinc object
 */
void fzn_reset_object_elements() {
	int i = 0;

	if (FZN_VERBOSE)
		printf("Reseting fzn_obj.\n");

	for (i = 0; i < fzn_obj.next_annot; i++) {
		free(fzn_obj.annots[i]);
		fzn_obj.annots[i] = NULL;
	}
	fzn_obj.annots_aux = NULL;
	fzn_obj.element_is_var_aux = NULL;

	fzn_obj.next_annot = 0;
	fzn_obj.next_element = 0;
	fzn_obj.is_array = false;
	fzn_obj.is_constraint = false;
	fzn_obj.is_bool = false;
	fzn_obj.range = true;
	fzn_obj.pos_init_2_array = -1;
}

/*
 * Create a new empty array that will contain constant values or variables IDs
 */
void fzn_new_fzn_obj_array() {
	int i;

	fzn_obj.is_array = true;

	if (FZN_VERBOSE)
		printf("Adding new FZN array (number %d).\n", fzn_next_array_posit);

	// if the array of arrays is full, doubles its size
	if (fzn_next_array_posit == fzn_n_arrays) {
		fzn_arrays_aux = malloc(fzn_n_arrays * 2 * (sizeof(fzn_array)));

		fzn_array_copy(fzn_arrays_aux, fzn_arrays, fzn_n_arrays);
		free(fzn_arrays);
		fzn_arrays = fzn_arrays_aux;

		fzn_n_arrays *= 2;
	}

	fzn_arrays[fzn_next_array_posit].output_var = false;
	fzn_arrays[fzn_next_array_posit].is_defined_var = false;
	fzn_arrays[fzn_next_array_posit].var_is_introduced = false;
	fzn_arrays[fzn_next_array_posit].output_array = false;
	fzn_arrays[fzn_next_array_posit].to_label = true;
	fzn_arrays[fzn_next_array_posit].next_position = 0;
	fzn_arrays[fzn_next_array_posit].values = NULL;
	fzn_arrays[fzn_next_array_posit].max_values = FZN_MAX_ELEMENTS;
	fzn_arrays[fzn_next_array_posit].values_aux = NULL;
	fzn_arrays[fzn_next_array_posit].var_array = true;
	fzn_arrays[fzn_next_array_posit].name = NULL;

	for (i = 0; i < fzn_obj.next_annot; i++) {

		if (fzn_obj.annots[i] == NULL) {
			fprintf(stderr, "Trying to add an annotation number %d that is empty to array number %d.\n", i, fzn_next_array_posit);
			exit(-1);
		}

		if (strcmp(fzn_obj.annots[i], "output_var") == 0) {

			if (FZN_VERBOSE)
				printf("Adding annotation output_var to array.\n");

			fzn_arrays[fzn_next_array_posit].output_var = true;

		} else if (strcmp(fzn_obj.annots[i], "is_defined_var") == 0) {

			if (FZN_VERBOSE)
				printf("Adding annotation is_defined_var to array.\n");

			fzn_arrays[fzn_next_array_posit].is_defined_var = true;

		} else if (strcmp(fzn_obj.annots[i], "var_is_introduced") == 0) {

			if (FZN_VERBOSE)
				printf("Adding annotation var_is_introduced to array.\n");

			fzn_arrays[fzn_next_array_posit].var_is_introduced = true;

		} else if (strcmp(fzn_obj.annots[i], "output_array") == 0) {

			if (FZN_VERBOSE)
				printf("Adding annotation output_array to array.\n");

			fzn_arrays[fzn_next_array_posit].output_array = true;

		} else {
			if (fzn_arrays[fzn_next_array_posit].name == NULL) {

				if (FZN_VERBOSE)
					printf("Adding name %s to array.\n", fzn_obj.annots[i]);

				fzn_arrays[fzn_next_array_posit].name = malloc((strlen(fzn_obj.annots[i]) + 1) * sizeof(char));
				strcpy(fzn_arrays[fzn_next_array_posit].name, fzn_obj.annots[i]);

			} else {
				fprintf(stderr, "Trying to name array with %s when its name is already %s.\n", fzn_arrays[fzn_next_array_posit].name, fzn_obj.annots[i]);
				exit(-1);
			}
		}
	}

	// reset all the array values
	fzn_arrays[fzn_next_array_posit].next_position = fzn_obj.next_element;
	fzn_arrays[fzn_next_array_posit].to_label = false;
	fzn_arrays[fzn_next_array_posit].values = malloc(fzn_obj.next_element * sizeof(int));
	fzn_arrays[fzn_next_array_posit].max_values = fzn_obj.next_element;
	fzn_arrays[fzn_next_array_posit].values_aux = NULL;
	fzn_arrays[fzn_next_array_posit].var_array = false;
	for (i = 0; i < fzn_obj.next_element; i++) {
		if (fzn_obj.element_is_var[i]) {
			fzn_arrays[fzn_next_array_posit].var_array = true;
			break;
		}
	}

	if (fzn_arrays[fzn_next_array_posit].var_array) {
		for (i = 0; i < fzn_obj.next_element; i++) {

			if (fzn_obj.element_is_var[i]) {

				fzn_arrays[fzn_next_array_posit].values[i] = fzn_obj.elements[i];

			} else {
				fzn_arrays[fzn_next_array_posit].values[i] = fzn_new_fzn_obj_var_value(fzn_obj.elements[i]);
			}
		}
	} else {
		for (i = 0; i < fzn_obj.next_element; i++) {
			fzn_arrays[fzn_next_array_posit].values[i] = fzn_obj.elements[i];
		}
	}

	fzn_reset_object_elements();

	fzn_next_array_posit++;
}

/*
 * Adds a variable ID to the last created array
 * name - name of the variable whose ID is to add to the array
 */
void fzn_add_var_to_array(char* var_name) {
	int i, j;

	if (FZN_VERBOSE)
		printf("Adding variable %s to FZN array number %d.\n", var_name, fzn_next_array_posit - 1);

	if (var_name == NULL) {
		fprintf(stderr, "Attempting to add a variable with no name to an array.\n");
		exit(-1);
	}

	// finds the variable with that name to retrieve its ID and adds the ID to the array
	for (i = 0; i < fzn_next_var_posit; i++) {
		if (fzn_vars[i].name != NULL && strcmp(var_name, fzn_vars[i].name) == 0) {

			// if the array of integers is already full, doubles its size
			if (fzn_arrays[fzn_next_array_posit - 1].next_position == fzn_arrays[fzn_next_array_posit - 1].max_values) {
				fzn_arrays[fzn_next_array_posit - 1].values_aux = malloc(fzn_arrays[fzn_next_array_posit - 1].max_values * 2 * (sizeof(int)));

				for (j = 0; j < fzn_arrays[fzn_next_array_posit - 1].max_values; j++) {
					fzn_arrays[fzn_next_array_posit - 1].values_aux[j] = fzn_arrays[fzn_next_array_posit - 1].values[i];
				}

				free(fzn_arrays[fzn_next_array_posit - 1].values);
				fzn_arrays[fzn_next_array_posit - 1].values = fzn_arrays[fzn_next_array_posit - 1].values_aux;

				fzn_arrays[fzn_next_array_posit - 1].max_values *= 2;
			}

			fzn_arrays[fzn_next_array_posit - 1].values[fzn_arrays[fzn_next_array_posit - 1].next_position] = i;
			fzn_arrays[fzn_next_array_posit - 1].next_position++;

			fzn_arrays[fzn_next_array_posit - 1].var_array = true;

			return;
		}
	}

	if (i == fzn_next_var_posit) {
		fprintf(stderr, "Variable name %s not found when adding it to an array.\n", var_name);
		exit(-1);
	}

	if (!fzn_arrays[fzn_next_array_posit - 1].var_array) {

		int val;
		for (i = 0; i < fzn_arrays[fzn_next_array_posit - 1].next_position; i++) {
			val = fzn_arrays[fzn_next_array_posit - 1].values[i];
			fzn_arrays[fzn_next_array_posit - 1].values[i] = fzn_new_fzn_var_range(val, val);
		}

		fzn_arrays[fzn_next_array_posit - 1].var_array = true;
	}
}

/*
 * Adds an integer value to the last created array
 * value - value to add to the array
 */
void fzn_add_val_to_array(int value) {
	int i;

	if (FZN_VERBOSE)
			printf("Adding value/variable %d to FZN array number %d.\n", value, fzn_next_array_posit - 1);

	// if the array of integers is already full, doubles its size
	if (fzn_arrays[fzn_next_array_posit - 1].next_position == fzn_arrays[fzn_next_array_posit - 1].max_values) {
		fzn_arrays[fzn_next_array_posit - 1].values_aux = malloc(fzn_arrays[fzn_next_array_posit - 1].max_values * 2 * (sizeof(int)));

		for (i = 0; i < fzn_arrays[fzn_next_array_posit - 1].max_values; i++) {
			fzn_arrays[fzn_next_array_posit - 1].values_aux[i] = fzn_arrays[fzn_next_array_posit - 1].values[i];
		}

		free(fzn_arrays[fzn_next_array_posit - 1].values);
		fzn_arrays[fzn_next_array_posit - 1].values = fzn_arrays[fzn_next_array_posit - 1].values_aux;

		fzn_arrays[fzn_next_array_posit - 1].max_values *= 2;
	}

	if (fzn_arrays[fzn_next_array_posit - 1].var_array) {
		fzn_arrays[fzn_next_array_posit - 1].values[fzn_arrays[fzn_next_array_posit - 1].next_position] = fzn_new_fzn_var_range(value, value);

	} else {
		// adds the new value to the array
		fzn_arrays[fzn_next_array_posit - 1].values[fzn_arrays[fzn_next_array_posit - 1].next_position] = value;
	}
	fzn_arrays[fzn_next_array_posit - 1].next_position++;
}

/*
 * Copy a Flatzinc array
 * dest - the array from where to copy the fzn_array to
 * src - the array from where to copy the fzn_array from
 * n_arrays - number of fzn_arrays to copy
 */
void fzn_array_copy(fzn_array* dest, fzn_array* src, int n_arrays) {
	int i;

	if (FZN_VERBOSE)
		printf("Copying FZN array.\n");

	for (i = 0; i < n_arrays; i++) {

		dest[i].is_defined_var = src[i].is_defined_var;
		dest[i].max_values = src[i].max_values;
		dest[i].name = src[i].name;
		dest[i].next_position = src[i].next_position;
		dest[i].output_array = src[i].output_array;
		dest[i].output_var = src[i].output_var;
		dest[i].to_label = src[i].to_label;
		dest[i].values = src[i].values;
		dest[i].values_aux = src[i].values_aux;
		dest[i].var_array = src[i].var_array;
		dest[i].var_is_introduced = src[i].var_is_introduced;
	}
}

/*
 * Create a new Flatzinc variable with the minimum and the maximum value of its domain
 * and return the index of the variable in fzn_vars array
 * min - minimum value of the variable domain
 * max - maximum value of the variable domain
 */
int fzn_new_fzn_var_range(int min, int max) {
	int i;

	if (FZN_VERBOSE)
			printf("Creating new FZN variable with range [%d, %d].\n", min, max);

	if (min == max) {
		for (i = 0; i < fzn_next_var_posit; i++) {
			if (fzn_vars[i].min == min && fzn_vars[i].min == fzn_vars[i].max && fzn_vars[i].range == true && fzn_vars[i].name == NULL) {
				return i;
			}
		}
	}

	// if the array of variables is already full, doubles its size
	fzn_vars_extend();

	fzn_vars[fzn_next_var_posit].values = NULL;
	fzn_vars[fzn_next_var_posit].values_aux = NULL;
	fzn_vars[fzn_next_var_posit].next_position = 0;
	fzn_vars[fzn_next_var_posit].max_values = 0;
    fzn_vars[fzn_next_var_posit].range = true;
	fzn_vars[fzn_next_var_posit].defined_by_constr_idx = -1;
    fzn_vars[fzn_next_var_posit].id = -1;
    fzn_vars[fzn_next_var_posit].ignore = false;
    fzn_vars[fzn_next_var_posit].is_defined_var = false;
    fzn_vars[fzn_next_var_posit].max = max;
    fzn_vars[fzn_next_var_posit].min = min;
    fzn_vars[fzn_next_var_posit].name = NULL;
    fzn_vars[fzn_next_var_posit].output_var = false;
    fzn_vars[fzn_next_var_posit].to_label = false;
    fzn_vars[fzn_next_var_posit].replace_by_v_id = -1;
    fzn_vars[fzn_next_var_posit].created = false;
    fzn_next_var_posit++;

    return fzn_next_var_posit - 1;
}

/*
 * Create a new Flatzinc variable with a single value on its domain
 * and return the index of the variable in fzn_vars array
 * val - value of the variable domain
 */
int fzn_new_fzn_obj_var_value(int val) {
	int i;

	if (fzn_obj.is_bool && fzn_obj.is_array != true) {
		fzn_add_val_to_object(0);
		fzn_add_val_to_object(1);
	}

	if (fzn_obj.is_array == true || fzn_obj.is_constraint || fzn_obj.annots[0] == NULL) {

		for (i = 0; i < fzn_next_var_posit; i++) {
			if (fzn_vars[i].min == val && fzn_vars[i].min == fzn_vars[i].max && fzn_vars[i].range == true && fzn_vars[i].name == NULL) {

				if (FZN_VERBOSE)
					printf("New FZN variable with value %d not created, as one already exists.\n", val);

				return i;
			}
		}
	}

	if (FZN_VERBOSE)
		printf("Creating new FZN variable with value %d.\n", val);

	// if the array of variables is already full, doubles its size
	fzn_vars_extend();

	fzn_vars[fzn_next_var_posit].values = NULL;
	fzn_vars[fzn_next_var_posit].values_aux = NULL;
	fzn_vars[fzn_next_var_posit].next_position = 0;
	fzn_vars[fzn_next_var_posit].max_values = 0;
	fzn_vars[fzn_next_var_posit].name = NULL;
    fzn_vars[fzn_next_var_posit].range = true;
	fzn_vars[fzn_next_var_posit].defined_by_constr_idx = -1;
    fzn_vars[fzn_next_var_posit].id = -1;
    fzn_vars[fzn_next_var_posit].ignore = false;
    fzn_vars[fzn_next_var_posit].is_defined_var = false;
    fzn_vars[fzn_next_var_posit].max = val;
    fzn_vars[fzn_next_var_posit].min = val;
    fzn_vars[fzn_next_var_posit].output_var = false;
    fzn_vars[fzn_next_var_posit].to_label = false;
    fzn_vars[fzn_next_var_posit].replace_by_v_id = -1;
    fzn_vars[fzn_next_var_posit].var_is_introduced = false;
    fzn_vars[fzn_next_var_posit].created = false;

    fzn_next_var_posit++;

    return fzn_next_var_posit - 1;
}

/*
 * Create a new Flatzinc variable with the fzn_obj data
 */
int fzn_new_fzn_obj_var() {

	if (fzn_obj.is_bool && fzn_obj.is_array != true) {
		fzn_add_val_to_object(0);
		fzn_add_val_to_object(1);
	}

	int min = fzn_obj.elements[0];
	int max = fzn_obj.elements[1];
	int i;

	if (min == max && (fzn_obj.annots[0] == NULL || fzn_obj.is_array == true || fzn_obj.is_constraint)) {
		for (i = 0; i < fzn_next_var_posit; i++) {
			if (fzn_vars[i].min == min && fzn_vars[i].min == fzn_vars[i].max && fzn_vars[i].range == true && fzn_vars[i].name == NULL) {

				if (FZN_VERBOSE)
					printf("New FZN variable with with range [%d, %d] not created, as one already exists.\n", min, max);

				return i;
			}
		}
	}

	// if the array of variables is already full, doubles its size
	fzn_vars_extend();

	fzn_vars[fzn_next_var_posit].values = NULL;
	fzn_vars[fzn_next_var_posit].values_aux = NULL;
	fzn_vars[fzn_next_var_posit].next_position = 0;
	fzn_vars[fzn_next_var_posit].max_values = 0;
	fzn_vars[fzn_next_var_posit].name = NULL;
    fzn_vars[fzn_next_var_posit].range = true;
	fzn_vars[fzn_next_var_posit].defined_by_constr_idx = -1;
    fzn_vars[fzn_next_var_posit].id = -1;
    fzn_vars[fzn_next_var_posit].ignore = false;
    fzn_vars[fzn_next_var_posit].is_defined_var = false;
    fzn_vars[fzn_next_var_posit].max = -1;
    fzn_vars[fzn_next_var_posit].min = -1;
    fzn_vars[fzn_next_var_posit].output_var = false;
    fzn_vars[fzn_next_var_posit].to_label = false;
    fzn_vars[fzn_next_var_posit].replace_by_v_id = -1;
    fzn_vars[fzn_next_var_posit].var_is_introduced = false;
    fzn_vars[fzn_next_var_posit].created = false;

	for (i = 0; i < fzn_obj.next_annot; i++) {

		if (strcmp(fzn_obj.annots[i], "output_var") == 0) {

			if (FZN_VERBOSE)
				printf("Adding annotation output_var to variable.\n");

			fzn_vars[fzn_next_var_posit].output_var = true;

		} else if (strcmp(fzn_obj.annots[i], "is_defined_var") == 0) {

			if (FZN_VERBOSE)
				printf("Adding annotation is_defined_var to variable.\n");

			fzn_vars[fzn_next_var_posit].is_defined_var = true;

		} else if (strcmp(fzn_obj.annots[i], "var_is_introduced") == 0) {

			if (FZN_VERBOSE)
				printf("Adding annotation var_is_introduced to variable.\n");

			fzn_vars[fzn_next_var_posit].var_is_introduced = true;

		}  else {
			if (fzn_vars[fzn_next_var_posit].name == NULL) {

				if (FZN_VERBOSE)
					printf("Adding name %s to variable.\n", fzn_obj.annots[i]);

				fzn_vars[fzn_next_var_posit].name = malloc((strlen(fzn_obj.annots[i]) + 1) * sizeof(char));
				strcpy(fzn_vars[fzn_next_var_posit].name, fzn_obj.annots[i]);

			} else {
				fprintf(stderr, "Trying to name variable with %s when its name is already %s.\n", fzn_vars[fzn_next_var_posit].name, fzn_obj.annots[i]);
				exit(-1);
			}
		}
	}

    fzn_vars[fzn_next_var_posit].range = fzn_obj.range;

	if (fzn_obj.range) {
		if (FZN_VERBOSE)
			printf("Creating new FZN variable (number %d) with range [%d, %d].\n", fzn_next_var_posit, min, max);

	    fzn_vars[fzn_next_var_posit].max = max;
	    fzn_vars[fzn_next_var_posit].min = min;

	} else {

		if (FZN_VERBOSE)
			printf("Creating new FZN variable (number %d) with values %d...%d.\n", fzn_next_var_posit, fzn_obj.elements[0],
					fzn_obj.elements[fzn_obj.next_element - 1]);

	    fzn_vars[fzn_next_var_posit].values = malloc(fzn_obj.next_element * sizeof(int));
		fzn_vars[fzn_next_var_posit].values_aux = NULL;
		fzn_vars[fzn_next_var_posit].next_position = fzn_obj.next_element;
		fzn_vars[fzn_next_var_posit].max_values = fzn_obj.next_element;

		for (i = 0; i < fzn_obj.next_element; i++) {
			fzn_vars[fzn_next_var_posit].values[i] = fzn_obj.elements[i];
		}

	    // may not be, if value not ordered, but PHACT does it correctly
	    fzn_vars[fzn_next_var_posit].max = fzn_obj.elements[fzn_obj.next_element - 1];
	    fzn_vars[fzn_next_var_posit].min = fzn_obj.elements[0];
	}

	fzn_vars[fzn_next_var_posit].defined_by_constr_idx = -1;
    fzn_vars[fzn_next_var_posit].id = -1;
    fzn_vars[fzn_next_var_posit].to_label = false;
    fzn_vars[fzn_next_var_posit].created = false;

	if (fzn_obj.element_is_var[fzn_obj.next_element - 1]) {
	    fzn_vars[fzn_next_var_posit].ignore = true;
	    fzn_vars[fzn_next_var_posit].replace_by_v_id = fzn_obj.elements[fzn_obj.next_element - 1];

	} else {
	    fzn_vars[fzn_next_var_posit].ignore = false;
	    fzn_vars[fzn_next_var_posit].replace_by_v_id = -1;
	}


    fzn_next_var_posit++;

    fzn_reset_object_elements();

    return fzn_next_var_posit - 1;
}

/*
 * Copy a Flatzinc variable
 * dest - the array from where to copy the variable to
 * src - the array from where to copy the variable from
 * n_vs - number of variables to copy
 */
void fzn_vars_copy(fzn_var* dest, fzn_var* src, int n_vs) {
	int i;

	if (FZN_VERBOSE)
			printf("Copying FZN variable.\n");

	for (i = 0; i < n_vs; i++) {
		dest[i].values = src[i].values;
		dest[i].values_aux = src[i].values_aux;
		dest[i].next_position = src[i].next_position;
		dest[i].max_values = src[i].max_values;
		dest[i].range = src[i].range;
		dest[i].defined_by_constr_idx = src[i].defined_by_constr_idx;
		dest[i].id = src[i].id;
		dest[i].ignore = src[i].ignore;
		dest[i].is_defined_var = src[i].is_defined_var;
		dest[i].max = src[i].max;
		dest[i].min = src[i].min;
		dest[i].name = src[i].name;
		dest[i].output_var = src[i].output_var;
		dest[i].to_label = src[i].to_label;
		dest[i].var_is_introduced = src[i].var_is_introduced;
		dest[i].replace_by_v_id = src[i].replace_by_v_id;
		dest[i].created = src[i].created;
	}
}

/*
 * If the array of variables is already full, doubles its size
 */
void fzn_vars_extend() {

	if (fzn_next_var_posit == fzn_n_vars) {

		if (FZN_VERBOSE)
			printf("Extending FZN variables array.\n");

		fzn_vars_aux = malloc(fzn_n_vars * 2 * (sizeof(fzn_var)));

		fzn_vars_copy(fzn_vars_aux, fzn_vars, fzn_n_vars);

		free(fzn_vars);

		fzn_vars = fzn_vars_aux;

		fzn_n_vars *= 2;
	}
}

/*
 * Save the index of the variable to optimize
 */
void fzn_set_var_to_optimize(char* var_name) {
	int i;

	if (FZN_VERBOSE)
			printf("Preparing optimization.\n");

	// get the ID of the variable with that name
	for (i = 0; i < fzn_next_var_posit; i++) {
		if (fzn_vars[i].name != NULL && strcmp(var_name, fzn_vars[i].name) == 0) {
			optimize_var_idx = i;
			break;
		}
	}
}

/*
 * Create a new empty output array that will contain the IDs of the variable to print
 */
void fzn_new_output_array() {

	if (FZN_VERBOSE)
			printf("Adding new FZN output array (%d).\n", fzn_next_output_array_posit);

	// if the array of output arrays is full, doubles its size
	if (fzn_next_output_array_posit == fzn_n_output_arrays) {
		fzn_output_arrays_aux = malloc(fzn_n_output_arrays * 2 * (sizeof(fzn_output_array)));

		fzn_output_array_copy(fzn_output_arrays_aux, fzn_output_arrays, fzn_n_output_arrays);

		free(fzn_output_arrays);
		fzn_output_arrays = fzn_output_arrays_aux;

		fzn_n_output_arrays *= 2;
	}

	// reset all the array values
	fzn_output_arrays[fzn_next_output_array_posit].max_vars = FZN_MAX_ELEMENTS;
	fzn_output_arrays[fzn_next_output_array_posit].next_position = 0;
	fzn_output_arrays[fzn_next_output_array_posit].vars_id = malloc(FZN_MAX_ELEMENTS * sizeof(unsigned int));
	fzn_output_arrays[fzn_next_output_array_posit].vars_id_aux = NULL;
	fzn_output_arrays[fzn_next_output_array_posit].name = NULL;
	fzn_next_output_array_posit++;
}

/*
 * Copy an output array
 * dest - the array from where to copy the output_array to
 * src - the array from where to copy the output_array from
 * n_arrays - number of output_arrays to copy
 */
void fzn_output_array_copy(fzn_output_array* dest, fzn_output_array* src, int n_arrays) {
	int i;

	if (FZN_VERBOSE)
			printf("Copying FZN output array.\n");

	for (i = 0; i < n_arrays; i++) {
		dest[i].max_vars = src[i].max_vars;
		dest[i].next_position = src[i].next_position;
		dest[i].vars_id = src[i].vars_id;
		dest[i].vars_id_aux = src[i].vars_id_aux;
		dest[i].name = src[i].name;
	}
}

/*
 * Adds a variable ID to the last created output_array
 * v_id - ID of the variable to add to the array
 */
void fzn_add_var_id_to_output_array(unsigned int v_id) {
	int i;

	if (FZN_VERBOSE) {
		if (fzn_vars[v_id].name != NULL) {
			printf("Adding variable ID %d with name %s to FZN output array number %d.\n", v_id, fzn_vars[v_id].name, fzn_next_output_array_posit - 1);

		} else {
			printf("Adding variable ID %d to FZN output array number %d.\n", v_id, fzn_next_output_array_posit - 1);
		}
	}

	// if the array of integers is already full, doubles its size
	if (fzn_output_arrays[fzn_next_output_array_posit - 1].next_position == fzn_output_arrays[fzn_next_output_array_posit - 1].max_vars) {
		fzn_output_arrays[fzn_next_output_array_posit - 1].vars_id_aux = malloc(fzn_output_arrays[fzn_next_output_array_posit - 1].max_vars * 2 * (sizeof(unsigned int)));

		for (i = 0; i < fzn_output_arrays[fzn_next_output_array_posit - 1].max_vars; i++) {
			fzn_output_arrays[fzn_next_output_array_posit - 1].vars_id_aux[i] = fzn_output_arrays[fzn_next_output_array_posit - 1].vars_id[i];
		}

		free(fzn_output_arrays[fzn_next_output_array_posit - 1].vars_id);
		fzn_output_arrays[fzn_next_output_array_posit - 1].vars_id = fzn_output_arrays[fzn_next_output_array_posit - 1].vars_id_aux;

		fzn_output_arrays[fzn_next_output_array_posit - 1].max_vars *= 2;
	}

	// adds the new value to the array
	fzn_output_arrays[fzn_next_output_array_posit - 1].vars_id[fzn_output_arrays[fzn_next_output_array_posit - 1].next_position] = v_id;
	fzn_output_arrays[fzn_next_output_array_posit - 1].next_position++;
}

/*
 * Create a new flatzinc constraint structure
 */
void fzn_new_fzn_obj_constr() {
	int i, j;

	if (FZN_VERBOSE)
			printf("Creating new FZN constraint (number %d).\n", fzn_next_constr_posit);

	fzn_obj.is_constraint = true;

	// if the array of constraints is already full, doubles its size
	if (fzn_next_constr_posit == fzn_n_constrs) {

		if (FZN_VERBOSE)
			printf("Extending fzn constraints array.\n");

		fzn_constrs_aux = malloc(fzn_n_constrs * 2 * (sizeof(fzn_constr)));

		fzn_constrs_copy(fzn_constrs_aux, fzn_constrs, fzn_n_constrs);

		free(fzn_constrs);
		fzn_constrs = fzn_constrs_aux;

		fzn_n_constrs *= 2;
	}

	fzn_constrs[fzn_next_constr_posit].name = NULL;
	fzn_constrs[fzn_next_constr_posit].defines_var_idx = -1;
	fzn_constrs[fzn_next_constr_posit].consts = NULL;
	fzn_constrs[fzn_next_constr_posit].consts_aux = NULL;
	fzn_constrs[fzn_next_constr_posit].vars_id = NULL;
	fzn_constrs[fzn_next_constr_posit].vars_id_aux = NULL;
	fzn_constrs[fzn_next_constr_posit].ignore = false;
	fzn_constrs[fzn_next_constr_posit].max_consts = 0;
	fzn_constrs[fzn_next_constr_posit].max_vars = 0;
	fzn_constrs[fzn_next_constr_posit].next_const_to_add = 0;
	fzn_constrs[fzn_next_constr_posit].next_var_to_add = 0;
	fzn_constrs[fzn_next_constr_posit].boundsR = false;
	fzn_constrs[fzn_next_constr_posit].boundsD = false;
	fzn_constrs[fzn_next_constr_posit].boundsZ = false;
	fzn_constrs[fzn_next_constr_posit].domain = false;
	fzn_constrs[fzn_next_constr_posit].priority = false;
	fzn_constrs[fzn_next_constr_posit].id = -1;
	fzn_constrs[fzn_next_constr_posit].pos_init_2_array = fzn_obj.pos_init_2_array;

	for (i = 0; i < fzn_obj.next_annot; i++) {

		if (FZN_VERBOSE)
			printf("Adding annotation %s to constraint.\n", fzn_obj.annots[i]);

		if (strcmp(fzn_obj.annots[i], "defines_var") == 0) {

			for (j = 0; j < fzn_next_var_posit; j++) {
				if (fzn_vars[j].name != NULL && strcmp(fzn_vars[j].name, fzn_constrs[fzn_next_constr_posit].name) == 0) {

					if (FZN_VERBOSE)
						printf("Setting this constraint as defining variable %s.\n", fzn_vars[j].name);

					fzn_constrs[fzn_next_constr_posit].defines_var_idx = j;
					fzn_vars[j].defined_by_constr_idx = fzn_next_constr_posit;
					fzn_vars[j].is_defined_var = true; // some FlatZinc models do not mark the variable

					if (FZN_VERBOSE)
						printf("Setting variable %s as defined by current constraint.\n", fzn_vars[j].name);

					free(fzn_constrs[fzn_next_constr_posit].name);
					fzn_constrs[fzn_next_constr_posit].name = NULL;

					break;
				}
			}

		} else if (strcmp(fzn_obj.annots[i], "boundsZ") == 0) {
			fzn_constrs[fzn_next_constr_posit].boundsZ = true;

		} else if (strcmp(fzn_obj.annots[i], "boundsR") == 0) {
			fzn_constrs[fzn_next_constr_posit].boundsR = true;

		} else if (strcmp(fzn_obj.annots[i], "boundsD") == 0) {
			fzn_constrs[fzn_next_constr_posit].boundsD = true;

		} else if (strcmp(fzn_obj.annots[i], "domain") == 0) {
			fzn_constrs[fzn_next_constr_posit].domain = true;

		} else if (strcmp(fzn_obj.annots[i], "priority") == 0) {
			fzn_constrs[fzn_next_constr_posit].priority = true;

		} else {

			if (fzn_constrs[fzn_next_constr_posit].name == NULL) {

				if (FZN_VERBOSE)
					printf("Adding name %s to constraint.\n", fzn_obj.annots[i]);

				fzn_constrs[fzn_next_constr_posit].name = malloc((strlen(fzn_obj.annots[i]) + 1) * sizeof(char));
				strcpy(fzn_constrs[fzn_next_constr_posit].name, fzn_obj.annots[i]);

			} else {
				fprintf(stderr, "Trying to name constraint with %s when its name is already %s.\n", fzn_constrs[fzn_next_constr_posit].name, fzn_obj.annots[i]);
				exit(-1);
			}
		}
	}

	if (strcmp(fzn_constrs[fzn_next_constr_posit].name, "int_lt") == 0
			|| strcmp(fzn_constrs[fzn_next_constr_posit].name, "int_le") == 0) {

		fzn_constrs[fzn_next_constr_posit].vars_id = malloc(2 * sizeof(unsigned int));
		fzn_constrs[fzn_next_constr_posit].max_vars = 2;

		fzn_add_fzn_obj_elem_var_to_constr(0);
		fzn_add_fzn_obj_elem_var_to_constr(1);

	} else if (strcmp(fzn_constrs[fzn_next_constr_posit].name, "bool2int") == 0
			|| strcmp(fzn_constrs[fzn_next_constr_posit].name, "bool_eq") == 0) {

		if (fzn_obj.element_is_var[0] && fzn_obj.element_is_var[1]) {

			fzn_constrs[fzn_next_constr_posit].vars_id = malloc(2 * sizeof(unsigned int));

#if FZN_REPLACE_BOOL2INT
			fzn_vars[fzn_obj.elements[1]].replace_by_v_id = fzn_obj.elements[0];
			fzn_vars[fzn_obj.elements[1]].ignore = true;

			if (FZN_VERBOSE)
				printf("Replacing variable %s by variable %s due to FZN constraint %s.\n", fzn_vars[fzn_obj.elements[1]].name,
						fzn_vars[fzn_obj.elements[0]].name, fzn_constrs[fzn_next_constr_posit].name);

			fzn_constrs[fzn_next_constr_posit].ignore = true;
#endif

			fzn_constrs[fzn_next_constr_posit].max_vars = 2;

			fzn_add_fzn_obj_elem_var_to_constr(0);
			fzn_add_fzn_obj_elem_var_to_constr(1);

		} else {
			fprintf(stderr, "fzn_obj has values instead of variables when ignoring constraint %s (%d).\n", fzn_obj.annots[0], fzn_next_constr_posit);
			exit(-1);
		}

	} else if (strcmp(fzn_constrs[fzn_next_constr_posit].name, "bool_clause") == 0) {

		fzn_constrs[fzn_next_constr_posit].vars_id = malloc(fzn_obj.next_element * sizeof(unsigned int));
		fzn_constrs[fzn_next_constr_posit].max_vars = fzn_obj.next_element;

		for (i = 0; i < fzn_obj.next_element; i++) {
			fzn_add_fzn_obj_elem_var_to_constr(i);
		}

	} else if (strcmp(fzn_constrs[fzn_next_constr_posit].name, "int_ne") == 0 && !fzn_obj.element_is_var[1]) {

		fzn_constrs[fzn_next_constr_posit].consts = malloc(sizeof(int));
		fzn_constrs[fzn_next_constr_posit].vars_id = malloc(sizeof(unsigned int));
		fzn_constrs[fzn_next_constr_posit].max_consts = 1;
		fzn_constrs[fzn_next_constr_posit].max_vars = 1;

		fzn_add_fzn_obj_elem_var_to_constr(0);
		fzn_add_fzn_obj_elem_val_to_constr(1);

	} else if ((strcmp(fzn_constrs[fzn_next_constr_posit].name, "int_eq_reif") == 0 && !fzn_obj.element_is_var[1])
			|| (strcmp(fzn_constrs[fzn_next_constr_posit].name, "bool_eq_reif") == 0 && !fzn_obj.element_is_var[1])) {

		fzn_constrs[fzn_next_constr_posit].consts = malloc(1 * sizeof(int));
		fzn_constrs[fzn_next_constr_posit].vars_id = malloc(2 * sizeof(unsigned int));
		fzn_constrs[fzn_next_constr_posit].max_consts = 1;
		fzn_constrs[fzn_next_constr_posit].max_vars = 2;

		fzn_add_fzn_obj_elem_var_to_constr(0);
		fzn_add_fzn_obj_elem_val_to_constr(1);
		fzn_add_fzn_obj_elem_var_to_constr(2);

	} else if (strcmp(fzn_constrs[fzn_next_constr_posit].name, "int_times") == 0
			|| strcmp(fzn_constrs[fzn_next_constr_posit].name, "int_eq_reif") == 0
			|| strcmp(fzn_constrs[fzn_next_constr_posit].name, "int_lt_reif") == 0
			|| strcmp(fzn_constrs[fzn_next_constr_posit].name, "int_le_reif") == 0
			|| strcmp(fzn_constrs[fzn_next_constr_posit].name, "int_ne_reif") == 0
			|| strcmp(fzn_constrs[fzn_next_constr_posit].name, "bool_eq_reif") == 0
			|| strcmp(fzn_constrs[fzn_next_constr_posit].name, "int_max") == 0) {

		fzn_constrs[fzn_next_constr_posit].vars_id = malloc(3 * sizeof(unsigned int));
		fzn_constrs[fzn_next_constr_posit].max_vars = 3;

		fzn_add_fzn_obj_elem_var_to_constr(0);
		fzn_add_fzn_obj_elem_var_to_constr(1);
		fzn_add_fzn_obj_elem_var_to_constr(2);

	} else if (strcmp(fzn_constrs[fzn_next_constr_posit].name, "int_lin_ne") == 0
			|| strcmp(fzn_constrs[fzn_next_constr_posit].name, "int_lin_le") == 0
			|| strcmp(fzn_constrs[fzn_next_constr_posit].name, "int_lin_eq") == 0) {

		int n_consts = (fzn_obj.next_element - 1) / 2 + 1;
		int n_vars = fzn_obj.next_element - n_consts;

		fzn_constrs[fzn_next_constr_posit].consts = malloc(n_consts * sizeof(int));
		fzn_constrs[fzn_next_constr_posit].vars_id = malloc(n_vars * sizeof(unsigned int));
		fzn_constrs[fzn_next_constr_posit].max_consts = n_consts;
		fzn_constrs[fzn_next_constr_posit].max_vars = n_vars;

		for (i = 0; i < n_consts - 1; i++) {
			fzn_add_fzn_obj_elem_val_to_constr(i);
		}
		for (; i < n_vars + n_consts - 1; i++) {
			fzn_add_fzn_obj_elem_var_to_constr(i);
		}
		fzn_add_fzn_obj_elem_val_to_constr(i);

	} else if (strcmp(fzn_constrs[fzn_next_constr_posit].name, "int_lin_ne_reif") == 0
			|| strcmp(fzn_constrs[fzn_next_constr_posit].name, "int_lin_le_reif") == 0
			|| strcmp(fzn_constrs[fzn_next_constr_posit].name, "int_lin_eq_reif") == 0) {

		int n_consts = (fzn_obj.next_element - 2) / 2 + 1;
		int n_vars = fzn_obj.next_element - n_consts;

		fzn_constrs[fzn_next_constr_posit].consts = malloc(n_consts * sizeof(int));
		fzn_constrs[fzn_next_constr_posit].vars_id = malloc(n_vars * sizeof(unsigned int));
		fzn_constrs[fzn_next_constr_posit].max_consts = n_consts;
		fzn_constrs[fzn_next_constr_posit].max_vars = n_vars;

		for (i = 0; i < (fzn_obj.next_element - 2) / 2; i++) {
			fzn_add_fzn_obj_elem_val_to_constr(i);
		}
		for (; i < fzn_obj.next_element - 2; i++) {
			fzn_add_fzn_obj_elem_var_to_constr(i);
		}
		fzn_add_fzn_obj_elem_val_to_constr(i);
		fzn_add_fzn_obj_elem_var_to_constr(i + 1);

	} else if (strcmp(fzn_constrs[fzn_next_constr_posit].name, "array_bool_or") == 0
			|| strcmp(fzn_constrs[fzn_next_constr_posit].name, "array_bool_and") == 0) {

		fzn_constrs[fzn_next_constr_posit].vars_id = malloc(fzn_obj.next_element * sizeof(unsigned int));
		fzn_constrs[fzn_next_constr_posit].max_vars = fzn_obj.next_element;

		for (i = 0; i < fzn_obj.next_element; i++) {
			fzn_add_fzn_obj_elem_var_to_constr(i);
		}

	} else if (strcmp(fzn_constrs[fzn_next_constr_posit].name, "array_var_int_element") == 0) {

		if (fzn_obj.element_is_var[fzn_obj.next_element - 1]) {

			fzn_constrs[fzn_next_constr_posit].vars_id = malloc(fzn_obj.next_element * sizeof(unsigned int));
			fzn_constrs[fzn_next_constr_posit].max_vars = fzn_obj.next_element;

		} else {
			fzn_constrs[fzn_next_constr_posit].consts = malloc(1 * sizeof(int));
			fzn_constrs[fzn_next_constr_posit].vars_id = malloc((fzn_obj.next_element - 1) * sizeof(unsigned int));
			fzn_constrs[fzn_next_constr_posit].max_consts = 1;
			fzn_constrs[fzn_next_constr_posit].max_vars = fzn_obj.next_element - 1;
		}

		for (i = 0; i < fzn_obj.next_element - 1; i++) {
			fzn_add_fzn_obj_elem_var_to_constr(i);
		}
		if (fzn_obj.element_is_var[fzn_obj.next_element - 1]) {
			fzn_add_fzn_obj_elem_var_to_constr(i);
		} else {
			fzn_add_fzn_obj_elem_val_to_constr(i);
		}

	} else if (strcmp(fzn_constrs[fzn_next_constr_posit].name, "array_int_element") == 0) {

		fzn_constrs[fzn_next_constr_posit].consts = malloc((fzn_obj.next_element - 2) * sizeof(int));
		fzn_constrs[fzn_next_constr_posit].vars_id = malloc(2 * sizeof(unsigned int));
		fzn_constrs[fzn_next_constr_posit].max_consts = fzn_obj.next_element - 2;
		fzn_constrs[fzn_next_constr_posit].max_vars = 2;

		fzn_add_fzn_obj_elem_var_to_constr(0);
		for (i = 1; i < fzn_obj.next_element - 1; i++) {
			fzn_add_fzn_obj_elem_val_to_constr(i);
		}
		fzn_add_fzn_obj_elem_var_to_constr(i);

	} else if (strcmp(fzn_constrs[fzn_next_constr_posit].name, "all_different") == 0) {
		// already done

	} else {
		fprintf(stderr, "Constraint \"%s\" (%d) not recognized when creating FZN constraint.\n", fzn_constrs[fzn_next_constr_posit].name, fzn_next_constr_posit);
		exit(-1);
	}

    fzn_reset_object_elements();

	fzn_next_constr_posit++;
}

/*
 * Add an element IDX to the last created constraint
 * e_idx - element idx in fzn_obj
 */
void fzn_add_fzn_obj_elem_var_to_constr(int e_idx) {
	int v_idx;
	int i;

	if (fzn_constrs[fzn_next_constr_posit].max_vars == 0) {
		fprintf(stderr, "\n Error: max_vars = 0 when constructing fzn constraint %s.\n", fzn_constrs[fzn_next_constr_posit].name);
		exit(-1);
	}

	// if the array of variables that are constrained by this constraint is already full, doubles it
	if (fzn_constrs[fzn_next_constr_posit].next_var_to_add == fzn_constrs[fzn_next_constr_posit].max_vars) {

		if (FZN_VERBOSE)
				printf("Extending variables array for constraint %s.\n", fzn_constrs[fzn_next_constr_posit].name);

		fzn_constrs[fzn_next_constr_posit].vars_id_aux = malloc(fzn_constrs[fzn_next_constr_posit].max_vars * 2 * (sizeof(unsigned int)));

		for (i = 0; i < fzn_constrs[fzn_next_constr_posit].max_vars; i++) {
			fzn_constrs[fzn_next_constr_posit].vars_id_aux[i] = fzn_constrs[fzn_next_constr_posit].vars_id[i];
		}

		free(fzn_constrs[fzn_next_constr_posit].vars_id);
		fzn_constrs[fzn_next_constr_posit].vars_id = fzn_constrs[fzn_next_constr_posit].vars_id_aux;

		fzn_constrs[fzn_next_constr_posit].max_vars *= 2;
	}

	if (fzn_obj.element_is_var[e_idx]) {
		v_idx = fzn_obj.elements[e_idx];
	} else {
		v_idx = fzn_new_fzn_obj_var_value(fzn_obj.elements[e_idx]);
	}

	if (FZN_VERBOSE)
			printf("Adding variable %d to constraint %s.\n", v_idx, fzn_constrs[fzn_next_constr_posit].name);

	fzn_constrs[fzn_next_constr_posit].vars_id[fzn_constrs[fzn_next_constr_posit].next_var_to_add] = v_idx;
	fzn_constrs[fzn_next_constr_posit].next_var_to_add++;
}

/*
 * Adds a value to the array of constants of the flatzinc constraint
 * e_idx - element idx in fzn_obj
 */
void fzn_add_fzn_obj_elem_val_to_constr(int e_idx) {
	int i;

	if (FZN_VERBOSE)
			printf("Adding value %d to constraint %s.\n", fzn_obj.elements[e_idx], fzn_constrs[fzn_next_constr_posit].name);

	if (fzn_constrs[fzn_next_constr_posit].max_consts == 0) {
		fprintf(stderr, "\n Error: max_consts = 0 when constructing fzn constraint %s.\n", fzn_constrs[fzn_next_constr_posit].name);
		exit(-1);
	}

	// If the array of constants is already full, doubles its size
	if (fzn_constrs[fzn_next_constr_posit].next_const_to_add == fzn_constrs[fzn_next_constr_posit].max_consts) {

		if (FZN_VERBOSE)
				printf("Extending values array for constraint %s.\n", fzn_constrs[fzn_next_constr_posit].name);

		fzn_constrs[fzn_next_constr_posit].consts_aux = malloc(fzn_constrs[fzn_next_constr_posit].max_consts * 2 * (sizeof(int)));

		for (i = 0; i < fzn_constrs[fzn_next_constr_posit].max_consts; i++) {
			fzn_constrs[fzn_next_constr_posit].consts_aux[i] = fzn_constrs[fzn_next_constr_posit].consts[i];
		}

		free(fzn_constrs[fzn_next_constr_posit].consts);
		fzn_constrs[fzn_next_constr_posit].consts = fzn_constrs[fzn_next_constr_posit].consts_aux;

		fzn_constrs[fzn_next_constr_posit].max_consts *= 2;
	}

	if (fzn_obj.element_is_var[e_idx]) {
		fprintf(stderr, "\n Error: value marked as variable when constructing fzn constraint %s.\n", fzn_constrs[fzn_next_constr_posit].name);
		exit(-1);
	}

	// Adds the value
	fzn_constrs[fzn_next_constr_posit].consts[fzn_constrs[fzn_next_constr_posit].next_const_to_add] = fzn_obj.elements[e_idx];
	fzn_constrs[fzn_next_constr_posit].next_const_to_add++;
}

/*
 * Copy a Flatzinc constraint
 * dest - the array from where to copy the constraint to
 * src - the array from where to copy the constraint from
 * n_constrs - number of constraints to copy
 */
void fzn_constrs_copy(fzn_constr* dest, fzn_constr* src, int n_constrs) {
	int i;

	if (FZN_VERBOSE)
			printf("Copying FZN constraint.\n");

	for (i = 0; i < n_constrs; i++) {
		dest[i].consts = src[i].consts;
		dest[i].consts_aux = src[i].consts_aux;
		dest[i].defines_var_idx = src[i].defines_var_idx;
		dest[i].ignore = src[i].ignore;
		dest[i].boundsZ = src[i].boundsZ;
		dest[i].boundsR = src[i].boundsR;
		dest[i].boundsD = src[i].boundsD;
		dest[i].domain = src[i].domain;
		dest[i].priority = src[i].priority;
		dest[i].priority_v_id = src[i].priority_v_id;
		dest[i].max_consts = src[i].max_consts;
		dest[i].max_vars = src[i].max_vars;
		dest[i].name = src[i].name;
		dest[i].next_const_to_add = src[i].next_const_to_add;
		dest[i].next_var_to_add = src[i].next_var_to_add;
		dest[i].vars_id = src[i].vars_id;
		dest[i].vars_id_aux = src[i].vars_id_aux;
		dest[i].pos_init_2_array = src[i].pos_init_2_array;
	}
}

/*
 * Create a new search annotation with the last fzn_obj data
 */
void fzn_add_fzn_obj_search_annot() {
	int i;

	// if the array of search annotations is already full, doubles its size
	if (fzn_next_search_annot_posit == fzn_n_search_annot) {
		fzn_search_annot_aux = malloc(fzn_n_search_annot * 2 * (sizeof(fzn_search_annotat)));

		fzn_search_annots_copy(fzn_search_annot_aux, fzn_search_annot, fzn_n_search_annot);

		free(fzn_search_annot);
		fzn_search_annot = fzn_search_annot_aux;

		fzn_n_search_annot *= 2;
	}

	fzn_search_annot[fzn_next_search_annot_posit].label_array_name = NULL;

	if (fzn_obj.next_annot > 5) {
		i = 0;

		if (FZN_VERBOSE)
			printf("Adding new array with name array_to_label (number %d).\n", fzn_next_array_posit);

		// if the array of arrays is full, doubles its size
		if (fzn_next_array_posit == fzn_n_arrays) {
			fzn_arrays_aux = malloc(fzn_n_arrays * 2 * (sizeof(fzn_array)));

			fzn_array_copy(fzn_arrays_aux, fzn_arrays, fzn_n_arrays);

			free(fzn_arrays);
			fzn_arrays = fzn_arrays_aux;

			fzn_n_arrays *= 2;
		}

		fzn_arrays[fzn_next_array_posit].name = malloc((strlen("array_to_label") + 1) * sizeof(char));
		strcpy(fzn_arrays[fzn_next_array_posit].name, "array_to_label");

		fzn_arrays[fzn_next_array_posit].output_var = false;
		fzn_arrays[fzn_next_array_posit].is_defined_var = false;
		fzn_arrays[fzn_next_array_posit].var_is_introduced = false;
		fzn_arrays[fzn_next_array_posit].output_array = false;
		fzn_arrays[fzn_next_array_posit].to_label = true;
		fzn_arrays[fzn_next_array_posit].next_position = 0;
		fzn_arrays[fzn_next_array_posit].values = malloc(FZN_MAX_ELEMENTS * sizeof(int));
		fzn_arrays[fzn_next_array_posit].max_values = FZN_MAX_ELEMENTS;
		fzn_arrays[fzn_next_array_posit].values_aux = NULL;
		fzn_arrays[fzn_next_array_posit].var_array = true;

		fzn_search_annot[fzn_next_search_annot_posit].label_array_name = malloc((strlen("array_to_label") + 1) * sizeof(char));
		strcpy(fzn_search_annot[fzn_next_search_annot_posit].label_array_name, "array_to_label");

		fzn_next_array_posit++;

		for (i = 0; i < fzn_obj.next_annot - 4; i++) {
			fzn_add_var_to_array(fzn_obj.annots[i]);
		}

	} else {
		fzn_search_annot[fzn_next_search_annot_posit].label_array_name = malloc((strlen(fzn_obj.annots[0]) + 1) * sizeof(char));
		strcpy(fzn_search_annot[fzn_next_search_annot_posit].label_array_name, fzn_obj.annots[0]);
		i = 1;
	}

	if (FZN_VERBOSE)
			printf("Creating new search annotation %s, %s, %s, %s, %s.\n", fzn_obj.annots[i + 3]
					, fzn_search_annot[fzn_next_search_annot_posit].label_array_name
					, fzn_obj.annots[i], fzn_obj.annots[i + 1], fzn_obj.annots[i + 2]);

	fzn_search_annot[fzn_next_search_annot_posit].label_heur = malloc((strlen(fzn_obj.annots[i]) + 1) * sizeof(char));
	strcpy(fzn_search_annot[fzn_next_search_annot_posit].label_heur, fzn_obj.annots[i]);

	fzn_search_annot[fzn_next_search_annot_posit].assign_heur = malloc((strlen(fzn_obj.annots[i + 1]) + 1) * sizeof(char));
	strcpy(fzn_search_annot[fzn_next_search_annot_posit].assign_heur, fzn_obj.annots[i + 1]);

	fzn_search_annot[fzn_next_search_annot_posit].search_strategy = malloc((strlen(fzn_obj.annots[i + 2]) + 1) * sizeof(char));
	strcpy(fzn_search_annot[fzn_next_search_annot_posit].search_strategy, fzn_obj.annots[i + 2]);

	fzn_search_annot[fzn_next_search_annot_posit].search_type = malloc((strlen(fzn_obj.annots[i + 3]) + 1) * sizeof(char));
	strcpy(fzn_search_annot[fzn_next_search_annot_posit].search_type, fzn_obj.annots[i + 3]);

	fzn_next_search_annot_posit++;

	// int_search or bool_search
	fzn_reset_object_elements();
}

/*
 * Copy a Flatzinc search annotation
 * dest - the array from where to copy the search annotation to
 * src - the array from where to copy the search annotation from
 * n_search_annots - number of search annotation to copy
 */
void fzn_search_annots_copy(fzn_search_annotat* dest, fzn_search_annotat* src, int n_search_annots) {
	int i;

	if (FZN_VERBOSE)
			printf("Copying FZN constraint.\n");

	for (i = 0; i < n_search_annots; i++) {
		dest[i].assign_heur = src[i].assign_heur;
		dest[i].label_array_name = src[i].label_array_name;
		dest[i].label_heur = src[i].label_heur;
		dest[i].search_strategy = src[i].search_strategy;
		dest[i].search_type = src[i].search_type;
	}
}

/*
 * Set an array of variables or a variable to label
 */
void fzn_set_var_or_array_to_label(char* name) {
	int i, j;

	for (i = 0; i < fzn_next_array_posit; i++) {

		if (fzn_arrays[i].name != NULL && strcmp(fzn_arrays[i].name, name) == 0) {

			if (FZN_VERBOSE)
				printf("Setting array %s to label.\n", name);

			fzn_arrays[i].to_label = true;

			for (j = 0; j < fzn_arrays[i].next_position; j++) {

				if (fzn_vars[fzn_arrays[i].values[j]].ignore) {

					if (FZN_VERBOSE)
						printf("Setting variable %s to label because variable %s is ignored.\n",
								fzn_vars[fzn_vars[fzn_arrays[i].values[j]].replace_by_v_id].name, fzn_vars[fzn_arrays[i].values[j]].name);

					fzn_vars[fzn_vars[fzn_arrays[i].values[j]].replace_by_v_id].to_label = true;

				} else {
					if (FZN_VERBOSE)
						printf("Setting variable %s to label.\n", fzn_vars[fzn_arrays[i].values[j]].name);

					fzn_vars[fzn_arrays[i].values[j]].to_label = true;
				}
			}
			return;
		}
	}

	for (i = 0; i < fzn_next_var_posit; i++) {
		if (fzn_vars[i].name != NULL && strcmp(fzn_vars[i].name, name) == 0) {

			if (fzn_vars[i].ignore) {

				if (FZN_VERBOSE)
					printf("Setting variable %s to label because variable %s is ignored.\n", fzn_vars[fzn_vars[i].replace_by_v_id].name, name);

				fzn_vars[fzn_vars[i].replace_by_v_id].to_label = true;

			} else {
				if (FZN_VERBOSE)
					printf("Setting variable %s to label.\n", name);

				fzn_vars[i].to_label = true;
			}

			return;
		}
	}

	fprintf(stderr, "\n Error: variable or array name (\"%s\") not found when setting it to label.\n", name);
	exit(-1);
}

/*
 * Sort the variables of some constraints for input order for possible detection and removal of duplicated constraints
 */
void fzn_sort_constr_vars() {
	unsigned int* vars;
	int* consts;
	int temp_int;
	unsigned int temp_uint;
	int i, j, k, n_vars;

	if (FZN_VERBOSE)
		printf("Sorting the variables of some constraints in input order.\n");

	for (i = 0; i < fzn_next_constr_posit; i++) {

		if (strcmp(fzn_constrs[i].name, "int_lin_le") == 0) {
			n_vars = fzn_constrs[i].next_var_to_add;

			vars = fzn_constrs[i].vars_id;
			consts = fzn_constrs[i].consts;

			for (j = 0; j < n_vars - 1; j++) {
				for (k = 0; k < n_vars - j - 1; k++) {
					if (vars[k] > vars[k + 1]) {

						// swap variables
						temp_uint = vars[k];
						vars[k] = vars[k + 1];
						vars[k + 1] = temp_uint;

						// swap constants
						temp_int = consts[k];
						consts[k] = consts[k + 1];
						consts[k + 1] = temp_int;
					}
				}
			}
		}
	}
}

/*
 * Create a new CSP variable correspondent to the Flatzinc variable in index var_idx of fzn_vars array
 * var_idx - index of fzn_vars array where the variable is
 */
void fzn_new_csp_var(int var_idx) {
	unsigned int v_id;
	int i;

	if (FZN_VERBOSE) {
		if (!fzn_vars[var_idx].ignore && !fzn_vars[var_idx].created) {
			printf("Creating new CSP variable");

			if (fzn_vars[var_idx].name != NULL) {
				printf(" from %s", fzn_vars[var_idx].name);
			}

			if (fzn_vars[var_idx].range == true) {
				printf(" with range %d,%d", fzn_vars[var_idx].min, fzn_vars[var_idx].max);

			} else {
				printf(" with values {");
				for (i = 0; i < fzn_vars[var_idx].next_position - 1; i++) {
					printf("%d,", fzn_vars[var_idx].values[i]);
				}
				printf("%d}", fzn_vars[var_idx].values[i]);
			}

		} else {
			printf("Variable");

			if (fzn_vars[var_idx].name != NULL) {
				printf(" from %s", fzn_vars[var_idx].name);
			}

			if (fzn_vars[var_idx].range == true) {
				printf(" with range %d,%d ", fzn_vars[var_idx].min, fzn_vars[var_idx].max);

			} else {
				printf(" with values {");
				for (i = 0; i < fzn_vars[var_idx].next_position - 1; i++) {
					printf("%d,", fzn_vars[var_idx].values[i]);
				}
				printf("%d} ", fzn_vars[var_idx].values[i]);
			}

			printf("is ignored (or already created), so it won't be created.\n");
		}
	}

  	if (!fzn_vars[var_idx].ignore && !fzn_vars[var_idx].created) {

  		// ranged values
  		if (fzn_vars[var_idx].range == true) {

  			if (fzn_vars[var_idx].min < 0 || fzn_vars[var_idx].max < 0) {
  				fprintf(stderr, "\n PHACT can only work with variables whose domains contain only values equal or greater than zero.\n"
  						" Please apply an offset for the variables domains on your CSP model.\n");
  				exit(-1);
  			}

			v_id = v_new_range(fzn_vars[var_idx].min, fzn_vars[var_idx].max, fzn_vars[var_idx].to_label);

		// alternated values
  		} else {

  			for (i = 0; i < fzn_vars[var_idx].next_position; i++) {
  				if (fzn_vars[var_idx].values[i] < 0) {
  	  				fprintf(stderr, "\n PHACT can only work with variables whose domains contain only values equal or greater than zero.\n"
  	  						" Please apply an offset to the domains of the variables of your CSP model.\n");
  	  				exit(-1);
  				}
  			}

			v_id = v_new_vals((unsigned int*)fzn_vars[var_idx].values, fzn_vars[var_idx].next_position, fzn_vars[var_idx].to_label);
  		}
  		fzn_vars[var_idx].id = v_id;

  		if (FZN_VERBOSE) {
  			printf(" with ID %d and label %d\n", v_id, fzn_vars[var_idx].to_label);
  		}

  		fzn_vars[var_idx].created = true;
  	}
}

/*
 * Creates a new CSP constraint correspondent to the Flatzinc constraint on index constr_idx from fzn_constrs array
 * constr_idx - index in the fzn_constrs array of the Flatzinc constraint to create
 */
void fzn_new_csp_constr(int constr_idx) {
	int i;

	if (!fzn_constrs[constr_idx].ignore) {

#if FZN_REMOVE_ACHIEVED_CONSTRS
		int k;

		if (strcmp(fzn_constrs[constr_idx].name, "int_lin_le") == 0
				&& fzn_constrs[constr_idx].consts[fzn_constrs[constr_idx].next_const_to_add - 1] >= 0) {

			for (k = 0; k < fzn_constrs[constr_idx].next_const_to_add - 1; k++) {
				if (fzn_constrs[constr_idx].consts[k] > 0) {
					break;
				}
			}
			if (k == fzn_constrs[constr_idx].next_const_to_add - 1) {
				fzn_constrs[constr_idx].ignore = true;
				return;
			}
		}
#endif

		// update the variables id from Flatzinc to PHACT
		for (i = 0; i < fzn_constrs[constr_idx].next_var_to_add; i++) {

			if (fzn_vars[fzn_constrs[constr_idx].vars_id[i]].replace_by_v_id == -1) {
				fzn_constrs[constr_idx].vars_id[i] = fzn_vars[fzn_constrs[constr_idx].vars_id[i]].id;

			} else {

				if (fzn_vars[fzn_vars[fzn_constrs[constr_idx].vars_id[i]].replace_by_v_id].ignore) {
					fprintf(stderr, "The %d variable of the constraint \"%s\" (%d) is a replacement variable marked as ignored.\n", i,
							fzn_constrs[constr_idx].name, constr_idx);
					exit(-1);
				}

				fzn_constrs[constr_idx].vars_id[i] = fzn_vars[fzn_vars[fzn_constrs[constr_idx].vars_id[i]].replace_by_v_id].id;
			}

			if (fzn_vars[fzn_constrs[constr_idx].vars_id[i]].ignore && fzn_vars[fzn_constrs[constr_idx].vars_id[i]].replace_by_v_id == -1) {
				fprintf(stderr, "The %d variable of the constraint \"%s\" (%d) is marked as ignored and has no replacement.\n", i,
						fzn_constrs[constr_idx].name, constr_idx);
				exit(-1);
			}

		}

#if FZN_REMOVE_DUPLICATE_CONSTRS
		int j;

		if (FZN_VERBOSE)
			printf("Checking and removing possible duplicated constraints\n");

		for (i = constr_idx + 1; i < fzn_next_constr_posit; i++) {

			if (fzn_constrs[constr_idx].next_const_to_add == fzn_constrs[i].next_const_to_add
					&& fzn_constrs[constr_idx].next_var_to_add == fzn_constrs[i].next_var_to_add
					&& fzn_constrs[i].ignore == false
					&& strcmp(fzn_constrs[constr_idx].name, fzn_constrs[i].name) == 0) {

				fzn_constrs[i].ignore = true;

				for (j = 0; j < fzn_constrs[constr_idx].next_var_to_add; j++) {
					if (fzn_constrs[constr_idx].vars_id[j] != fzn_constrs[i].vars_id[j]) {
						fzn_constrs[i].ignore = false;
						break;
					}
				}

				if (fzn_constrs[i].ignore == true) {
					fzn_constrs[i].ignore = false;
					if (strcmp(fzn_constrs[constr_idx].name, "int_lin_le") == 0) {
						for (j = 0; j < fzn_constrs[constr_idx].next_const_to_add - 1; j++) {
							if (fzn_constrs[constr_idx].consts[j] != fzn_constrs[i].consts[j]) {
								fzn_constrs[i].ignore = false;
								break;
							}
						}

						if (fzn_constrs[i].ignore) {
							if (fzn_constrs[constr_idx].consts[j] < fzn_constrs[i].consts[j]) {
								fzn_constrs[constr_idx].ignore = false;
								fzn_constrs[i].ignore = true;
							} else {
								fzn_constrs[constr_idx].ignore = true;
								fzn_constrs[i].ignore = false;
							}
						}

					} else {
						for (j = 0; j < fzn_constrs[constr_idx].next_const_to_add; j++) {
							if (fzn_constrs[constr_idx].consts[j] != fzn_constrs[i].consts[j]) {
								fzn_constrs[i].ignore = false;
								break;
							}
						}
					}
				}
			}
		}
#endif

		if (!fzn_constrs[constr_idx].ignore) {

			if (strcmp(fzn_constrs[constr_idx].name, "int_lt") == 0) {

				if (FZN_VERBOSE)
					printf("Adding new CSP (%d) int_lt (c_lt) with variables %d and %d", constr_idx, fzn_constrs[constr_idx].vars_id[0],
							fzn_constrs[constr_idx].vars_id[1]);

				fzn_constrs[constr_idx].id = c_lt(fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].vars_id[1]);

				if (FZN_VERBOSE)
					printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);

			} else if (strcmp(fzn_constrs[constr_idx].name, "int_ne") == 0 && fzn_constrs[constr_idx].next_const_to_add == 1) {

				if (FZN_VERBOSE)
					printf("Deleting value %d from variable %d from int_ne\n", fzn_constrs[constr_idx].consts[0], fzn_constrs[constr_idx].vars_id[0]);

				fzn_constrs[constr_idx].ignore = true;
				v_del_val(&VS[fzn_constrs[constr_idx].vars_id[0]], fzn_constrs[constr_idx].consts[0]);

				if (FZN_VERBOSE)
					printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);

			} else if (strcmp(fzn_constrs[constr_idx].name, "int_le") == 0) {

				if (FZN_VERBOSE)
					printf("Adding new CSP (%d) int_le (c_le) with variables %d and %d", constr_idx, fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].vars_id[1]);

				fzn_constrs[constr_idx].id = c_le(fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].vars_id[1]);

				if (FZN_VERBOSE)
					printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);

			} else if (strcmp(fzn_constrs[constr_idx].name, "int_le_reif") == 0) {

				if (FZN_VERBOSE)
					printf("Adding new CSP (%d) int_le_reif (c_le_reif) with variables %d, %d and %d", constr_idx, fzn_constrs[constr_idx].vars_id[0],
							fzn_constrs[constr_idx].vars_id[1], 	fzn_constrs[constr_idx].vars_id[2]);

				fzn_constrs[constr_idx].id = c_le_reif(fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].vars_id[1], fzn_constrs[constr_idx].vars_id[2]);

				if (FZN_VERBOSE)
					printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);

			} else if (strcmp(fzn_constrs[constr_idx].name, "int_lt_reif") == 0) {

				if (FZN_VERBOSE)
					printf("Adding new CSP (%d) int_lt_reif (c_lt_reif) with variables %d, %d and %d", constr_idx, fzn_constrs[constr_idx].vars_id[0],
							fzn_constrs[constr_idx].vars_id[1], fzn_constrs[constr_idx].vars_id[2]);

				fzn_constrs[constr_idx].id = c_lt_reif(fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].vars_id[1], fzn_constrs[constr_idx].vars_id[2]);

				if (FZN_VERBOSE)
					printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);

			} else if (strcmp(fzn_constrs[constr_idx].name, "int_ne_reif") == 0) {

				if (FZN_VERBOSE)
					printf("Adding new CSP (%d) int_ne_reif (c_ne_reif) with variables %d, %d and %d", constr_idx, fzn_constrs[constr_idx].vars_id[0],
							fzn_constrs[constr_idx].vars_id[1], fzn_constrs[constr_idx].vars_id[2]);

				fzn_constrs[constr_idx].id = c_ne_reif(fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].vars_id[1], fzn_constrs[constr_idx].vars_id[2]);

				if (FZN_VERBOSE)
					printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);

			} else if (strcmp(fzn_constrs[constr_idx].name, "int_max") == 0) {

				if (FZN_VERBOSE)
					printf("Adding new CSP (%d) constraint int_max (c_max) with variables %d, %d and %d", constr_idx, fzn_constrs[constr_idx].vars_id[0],
							fzn_constrs[constr_idx].vars_id[1],	fzn_constrs[constr_idx].vars_id[2]);

				fzn_constrs[constr_idx].id = c_max(fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].vars_id[1], fzn_constrs[constr_idx].vars_id[2]);

				if (FZN_VERBOSE)
					printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);

			} else if (strcmp(fzn_constrs[constr_idx].name, "int_lin_ne") == 0) {

				// remove value
				if (fzn_constrs[constr_idx].next_var_to_add == 1) {

					if (fzn_constrs[constr_idx].consts[0] == 1 && fzn_constrs[constr_idx].consts[1] >= 0) {

						if (FZN_VERBOSE)
							printf("Deleting value %d from variable %d from int_lin_ne\n", fzn_constrs[constr_idx].consts[1], fzn_constrs[constr_idx].vars_id[0]);

						fzn_constrs[constr_idx].ignore = true;
						v_del_val(&VS[fzn_constrs[constr_idx].vars_id[0]], fzn_constrs[constr_idx].consts[1]);

					} else if (fzn_constrs[constr_idx].next_var_to_add == 1 && fzn_constrs[constr_idx].consts[0] == -1 && fzn_constrs[constr_idx].consts[1] <= 0) {

						if (FZN_VERBOSE)
							printf("Deleting value %d from variable %d from int_lin_ne\n", abs(fzn_constrs[constr_idx].consts[1]), fzn_constrs[constr_idx].vars_id[0]);

						fzn_constrs[constr_idx].ignore = true;
						v_del_val(&VS[fzn_constrs[constr_idx].vars_id[0]], abs(fzn_constrs[constr_idx].consts[1]));

					} else {

						if (FZN_VERBOSE)
							printf("Adding new CSP (%d) int_lin_ne (c_linear_ne) with constants %d..., variables %d... and result %d", constr_idx,
									fzn_constrs[constr_idx].consts[0], fzn_constrs[constr_idx].vars_id[0],
									fzn_constrs[constr_idx].consts[fzn_constrs[constr_idx].next_var_to_add]);

						fzn_constrs[constr_idx].id = c_linear_ne(fzn_constrs[constr_idx].consts, fzn_constrs[constr_idx].vars_id, fzn_constrs[constr_idx].next_var_to_add,
								fzn_constrs[constr_idx].consts[fzn_constrs[constr_idx].next_var_to_add]);

						if (FZN_VERBOSE)
							printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);
					}

				// ne, minus_ne or linear_ne
				} else if (fzn_constrs[constr_idx].next_var_to_add == 2) {

					if (fzn_constrs[constr_idx].consts[2] == 0 && ((fzn_constrs[constr_idx].consts[0] == 1 && fzn_constrs[constr_idx].consts[1] == -1)
						|| (fzn_constrs[constr_idx].consts[0] == -1 && fzn_constrs[constr_idx].consts[1] == 1))) {

						if (FZN_VERBOSE)
							printf("Adding new CSP (%d) int_lin_ne (c_ne) with variables %d and %d", constr_idx, fzn_constrs[constr_idx].vars_id[0],
									fzn_constrs[constr_idx].vars_id[1]);

						fzn_constrs[constr_idx].id = c_ne(fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].vars_id[1]);

						if (FZN_VERBOSE)
							printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);

					} else if (fzn_constrs[constr_idx].consts[0] == 1) {

						if (fzn_constrs[constr_idx].consts[1] == -1) {

							if (FZN_VERBOSE)
								printf("Adding new CSP (%d) int_lin_ne (c_minus_ne) with variables %d and %d and a constant %d", constr_idx,
										fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].vars_id[1], fzn_constrs[constr_idx].consts[2]);

							fzn_constrs[constr_idx].id = c_minus_ne(fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].vars_id[1], fzn_constrs[constr_idx].consts[2]);

							if (FZN_VERBOSE)
								printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);

						} else if (fzn_constrs[constr_idx].consts[1] == 1) {

							if (FZN_VERBOSE)
								printf("Adding new CSP (%d) int_lin_ne (c_minus_ne) with variables %d and %d and a constant %d ", constr_idx,
										fzn_constrs[constr_idx].vars_id[1], fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].consts[2]);

							fzn_constrs[constr_idx].id = c_minus_ne(fzn_constrs[constr_idx].vars_id[1], fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].consts[2]);

							if (FZN_VERBOSE)
								printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);
						}
					} else {

						if (FZN_VERBOSE)
							printf("Adding new CSP (%d) int_lin_ne (c_linear_ne) with constants %d..., variables %d... and result %d", constr_idx,
									fzn_constrs[constr_idx].consts[0], fzn_constrs[constr_idx].vars_id[0],
									fzn_constrs[constr_idx].consts[fzn_constrs[constr_idx].next_var_to_add]);

						fzn_constrs[constr_idx].id = c_linear_ne(fzn_constrs[constr_idx].consts, fzn_constrs[constr_idx].vars_id, fzn_constrs[constr_idx].next_var_to_add,
								fzn_constrs[constr_idx].consts[fzn_constrs[constr_idx].next_var_to_add]);

						if (FZN_VERBOSE)
							printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);
					}
				// linear_ne
				} else {

					if (FZN_VERBOSE)
						printf("Adding new CSP (%d) int_lin_ne (c_linear_ne) with constants %d..., variables %d... and result %d", constr_idx,
								fzn_constrs[constr_idx].consts[0], fzn_constrs[constr_idx].vars_id[0],
								fzn_constrs[constr_idx].consts[fzn_constrs[constr_idx].next_var_to_add]);

					fzn_constrs[constr_idx].id = c_linear_ne(fzn_constrs[constr_idx].consts, fzn_constrs[constr_idx].vars_id, fzn_constrs[constr_idx].next_var_to_add,
							fzn_constrs[constr_idx].consts[fzn_constrs[constr_idx].next_var_to_add]);

					if (FZN_VERBOSE)
						printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);
				}
			} else if (strcmp(fzn_constrs[constr_idx].name, "int_lin_le") == 0) {

				if (fzn_constrs[constr_idx].next_var_to_add == 2 && fzn_constrs[constr_idx].next_const_to_add == 3
						&& fzn_constrs[constr_idx].consts[0] == 1 && fzn_constrs[constr_idx].consts[1] == -1 && fzn_constrs[constr_idx].consts[2] == -1) {

					if (FZN_VERBOSE)
						printf("Adding new CSP (%d) int_lin_le (c_lt) with variables %d and %d", constr_idx, fzn_constrs[constr_idx].vars_id[0],
								fzn_constrs[constr_idx].vars_id[1]);

					fzn_constrs[constr_idx].id = c_lt(fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].vars_id[1]);

					if (FZN_VERBOSE)
						printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);

				} else if (fzn_constrs[constr_idx].next_var_to_add == 2 && fzn_constrs[constr_idx].next_const_to_add == 3
						&& fzn_constrs[constr_idx].consts[0] == 1 && fzn_constrs[constr_idx].consts[1] == -1 && fzn_constrs[constr_idx].consts[2] == 0) {

					if (FZN_VERBOSE)
						printf("Adding new CSP (%d) int_lin_le (c_le) with variables %d and %d", constr_idx, fzn_constrs[constr_idx].vars_id[0],
								fzn_constrs[constr_idx].vars_id[1]);

					fzn_constrs[constr_idx].id = c_le(fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].vars_id[1]);

					if (FZN_VERBOSE)
						printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);

				} else {

					if (FZN_VERBOSE)
						printf("Adding new CSP (%d) int_lin_le (c_linear_lt) with constants %d..., variables %d... and result %d", constr_idx,
								fzn_constrs[constr_idx].consts[0], fzn_constrs[constr_idx].vars_id[0],
								fzn_constrs[constr_idx].consts[fzn_constrs[constr_idx].next_var_to_add]);

					fzn_constrs[constr_idx].id = c_linear_lt(fzn_constrs[constr_idx].consts, fzn_constrs[constr_idx].vars_id, fzn_constrs[constr_idx].next_var_to_add,
							fzn_constrs[constr_idx].consts[fzn_constrs[constr_idx].next_var_to_add] + 1);

					if (FZN_VERBOSE)
						printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);
				}

			} else if (strcmp(fzn_constrs[constr_idx].name, "int_lin_le_reif") == 0) {
				if (fzn_constrs[constr_idx].next_var_to_add == 3 && fzn_constrs[constr_idx].next_const_to_add == 3
						&& fzn_constrs[constr_idx].consts[0] == 1 && fzn_constrs[constr_idx].consts[1] == -1 && fzn_constrs[constr_idx].consts[2] == -1) {

					if (FZN_VERBOSE)
						printf("Adding new CSP (%d) int_lin_le_reif (c_lt_reif) with variables %d, %d and %d", constr_idx, fzn_constrs[constr_idx].vars_id[0],
								fzn_constrs[constr_idx].vars_id[1], fzn_constrs[constr_idx].vars_id[2]);

					fzn_constrs[constr_idx].id = c_lt_reif(fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].vars_id[1], fzn_constrs[constr_idx].vars_id[2]);

					if (FZN_VERBOSE)
						printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);

				} else {

					if (FZN_VERBOSE)
						printf("Adding new CSP (%d) int_lin_le_reif (c_linear_lt_reif) with constants %d..., variables %d..., result %d and reification variable %d",
								constr_idx, fzn_constrs[constr_idx].consts[0], fzn_constrs[constr_idx].vars_id[0],
								fzn_constrs[constr_idx].consts[fzn_constrs[constr_idx].next_var_to_add],
								fzn_constrs[constr_idx].vars_id[fzn_constrs[constr_idx].next_var_to_add - 1]);

					fzn_constrs[constr_idx].id = c_linear_lt_reif(fzn_constrs[constr_idx].consts, fzn_constrs[constr_idx].vars_id, fzn_constrs[constr_idx].next_var_to_add - 1,
							fzn_constrs[constr_idx].consts[fzn_constrs[constr_idx].next_var_to_add - 1] + 1,
							fzn_constrs[constr_idx].vars_id[fzn_constrs[constr_idx].next_var_to_add - 1]);

					if (FZN_VERBOSE)
						printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);
				}

			} else if (strcmp(fzn_constrs[constr_idx].name, "int_lin_eq") == 0) {

				// check if it is a sum_var constraint
				int j = 0;
				int minus_idx = 0;
				int plus_idx = 0;
				int minus_consts = 0;
				int plus_consts = 0;
				unsigned int* vars_idx = malloc(fzn_constrs[constr_idx].next_const_to_add * sizeof(unsigned int));

				for (i = 0; i < fzn_constrs[constr_idx].next_const_to_add; i++) {
					if (fzn_constrs[constr_idx].consts[i] == -1) {
						minus_idx = i;
						minus_consts++;
					} else if (fzn_constrs[constr_idx].consts[i] == 1) {
						plus_idx = i;
						plus_consts++;
					}
				}

				if ((plus_consts + 1 == fzn_constrs[constr_idx].next_const_to_add && fzn_constrs[constr_idx].consts[fzn_constrs[constr_idx].next_const_to_add - 1] != 1)
						|| (plus_consts == fzn_constrs[constr_idx].next_const_to_add)) {

					j = 0;
					for (i = 0; i < fzn_constrs[constr_idx].next_const_to_add - 1; i++) {
						vars_idx[j++] = fzn_constrs[constr_idx].vars_id[i];
					}

					if (FZN_VERBOSE)
						printf("Adding new CSP (%d) int_lin_eq (c_sum) with variables %d... and result %d", constr_idx, vars_idx[0],
								fzn_constrs[constr_idx].consts[fzn_constrs[constr_idx].next_const_to_add - 1]);

					fzn_constrs[constr_idx].id = c_sum(vars_idx, fzn_constrs[constr_idx].next_var_to_add,
							fzn_constrs[constr_idx].consts[fzn_constrs[constr_idx].next_const_to_add - 1]);

					if (FZN_VERBOSE)
						printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);

				} else if (minus_consts + plus_consts + 1 == fzn_constrs[constr_idx].next_const_to_add
						&& fzn_constrs[constr_idx].consts[fzn_constrs[constr_idx].next_const_to_add - 1] == 0 && (minus_consts == 1 || plus_consts == 1)) {

					if (minus_consts == 1) {
						j = 0;
						for (i = 0; i < fzn_constrs[constr_idx].next_const_to_add; i++) {
							if (fzn_constrs[constr_idx].consts[i] == 1) {
								vars_idx[j++] = fzn_constrs[constr_idx].vars_id[i];
							}
						}

						if (FZN_VERBOSE)
							printf("Adding new CSP (%d) int_lin_eq (c_sum_var) with variables %d... and result in variable %d", constr_idx, vars_idx[0],
									fzn_constrs[constr_idx].vars_id[minus_idx]);

						fzn_constrs[constr_idx].id = c_sum_var(vars_idx, fzn_constrs[constr_idx].next_var_to_add - 1, fzn_constrs[constr_idx].vars_id[minus_idx]);

						if (FZN_VERBOSE)
							printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);

					} else if (plus_consts == 1) {
						j = 0;
						for (i = 0; i < fzn_constrs[constr_idx].next_const_to_add; i++) {
							if (fzn_constrs[constr_idx].consts[i] == -1) {
								vars_idx[j++] = fzn_constrs[constr_idx].vars_id[i];
							}
						}

						if (FZN_VERBOSE)
							printf("Adding new CSP (%d) int_lin_eq (c_sum_var) with variables %d... and result in variable %d", constr_idx, vars_idx[0],
									fzn_constrs[constr_idx].vars_id[plus_idx]);

						fzn_constrs[constr_idx].id = c_sum_var(vars_idx, fzn_constrs[constr_idx].next_var_to_add - 1, fzn_constrs[constr_idx].vars_id[plus_idx]);

						if (FZN_VERBOSE)
							printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);
					}

				} else if (fzn_constrs[constr_idx].next_var_to_add == 3 && fzn_constrs[constr_idx].next_const_to_add == 4 && fzn_constrs[constr_idx].consts[0] == 1 &&
						fzn_constrs[constr_idx].consts[1] == -1 && fzn_constrs[constr_idx].consts[2] == 1 && fzn_constrs[constr_idx].consts[3] == 0) {

					if (FZN_VERBOSE)
						printf("Adding new CSP (%d) int_lin_eq (c_var_eq_minus) with variables %d, %d and %d", constr_idx, fzn_constrs[constr_idx].vars_id[0],
								fzn_constrs[constr_idx].vars_id[1], fzn_constrs[constr_idx].vars_id[2]);

					fzn_constrs[constr_idx].id = c_var_eq_minus(fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].vars_id[1], fzn_constrs[constr_idx].vars_id[2]);

					if (FZN_VERBOSE)
						printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);

				} else if (fzn_constrs[constr_idx].next_var_to_add == 3 && fzn_constrs[constr_idx].next_const_to_add == 4 && fzn_constrs[constr_idx].consts[0] == 1
						&& fzn_constrs[constr_idx].consts[1] == -1 && fzn_constrs[constr_idx].consts[2] == -1 && fzn_constrs[constr_idx].consts[3] == 0) {

					if (FZN_VERBOSE)
						printf("Adding new CSP (%d) int_lin_eq (c_var_eq_minus) with variables %d, %d and %d", constr_idx, fzn_constrs[constr_idx].vars_id[2],
								fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].vars_id[1]);

					fzn_constrs[constr_idx].id = c_var_eq_minus(fzn_constrs[constr_idx].vars_id[2], fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].vars_id[1]);

					if (FZN_VERBOSE)
						printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);

				} else if (fzn_constrs[constr_idx].next_var_to_add == 2 && fzn_constrs[constr_idx].consts[0] == 1 && fzn_constrs[constr_idx].consts[1] == -1) {

					if (FZN_VERBOSE)
						printf("Adding new CSP (%d) int_lin_eq (c_var_eq_minus) with variables %d and %d, and constants %d, %d and %d", constr_idx,
								fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].vars_id[1], fzn_constrs[constr_idx].consts[0],
								fzn_constrs[constr_idx].consts[1], fzn_constrs[constr_idx].consts[2]);

					fzn_constrs[constr_idx].id = c_minus_eq(fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].vars_id[1], fzn_constrs[constr_idx].consts[2]);

					if (FZN_VERBOSE)
						printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);

				} else if (fzn_constrs[constr_idx].next_var_to_add >= 3
						|| (fzn_constrs[constr_idx].next_var_to_add == 2 && fzn_constrs[constr_idx].consts[0] == 1 && fzn_constrs[constr_idx].consts[1] == 1
								&& fzn_constrs[constr_idx].consts[2] == 1)) {

					if (FZN_VERBOSE)
						printf("Adding new CSP (%d) int_lin_eq (c_linear) with constants %d..., variables %d... and result %d", constr_idx, fzn_constrs[constr_idx].consts[0],
								fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].consts[fzn_constrs[constr_idx].next_var_to_add]);

					fzn_constrs[constr_idx].id = c_linear(fzn_constrs[constr_idx].consts, fzn_constrs[constr_idx].vars_id, fzn_constrs[constr_idx].next_var_to_add,
							fzn_constrs[constr_idx].consts[fzn_constrs[constr_idx].next_var_to_add]);

					if (FZN_VERBOSE)
						printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);

				} else if (fzn_constrs[constr_idx].next_var_to_add == 2 && fzn_constrs[constr_idx].consts[0] > 1 && fzn_constrs[constr_idx].consts[1] == -1
								&& fzn_constrs[constr_idx].consts[2] == 0) {

					if (FZN_VERBOSE)
						printf("Adding new CSP (%d) int_lin_eq (c_linear) with constant %d, variable %d and variable result %d", constr_idx, fzn_constrs[constr_idx].consts[0],
								fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].vars_id[1]);

					fzn_constrs[constr_idx].id = c_linear_var(fzn_constrs[constr_idx].consts, fzn_constrs[constr_idx].vars_id, 1, fzn_constrs[constr_idx].vars_id[1]);

					if (FZN_VERBOSE)
						printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);

				} else {
					fprintf(stderr, "Type of constraint \"%s\" (%d) not recognized.\n", fzn_constrs[constr_idx].name, constr_idx);
					exit(-1);
				}

				free(vars_idx);

			} else if (strcmp(fzn_constrs[constr_idx].name, "int_eq_reif") == 0 && fzn_constrs[constr_idx].next_const_to_add == 1) {

				if (FZN_VERBOSE)
					printf("Adding new CSP (%d) int_eq_reif (c_eq_reif) with variable %d, constant %d and variable %d", constr_idx, fzn_constrs[constr_idx].vars_id[0],
							fzn_constrs[constr_idx].consts[0], fzn_constrs[constr_idx].vars_id[1]);

				fzn_constrs[constr_idx].id = c_eq_reif(fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].consts[0], fzn_constrs[constr_idx].vars_id[1]);

				if (FZN_VERBOSE)
					printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);

			} else if (strcmp(fzn_constrs[constr_idx].name, "int_eq_reif") == 0) {

				if (FZN_VERBOSE)
					printf("Adding new CSP (%d) int_eq_reif (c_eq_var_reif) with variables %d, %d and %d", constr_idx, fzn_constrs[constr_idx].vars_id[0],
							fzn_constrs[constr_idx].vars_id[1], fzn_constrs[constr_idx].vars_id[2]);

				fzn_constrs[constr_idx].id = c_eq_var_reif(fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].vars_id[1], fzn_constrs[constr_idx].vars_id[2]);

				if (FZN_VERBOSE)
					printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);

			} else if (strcmp(fzn_constrs[constr_idx].name, "bool_eq_reif") == 0 && fzn_constrs[constr_idx].next_const_to_add == 0) {

				if (FZN_VERBOSE)
					printf("Adding new CSP (%d) bool_eq_reif (c_eq_var_reif) with variables %d, %d and %d", constr_idx, fzn_constrs[constr_idx].vars_id[0],
							fzn_constrs[constr_idx].vars_id[1], fzn_constrs[constr_idx].vars_id[2]);

				fzn_constrs[constr_idx].id = c_eq_var_reif(fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].vars_id[1], fzn_constrs[constr_idx].vars_id[2]);

				if (FZN_VERBOSE)
					printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);

			} else if (strcmp(fzn_constrs[constr_idx].name, "bool_eq_reif") == 0 && fzn_constrs[constr_idx].next_const_to_add == 1) {

				if (FZN_VERBOSE)
					printf("Adding new CSP (%d) bool_eq_reif (c_eq_reif) with variable %d, value %d and reification variable %d", constr_idx,
							fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].consts[0], fzn_constrs[constr_idx].vars_id[1]);

				fzn_constrs[constr_idx].id = c_eq_reif(fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].consts[0], fzn_constrs[constr_idx].vars_id[1]);

				if (FZN_VERBOSE)
					printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);

			} else if (strcmp(fzn_constrs[constr_idx].name, "bool2int") == 0) {

				if (FZN_VERBOSE)
					printf("Adding new CSP (%d) bool2int (c_bool2int) with variables %d and %d", constr_idx, fzn_constrs[constr_idx].vars_id[0],
							fzn_constrs[constr_idx].vars_id[1]);

				fzn_constrs[constr_idx].id = c_bool2int(fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].vars_id[1]);

				if (FZN_VERBOSE)
					printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);

			} else if (strcmp(fzn_constrs[constr_idx].name, "bool_clause") == 0) {

				if (FZN_VERBOSE)
					printf("Adding new CSP (%d) bool_clause (c_bool_clause) with variables %d...", constr_idx, fzn_constrs[constr_idx].vars_id[0]);

				fzn_constrs[constr_idx].id = c_bool_clause(fzn_constrs[constr_idx].vars_id, fzn_constrs[constr_idx].pos_init_2_array,
						&fzn_constrs[constr_idx].vars_id[fzn_constrs[constr_idx].pos_init_2_array],
						fzn_constrs[constr_idx].next_var_to_add - fzn_constrs[constr_idx].pos_init_2_array);

				if (FZN_VERBOSE)
					printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);

			} else if (strcmp(fzn_constrs[constr_idx].name, "array_var_int_element") == 0) {

				if (fzn_constrs[constr_idx].next_const_to_add == 1) {

					if (FZN_VERBOSE)
						printf("Adding new CSP (%d) array_var_int_element (c_element) with variables %d... and %d and constant %d", constr_idx,
								fzn_constrs[constr_idx].vars_id[1], fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].consts[0]);

					fzn_constrs[constr_idx].id = c_element(&fzn_constrs[constr_idx].vars_id[1], fzn_constrs[constr_idx].next_var_to_add - 1, fzn_constrs[constr_idx].vars_id[0],
							fzn_constrs[constr_idx].consts[0]);

					if (FZN_VERBOSE)
						printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);

				} else {

					if (FZN_VERBOSE)
						printf("Adding new CSP (%d) array_var_int_element (c_element_var) with variables %d..., %d and %d", constr_idx, fzn_constrs[constr_idx].vars_id[1],
								fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].vars_id[fzn_constrs[constr_idx].next_var_to_add - 1]);

					fzn_constrs[constr_idx].id = c_element_var(&fzn_constrs[constr_idx].vars_id[1], fzn_constrs[constr_idx].next_var_to_add - 2, fzn_constrs[constr_idx].vars_id[0],
						fzn_constrs[constr_idx].vars_id[fzn_constrs[constr_idx].next_var_to_add - 1]);

					if (FZN_VERBOSE)
						printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);
				}

			} else if (strcmp(fzn_constrs[constr_idx].name, "array_int_element") == 0) {

				if (FZN_VERBOSE)
					printf("Adding new CSP (%d) array_int_element (c_element_int_var) with variables %d and %d and constants %d...", constr_idx,
							fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].vars_id[1], fzn_constrs[constr_idx].consts[0]);

				fzn_constrs[constr_idx].id = c_element_int_var(fzn_constrs[constr_idx].consts, fzn_constrs[constr_idx].next_const_to_add, fzn_constrs[constr_idx].vars_id[0],
						fzn_constrs[constr_idx].vars_id[1]);

				if (FZN_VERBOSE)
					printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);

			} else if (strcmp(fzn_constrs[constr_idx].name, "array_bool_or") == 0) {

				if (FZN_VERBOSE)
					printf("Adding new CSP (%d) array_bool_or (c_bool_or) with variables %d... and %d", constr_idx, fzn_constrs[constr_idx].vars_id[0],
							fzn_constrs[constr_idx].vars_id[fzn_constrs[constr_idx].next_var_to_add - 1]);

				fzn_constrs[constr_idx].id = c_bool_or(fzn_constrs[constr_idx].vars_id, fzn_constrs[constr_idx].next_var_to_add - 1,
						fzn_constrs[constr_idx].vars_id[fzn_constrs[constr_idx].next_var_to_add - 1]);

				if (FZN_VERBOSE)
					printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);

			} else if (strcmp(fzn_constrs[constr_idx].name, "array_bool_and") == 0) {

				if (FZN_VERBOSE)
					printf("Adding new CSP (%d) array_bool_and (c_bool_and) with variables %d... and %d", constr_idx, fzn_constrs[constr_idx].vars_id[0],
							fzn_constrs[constr_idx].vars_id[fzn_constrs[constr_idx].next_var_to_add - 1]);

				fzn_constrs[constr_idx].id = c_bool_and(fzn_constrs[constr_idx].vars_id, fzn_constrs[constr_idx].next_var_to_add - 1,
						fzn_constrs[constr_idx].vars_id[fzn_constrs[constr_idx].next_var_to_add - 1]);

				if (FZN_VERBOSE)
					printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);

			} else if (strcmp(fzn_constrs[constr_idx].name, "int_lin_ne_reif") == 0) {
				// check if its a "ne" reified constraint
				if (fzn_constrs[constr_idx].next_var_to_add == 3 && fzn_constrs[constr_idx].consts[0] == 1 && fzn_constrs[constr_idx].consts[1] == -1
						&& fzn_constrs[constr_idx].consts[2] == 0) {

					if (FZN_VERBOSE)
						printf("Adding new CSP (%d) int_lin_ne_reif (c_ne_reif) with variables %d, %d and %d", constr_idx, fzn_constrs[constr_idx].vars_id[0],
								fzn_constrs[constr_idx].vars_id[1], fzn_constrs[constr_idx].vars_id[2]);

					fzn_constrs[constr_idx].id = c_ne_reif(fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].vars_id[1], fzn_constrs[constr_idx].vars_id[2]);

					if (FZN_VERBOSE)
						printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);

				} else if (fzn_constrs[constr_idx].next_var_to_add > 3) {

					if (FZN_VERBOSE)
						printf("Adding new CSP (%d) int_lin_ne_reif (c_linear_ne) with variables %d, %d and %d", constr_idx, fzn_constrs[constr_idx].vars_id[0],
								fzn_constrs[constr_idx].vars_id[1], fzn_constrs[constr_idx].vars_id[2]);

					fzn_constrs[constr_idx].id = c_linear_ne_reif(fzn_constrs[constr_idx].consts, fzn_constrs[constr_idx].vars_id,
							fzn_constrs[constr_idx].next_var_to_add - 1, fzn_constrs[constr_idx].consts[fzn_constrs[constr_idx].next_const_to_add - 1],
							fzn_constrs[constr_idx].vars_id[fzn_constrs[constr_idx].next_var_to_add - 1]);

					if (FZN_VERBOSE)
						printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);

				} else {
					fprintf(stderr, "Constraint \"%s\" (%d) not recognized.\n", fzn_constrs[constr_idx].name, constr_idx);
					exit(-1);
				}

			} else if (strcmp(fzn_constrs[constr_idx].name, "int_lin_eq_reif") == 0) {

				// check if it is a sum_var constraint
				int j = 0;
				int plus_consts = 0;
				unsigned int* vars_idx = malloc(fzn_constrs[constr_idx].next_const_to_add * sizeof(unsigned int));

				for (i = 0; i < fzn_constrs[constr_idx].next_const_to_add; i++) {
					if (fzn_constrs[constr_idx].consts[i] == 1) {
						plus_consts++;
					}
				}

				if ((plus_consts + 1 == fzn_constrs[constr_idx].next_const_to_add && fzn_constrs[constr_idx].consts[fzn_constrs[constr_idx].next_const_to_add - 1] != 1)
						|| (plus_consts == fzn_constrs[constr_idx].next_const_to_add)) {

					j = 0;
					for (i = 0; i < fzn_constrs[constr_idx].next_const_to_add - 1; i++) {
						vars_idx[j++] = fzn_constrs[constr_idx].vars_id[i];
					}

					if (FZN_VERBOSE)
						printf("Adding new CSP (%d) int_lin_eq_reif (c_sum_reif) with variables %d..., reification variable %d and result %d", constr_idx, vars_idx[0],
								fzn_constrs[constr_idx].vars_id[fzn_constrs[constr_idx].next_var_to_add - 1],
								fzn_constrs[constr_idx].consts[fzn_constrs[constr_idx].next_const_to_add - 1]);

					fzn_constrs[constr_idx].id = c_sum_reif(vars_idx, fzn_constrs[constr_idx].next_var_to_add - 1,
							fzn_constrs[constr_idx].consts[fzn_constrs[constr_idx].next_const_to_add - 1],
							fzn_constrs[constr_idx].vars_id[fzn_constrs[constr_idx].next_var_to_add - 1]);

					if (FZN_VERBOSE)
						printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);

				} else if (fzn_constrs[constr_idx].next_const_to_add == 2 && fzn_constrs[constr_idx].consts[0] == 1  && fzn_constrs[constr_idx].consts[1] >= 0) {

					if (FZN_VERBOSE)
						printf("Adding new CSP (%d) int_lin_eq_reif (c_eq_reif) with variable %d, constant %d and reification variable %d", constr_idx,
								fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].consts[1], fzn_constrs[constr_idx].vars_id[1]);

					fzn_constrs[constr_idx].id = c_eq_reif(fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].consts[1], fzn_constrs[constr_idx].vars_id[1]);

					if (FZN_VERBOSE)
						printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);

				} else if (fzn_constrs[constr_idx].next_const_to_add == 2 && fzn_constrs[constr_idx].consts[0] == -1  && fzn_constrs[constr_idx].consts[1] <= 0) {

					if (FZN_VERBOSE)
						printf("Adding new CSP (%d) int_lin_eq_reif (c_eq_reif) with variable %d, constant %d and reification variable %d", constr_idx,
								fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].consts[1] * (-1), fzn_constrs[constr_idx].vars_id[1]);

					fzn_constrs[constr_idx].id = c_eq_reif(fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].consts[1] * (-1), fzn_constrs[constr_idx].vars_id[1]);

					if (FZN_VERBOSE)
						printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);

				} else if (fzn_constrs[constr_idx].next_const_to_add == 3 && fzn_constrs[constr_idx].next_var_to_add == 3
						&& fzn_constrs[constr_idx].consts[0] == 1 && fzn_constrs[constr_idx].consts[1] == -1) {

					if (FZN_VERBOSE)
						printf("Adding new CSP (%d) int_lin_eq_reif (c_minus_eq_reif) with variable %d and %d, constant %d and reification variable %d", constr_idx,
								fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].vars_id[1], fzn_constrs[constr_idx].consts[2], fzn_constrs[constr_idx].vars_id[2]);

					fzn_constrs[constr_idx].id = c_minus_eq_reif(fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].vars_id[1], fzn_constrs[constr_idx].consts[2],
							fzn_constrs[constr_idx].vars_id[2]);

					if (FZN_VERBOSE)
						printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);

				} else {

					if (FZN_VERBOSE)
						printf("Adding new CSP (%d) int_lin_eq_reif (c_linear_reif) with variables %d..., constants %d..., result %d and reification variable %d", constr_idx,
								fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].consts[0],
								fzn_constrs[constr_idx].consts[fzn_constrs[constr_idx].next_const_to_add - 1],
								fzn_constrs[constr_idx].vars_id[fzn_constrs[constr_idx].next_var_to_add - 1]);

					fzn_constrs[constr_idx].id = c_linear_reif(fzn_constrs[constr_idx].consts, fzn_constrs[constr_idx].vars_id, fzn_constrs[constr_idx].next_var_to_add - 1,
							fzn_constrs[constr_idx].consts[fzn_constrs[constr_idx].next_const_to_add - 1],
							fzn_constrs[constr_idx].vars_id[fzn_constrs[constr_idx].next_var_to_add - 1]);

					if (FZN_VERBOSE)
						printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);
				}

			} else if (strcmp(fzn_constrs[constr_idx].name, "int_times") == 0) {

				if (FZN_VERBOSE)
					printf("Adding new CSP (%d) int_times (c_var_eq_times) with variables %d, %d and %d", constr_idx, fzn_constrs[constr_idx].vars_id[0],
							fzn_constrs[constr_idx].vars_id[1], fzn_constrs[constr_idx].vars_id[2]);

				fzn_constrs[constr_idx].id = c_var_eq_times(fzn_constrs[constr_idx].vars_id[2], fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].vars_id[1]);

				if (FZN_VERBOSE)
					printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);

			} else if (strcmp(fzn_constrs[constr_idx].name, "all_different") == 0) {

				if (FZN_VERBOSE)
					printf("Adding new CSP (%d) all_different (c_all_different) with variables %d...", constr_idx, fzn_constrs[constr_idx].vars_id[0]);

				fzn_constrs[constr_idx].id = c_all_different(fzn_constrs[constr_idx].vars_id, fzn_constrs[constr_idx].next_var_to_add);

				if (FZN_VERBOSE)
					printf(" as constraint number %d\n",fzn_constrs[constr_idx].id);

			} else {
				fprintf(stderr, "Constraint \"%s\" (%d) not recognized when creating CSP constraint.\n", fzn_constrs[constr_idx].name, constr_idx);
				exit(-1);
			}
		}
	}
}

/*
 * Print the model from the FlatZinc file as interpreted by the interpreter
 */
void fzn_print_csp() {
	int i, j;

	printf("\n\n--------------------------------\n");
	printf("CSP as loaded by the Flatzinc interpreter:\n");

	for (i = 0; i < fzn_next_array_posit; i++) {

		if (!fzn_arrays[i].output_array && !fzn_arrays[i].output_var && !fzn_arrays[i].is_defined_var && !fzn_arrays[i].var_array) {

			printf(" - Array %s, values={", fzn_arrays[i].name);

			for (j = 0; j < fzn_arrays[i].next_position - 1; j++) {
				printf("%d,", fzn_arrays[i].values[j]);
			}
			printf("%d}\n", fzn_arrays[i].values[j]);
		}
	}

	for (i = 0; i < fzn_next_var_posit; i++) {
		printf(" - Variable");

		if (fzn_vars[i].name != NULL) {
			printf(" %s", fzn_vars[i].name);
		}

		printf(", domain={");
		if (fzn_vars[i].range == true) {
			printf("%d..%d}", fzn_vars[i].min, fzn_vars[i].max);

		} else {
			for (j = 0; j < fzn_vars[i].next_position - 1; j++) {
				printf("%d,", fzn_vars[i].values[j]);
			}
			printf("%d}", fzn_vars[i].values[j]);
		}

		if (fzn_vars[i].output_var) {
			printf(", output_var");
		}
		if (fzn_vars[i].var_is_introduced) {
			printf(", var_is_introduced");
		}
		if (fzn_vars[i].is_defined_var) {
			printf(", is_defined_var");
		}
		printf("\n");
	}

	for (i = 0; i < fzn_next_array_posit; i++) {

		if (fzn_arrays[i].output_array) {
			printf(" - Array %s, output_array", fzn_arrays[i].name);

			if (fzn_arrays[i].var_array) {
				printf(", variables={");
				for (j = 0; j < fzn_arrays[i].next_position - 1; j++) {

					if (fzn_vars[fzn_arrays[i].values[j]].name != NULL) {
						printf("%s,", fzn_vars[fzn_arrays[i].values[j]].name);
					} else {
						printf("%d,", fzn_vars[fzn_arrays[i].values[j]].min);
					}
				}
				if (fzn_vars[fzn_arrays[i].values[j]].name != NULL) {
					printf("%s}\n", fzn_vars[fzn_arrays[i].values[j]].name);
				} else {
					printf("%d}\n", fzn_vars[fzn_arrays[i].values[j]].min);
				}

			} else {
				printf(", values={");
				for (j = 0; j < fzn_arrays[i].next_position - 1; j++) {
					printf("%d,", fzn_arrays[i].values[j]);
				}
				printf("%d}\n", fzn_arrays[i].values[j]);
			}
		}
	}

	for (i = 0; i < fzn_next_array_posit; i++) {

		if (!fzn_arrays[i].output_array && !fzn_arrays[i].output_var && !fzn_arrays[i].is_defined_var && fzn_arrays[i].var_array) {

			printf(" - Array %s, variables={", fzn_arrays[i].name);

			for (j = 0; j < fzn_arrays[i].next_position - 1; j++) {
				if (fzn_vars[fzn_arrays[i].values[j]].name != NULL) {
					printf("%s,", fzn_vars[fzn_arrays[i].values[j]].name);
				} else {
					printf("%d,", fzn_vars[fzn_arrays[i].values[j]].min);
				}
			}
			if (fzn_vars[fzn_arrays[i].values[j]].name != NULL) {
				printf("%s}\n", fzn_vars[fzn_arrays[i].values[j]].name);
			} else {
				printf("%d}\n", fzn_vars[fzn_arrays[i].values[j]].min);
			}
		}
	}

	for (i = 0; i < fzn_next_constr_posit; i++) {

		printf(" - Constraint %s", fzn_constrs[i].name);

		if (fzn_constrs[i].next_const_to_add > 0) {
			printf(", values={");
			for (j = 0; j < fzn_constrs[i].next_const_to_add - 1; j++) {
				printf("%d,", fzn_constrs[i].consts[j]);
			}
			printf("%d}", fzn_constrs[i].consts[j]);
		}

		if (fzn_constrs[i].next_var_to_add > 0) {
			printf(", variables={");
			for (j = 0; j < fzn_constrs[i].next_var_to_add - 1; j++) {
				if (fzn_vars[fzn_constrs[i].vars_id[j]].name != NULL) {
					printf("%s,", fzn_vars[fzn_constrs[i].vars_id[j]].name);
				} else {
					printf("%d,", fzn_vars[fzn_constrs[i].vars_id[j]].min);
				}
			}
			if (fzn_vars[fzn_constrs[i].vars_id[j]].name != NULL) {
				printf("%s}", fzn_vars[fzn_constrs[i].vars_id[j]].name);
			} else {
				printf("%d}", fzn_vars[fzn_constrs[i].vars_id[j]].min);
			}
		}

		if (fzn_constrs[i].boundsD != false) {
			printf(", boundsD");
		}
		if (fzn_constrs[i].boundsZ != false) {
			printf(", boundsZ");
		}
		if (fzn_constrs[i].boundsR != false) {
			printf(", boundsR");
		}
		if (fzn_constrs[i].domain != false) {
			printf(", domain");
		}
		if (fzn_constrs[i].priority != false) {
			printf(", priority(%d)", fzn_constrs[i].priority_v_id);
		}

		if (fzn_constrs[i].defines_var_idx != -1) {
			printf(", defines_var(%s)", fzn_vars[fzn_constrs[i].defines_var_idx].name);
		}
		printf("\n");
	}

	// if any search annotation
	if (fzn_next_search_annot_posit > 0) {

		if (fzn_next_search_annot_posit > 1) {
			printf(" - solve seq_search:\n");

			for (i = 0; i < fzn_next_search_annot_posit; i++) {

				printf("    - %s(%s, %s, %s, %s)", fzn_search_annot[i].search_type, fzn_search_annot[i].label_array_name, fzn_search_annot[i].label_heur
						, fzn_search_annot[i].assign_heur, fzn_search_annot[i].search_strategy);

				if (i < fzn_next_search_annot_posit) {
					printf("\n");
				}
			}

			if (FZN_OPTIMIZE == FZN_MINIMIZE) {
				printf("    - minimize %s\n", fzn_vars[optimize_var_idx].name);
			} else if (FZN_OPTIMIZE == FZN_MAXIMIZE) {
				printf("    - maximize %s\n", fzn_vars[optimize_var_idx].name);
			} else {
				printf("    - satisfy");
			}

		} else {

			printf(" - solve %s(%s, %s, %s, %s)", fzn_search_annot[0].search_type, fzn_search_annot[0].label_array_name, fzn_search_annot[0].label_heur
					, fzn_search_annot[0].assign_heur, fzn_search_annot[0].search_strategy);

			if (FZN_OPTIMIZE == FZN_MINIMIZE) {
				printf(" minimize %s\n", fzn_vars[optimize_var_idx].name);
			} else if (FZN_OPTIMIZE == FZN_MAXIMIZE) {
				printf(" maximize %s\n", fzn_vars[optimize_var_idx].name);
			} else {
				printf(" satisfy");
			}
		}
	} else {
		printf(" - solve satisfy");
	}
	printf("\n");
	printf("--------------------------------\n\n");
}

/*
 * Prints each variable and constraint, one by one, from FZN to PHACT representations
 */
void fzn_map_fzn2phact() {

	int prev_val, new_val, cntr, phact_id;
	int fzn_id = 0;
	int i, j, k;

	printf("\nVariables:\n");

	for (i = 0; i < fzn_next_var_posit; i++) {

		phact_id = fzn_vars[i].id;

		if (fzn_vars[i].name != NULL) {
			printf(" - %d -> %s -> ", i, fzn_vars[i].name);

		} else {
			printf(" - %d -> ", i);
		}

		if (!fzn_vars[i].ignore) {
			printf("%d:\n", phact_id);

		} else {
			printf("ignored\n");
		}

		printf("   - FZN");

		if (fzn_vars[i].name != NULL) {
			printf(" %s", fzn_vars[i].name);
		}

		printf(", domain={");
		if (fzn_vars[i].range == true) {
			printf("%d..%d}", fzn_vars[i].min, fzn_vars[i].max);

		} else {
			for (j = 0; j < fzn_vars[i].next_position - 1; j++) {
				printf("%d,", fzn_vars[i].values[j]);
			}
			printf("%d}", fzn_vars[i].values[j]);
		}

		if (fzn_vars[i].output_var) {
			printf(", output_var");
		}
		if (fzn_vars[i].var_is_introduced) {
			printf(", var_is_introduced");
		}
		if (fzn_vars[i].is_defined_var) {
			printf(", is_defined_var");
		}
		printf("\n");

		if (!fzn_vars[i].ignore) {

			printf("   - PHACT ID=%u:  Values={", VS[phact_id].v_id);

			j = 1;
			prev_val = b_get_nth_val(&VS[phact_id].domain_b, j++);
			new_val = prev_val;
			printf("%u", prev_val);
			while (new_val < VS[phact_id].max) {

				cntr = 0;
				while ((new_val = b_get_nth_val(&VS[phact_id].domain_b, j++)) == prev_val + 1 && new_val < VS[phact_id].max) {
					prev_val = new_val;
					cntr++;
				}

				if (cntr == 0) {
					printf(",%u", new_val);
				} else {
					if (new_val == VS[phact_id].max && new_val == prev_val + 1) {
						printf("-%u", new_val);
					} else if (cntr == 1) {
						printf(",%u,%u", prev_val, new_val);
					} else {
						printf("-%u,%u", prev_val, new_val);
					}
				}
				prev_val = new_val;
			}

			if (VS[phact_id].to_label) {
				printf("}  Label=true");
			} else {
				printf("}  Label=false");
			}

			if (VS[phact_id].n_cs > 0) {
				printf("  Constraints={");
				for (j = 0; j < VS[phact_id].n_cs - 1; j++) {
					printf("%u,", VS[phact_id].cs[j]->c_id);
				}
				if (VS[phact_id].n_cs > 0) {
					printf("%u}\n", VS[phact_id].cs[j]->c_id);
				} else {
					printf("\n");
				}
			} else {
				printf("\n");
			}

		} else {
			printf("   - PHACT -> ignored\n");
		}
	}

	printf("\nConstraints:\n");

	for (i = 0; i < fzn_next_constr_posit; i++) {

		phact_id = fzn_constrs[i].id;

		if (fzn_constrs[i].name != NULL) {
			printf(" - %d -> %s -> ", i, fzn_constrs[i].name);
		} else {
			printf(" - %d -> ", i);
		}

		if (!fzn_constrs[i].ignore) {
			printf("%d:\n", phact_id);
		} else {
			printf(" ignored:\n");
		}

		printf("   - FZN");

		printf(" - Constraint %s", fzn_constrs[i].name);

		if (fzn_constrs[i].next_const_to_add > 0) {
			printf(", values={");
			for (j = 0; j < fzn_constrs[i].next_const_to_add - 1; j++) {
				printf("%d,", fzn_constrs[i].consts[j]);
			}
			printf("%d}", fzn_constrs[i].consts[j]);
		}

		if (fzn_constrs[i].next_var_to_add > 0) {
			printf(", variables={");
			for (j = 0; j < fzn_constrs[i].next_var_to_add - 1; j++) {

				phact_id = fzn_constrs[i].vars_id[j];
				for (k = 0; k < fzn_next_var_posit; k++) {
					if (fzn_vars[k].id == (unsigned int)phact_id) {
						phact_id = fzn_vars[k].id;
						fzn_id = k;
						break;
					}
				}

				if (fzn_vars[fzn_id].name != NULL) {
					printf("%s (%d),", fzn_vars[fzn_id].name, fzn_vars[fzn_id].id);
				} else {
					printf("\"\" (%d),", fzn_vars[fzn_id].id);
				}
			}

			phact_id = fzn_constrs[i].vars_id[j];
			for (k = 0; k < fzn_next_var_posit; k++) {
				if (fzn_vars[k].id == (unsigned int)phact_id) {
					phact_id = fzn_vars[k].id;
					fzn_id = k;
					break;
				}
			}

			if (fzn_vars[fzn_id].name != NULL) {
				printf("%s (%d)}", fzn_vars[fzn_id].name, fzn_vars[fzn_id].id);
			} else {
				printf("\"\" (%d)}", fzn_vars[fzn_id].id);
			}
		}

		if (fzn_constrs[i].boundsD != false) {
			printf(", boundsD");
		}
		if (fzn_constrs[i].boundsZ != false) {
			printf(", boundsZ");
		}
		if (fzn_constrs[i].boundsR != false) {
			printf(", boundsR");
		}
		if (fzn_constrs[i].domain != false) {
			printf(", domain");
		}
		if (fzn_constrs[i].priority != false) {
			printf(", priority(%d)", fzn_constrs[i].priority_v_id);
		}

		if (fzn_constrs[i].defines_var_idx != -1) {
			printf(", defines_var(%s)", fzn_vars[fzn_constrs[i].defines_var_idx].name);
		}
		printf("\n");

		if (!fzn_constrs[i].ignore) {

			phact_id = fzn_constrs[i].id;
			printf("   - PHACT ID=%u:  Type=", CS[phact_id].c_id);
			cs_print_type(&CS[phact_id]);
			printf("  Variables={");
			for (j = 0; j < CS[phact_id].n_c_vs - 1; j++) {
				printf("%u,", CS[phact_id].c_vs[j]->v_id);
			}
			printf("%u}", CS[phact_id].c_vs[j]->v_id);

			if (CS[phact_id].n_c_consts > 0) {
				printf("  Constants={");
				for (j = 0; j < CS[phact_id].n_c_consts - 1; j++) {
					printf("%d,", CS[phact_id].c_consts[j]);
				}

				if (CS[phact_id].kind == LINEAR || CS[phact_id].kind == LINEAR_NE || CS[phact_id].kind == LINEAR_LT) {

					printf("%d, %d}", CS[phact_id].c_consts[j], CS[phact_id].constant_val);
				} else {
					printf("%d}", CS[phact_id].c_consts[j]);
				}

			} else if (CS[phact_id].kind == ELEMENT || CS[phact_id].kind == EXACTLY_VAR || CS[phact_id].kind == LINEAR || CS[phact_id].kind == LINEAR_NE
					|| CS[phact_id].kind == MINUS_EQ || CS[phact_id].kind == MINUS_NE || CS[phact_id].kind == SUM_PROD || CS[phact_id].kind == SUM
					|| CS[phact_id].kind == LINEAR_LT || CS[phact_id].kind == ELEMENT_INT_VAR || CS[phact_id].kind == EQ) {
				printf("  Constants={%d}", CS[phact_id].constant_val);
			}

			if (CS[phact_id].reified) {
				printf("  reif_var_ID=%u\n", CS[phact_id].reif_v_id);
			} else {
				printf("\n");
			}

		} else {
			printf("   - PHACT -> ignored\n");
		}
	}
}

/*
 * Initialize the annotation for CSP solving
 */
void fzn_init_search_annots() {
	int i;
	bool more = false;

	if (fzn_next_search_annot_posit > 1) {
		printf("\nCurrent FlatZinc model uses seq_search with multiple heuristics.\n"
				"PHACT can only use one heuristic for labeling and another for value assignment.\n"
				"As such, it will join all the variables/arrays identified as the ones for labeling,\n"
				"but only the first introduced heuristic for labeling and the first introduced heuristic\n"
				"for assignment will be used.\n\n");
	}

	printf("Search annotation with \"[");

	for (i = 0; i < fzn_next_search_annot_posit; i++) {
		fzn_set_var_or_array_to_label(fzn_search_annot[i].label_array_name);

		if (more) {
			printf(", ");
		}
		printf("%s", fzn_search_annot[i].label_array_name);
		more = true;
	}

	printf("], %s, %s, %s", fzn_search_annot[0].label_heur , fzn_search_annot[0].assign_heur , fzn_search_annot[0].search_strategy);

	if (WORK == DEFAULT_W) {
		if (FZN_OPTIMIZE == FZN_MINIMIZE) {
			printf(", minimize %s\"", fzn_vars[optimize_var_idx].name);

		} else if (FZN_OPTIMIZE == FZN_MAXIMIZE) {
			printf(", maximize %s\"", fzn_vars[optimize_var_idx].name);

		} else {
			printf("\"");
		}
	} else {
		printf("\"");
	}
	printf("\n\n");

	// label heuristic
	if (strcmp("input_order", fzn_search_annot[0].label_heur) == 0) {
		LABEL_MODE = INPUT_ORDER;

	} else if (strcmp("occurrence", fzn_search_annot[0].label_heur) == 0) {
		LABEL_MODE = OCCURRENCE;

	} else if (strcmp("first_fail", fzn_search_annot[0].label_heur) == 0) {
		LABEL_MODE = FIRST_FAIL;

	} /*else if (strcmp("max_regret", fzn_search_annot[0].label_heur) == 0) {
		LABEL_MODE = MAX_REGRET;

	} else if (strcmp("smallest", fzn_search_annot[0].label_heur) == 0) {
		LABEL_MODE = SMALLEST;

	}*/ else {
		LABEL_MODE = INPUT_ORDER;
		printf("The %s heuristic for labeling is not implemented. Using default heuristic (INPUT_ORDER).\n", fzn_search_annot[0].label_heur);
	}


	// assignment heuristic
	if (strcmp("indomain_min", fzn_search_annot[0].assign_heur) == 0) {
		ASSIGN_MODE = MIN_VAL;

	} else if (strcmp("indomain_max", fzn_search_annot[0].assign_heur) == 0) {
		ASSIGN_MODE = MAX_VAL;

	} else if (strcmp("indomain_split", fzn_search_annot[0].assign_heur) == 0) {
		ASSIGN_MODE = SPLIT_VALS;

	} else {
		ASSIGN_MODE = MIN_VAL;
		printf("The %s heuristic for value selection is not implemented. Using default heuristic (MIN_VAL).\n", fzn_search_annot[0].assign_heur);
	}

	if (strcmp("complete", fzn_search_annot[0].search_strategy) != 0) {
		fprintf(stderr, "%s search strategy not implemented.\n", fzn_search_annot[0].search_strategy);
		exit(-1);
	}
}



/*
 * Print the number of variables, constraints, types of constraints and maximum domain value of the FlatZinc model
 */
void fzn_print_stats() {
	char constraints_name[100][30];	// values higher than the ones in FlatZinc specification
	int cs_ctr = 0;
	int max_dom = 0;
	int i, j;

	printf("\nFlatZinc model statistics:\n");

	printf(" - Number of variables:    %d\n", fzn_next_var_posit);

	for (i = 0; i < fzn_next_var_posit; i++) {

		if (fzn_vars[i].range == true && fzn_vars[i].max > max_dom) {
			max_dom =  fzn_vars[i].max;

		} else {
			for (j = 0; j < fzn_vars[i].next_position - 1; j++) {
				if (fzn_vars[i].values[j] > max_dom) {
					max_dom =  fzn_vars[i].values[j];
				}
			}
		}
	}

	printf(" - Maximum domain value:   %d\n", max_dom);
	printf(" - Number of constraints:  %d\n", fzn_next_constr_posit);

	for (i = 0; i < fzn_next_constr_posit; i++) {

		for (j = 0; j < cs_ctr; j++) {
			if (strcmp(fzn_constrs[i].name, constraints_name[j]) == 0) {
				break;
			}
		}

		if (j == cs_ctr) {
			strcpy(constraints_name[cs_ctr++], fzn_constrs[i].name);
		}
	}

	printf(" - Types of constraints:  %d\n", cs_ctr);
}