/*
 * 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 "actions.h"

#include "../../constraints/all_different.h"

#include "../../constraints/array_bool_and.h"
#include "../../constraints/array_bool_element.h"
#include "../../constraints/array_bool_or.h"
#include "../../constraints/array_bool_xor.h"
#include "../../constraints/array_int_element.h"
#include "../../constraints/array_var_int_element.h"

#include "../../constraints/at_least.h"

#include "../../constraints/at_most.h"

#include "../../constraints/at_most_one.h"

#include "../../constraints/bool_and.h"
#include "../../constraints/bool_clause.h"

#include "../../constraints/bool_eq.h"
#include "../../constraints/bool_le.h"
#include "../../constraints/bool_lin_eq.h"
#include "../../constraints/bool_lin_le.h"
#include "../../constraints/bool_lt.h"
#include "../../constraints/bool_not.h"

#include "../../constraints/bool_or.h"

#include "../../constraints/bool_xor.h"
#include "../../constraints/bool2int.h"

#include "../../constraints/element.h"

#include "../../constraints/int_eq.h"

#include "../../constraints/exactly.h"

#include "../../constraints/exactly_var.h"

#include "../../constraints/fake_all_different.h"
#include "../../constraints/ge.h"
#include "../../constraints/gt.h"

#include "../../constraints/int_div.h"
#include "../../constraints/int_eq_c.h"
#include "../../constraints/int_le.h"
#include "../../constraints/int_lin_le.h"
#include "../../constraints/int_lin_ne.h"
#include "../../constraints/int_lin_var.h"
#include "../../constraints/int_lin_eq.h"
#include "../../constraints/int_lt.h"
#include "../../constraints/int_max.h"
#include "../../constraints/int_min.h"
#include "../../constraints/int_mod.h"
#include "../../constraints/int_ne.h"
#include "../../constraints/int_plus.h"
#include "../../constraints/int_times.h"

#include "../../constraints/maximize.h"

#include "../../constraints/minimize.h"
#include "../../constraints/minus_eq.h"
#include "../../constraints/minus_ne.h"

#include "../../constraints/sum.h"

#include "../../constraints/sum_prod.h"
#include "../../constraints/sum_var.h"

#include "../../constraints/var_eq_minus.h"
#include "../../constraints/var_eq_minus_abs.h"

#include "../../constraints.h"
#include "../benchmark.h"
#include "../../config.h"
#include "../../split.h"
#include "../../variables.h"
#include "../../bitmaps.h"

#if COMPILE_FZN

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

// for elapse time calculation

struct timeval start, end;

char start_time[40];
char end_time[40];
char elapsed_time[40];

bool vs_to_label_set = false;	// true if any variable with more than one value in its domain was set for labeling

/*
 * Translate the flatzinc file to a PHACT representation of a CSP

 * fzn_file_name - name of the FlatZinc file containing the CSP model

 */

void parse(char *fzn_file_name) {

	int i;

	gettimeofday(&start, NULL);

	if (!(yyin = fopen(fzn_file_name, "r"))) {

		printf("\nFile %s does not exist.\n", fzn_file_name);

#if defined(WIN32) || defined(_WIN32) || defined(__WIN32) && !defined(__CYGWIN__)
		printf("\nPress any key to exit\n");
		int a = getchar();
#endif

		exit(0);

	}

	// 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((unsigned int) fzn_n_vars * sizeof(fzn_var));
	fzn_constrs = malloc((unsigned int) fzn_n_constrs * sizeof(fzn_constr));
	fzn_arrays = malloc((unsigned int) fzn_n_arrays * sizeof(fzn_array));
	fzn_output_arrays = malloc((unsigned int) fzn_n_output_arrays * sizeof(fzn_output_array));
	fzn_search_annot = malloc((unsigned int) 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);
	}

#if FZN_SEQ
	free(FZN_SEQ_LABELS);
	free(FZN_SEQ_ASSIGNS);
#endif

	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 = (unsigned int) fzn_next_var_posit;
	N_CS_ORIGINAL = (unsigned int) 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((unsigned int) 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((unsigned int) fzn_arrays[i].values[j]);

			}
		}
	}

#if FZN_LABEL_DEFINED_VARS
	bool defined_var = false;
#endif

	// 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) {
		if (!QUIET) {

			printf("Some variables marked as \"is_defined_var\" were also set for labeling.\n\n");
		}

	}

#endif

		if (!vs_to_label_set) {

			if (!QUIET) {
				printf("No variable with more than one value was marked for labeling, 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].is_defined_var) {

					fzn_vars[i].to_label = false;

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

					vs_to_label_set = true;
				}
			}

			if (!vs_to_label_set) {

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

					if (fzn_vars[i].min != fzn_vars[i].max) {
						fzn_vars[i].to_label = true;
						vs_to_label_set = true;
					}

				}
			}
		}

	} else {
		// set output variables for labeling
		output_vars = false;

#if LABEL_OUTPUT_VS
	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;

				}
			}
		}

	}
#endif

		if (!output_vars) {

			if (!QUIET) {
				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].is_defined_var) {

					fzn_vars[i].to_label = false;

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

					vs_to_label_set = true;
				}
			}

			if (!vs_to_label_set) {

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

					if (fzn_vars[i].min != fzn_vars[i].max) {
						fzn_vars[i].to_label = true;
						vs_to_label_set = true;
					}

				}
			}

		} else {

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

		}
	}

#if FZN_LABEL_ALL_VARS

if (!QUIET) {
	printf("\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 {

			FINDING_ONE_SOLUTION = true;
			WORK = ONE;

		}
	}

	// 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;

					j < fzn_next_constr_posit && 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(((unsigned int) 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((unsigned int) 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_id = -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((unsigned int) 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((unsigned int) fzn_vars[optimize_var_idx].id);

	} else if (FZN_OPTIMIZE == FZN_MAXIMIZE) {

		c_maximize((unsigned int) 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 (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("\n%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

	// run PHACT

	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((unsigned int) 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((unsigned int) 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((unsigned int) 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((unsigned int) 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((unsigned int) 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((unsigned int) 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, "\nError: variable or array name not found when adding it to a fzn_obj.\n");

#if defined(WIN32) || defined(_WIN32) || defined(__WIN32) && !defined(__CYGWIN__)
			printf("\nPress any key to exit\n");
			int a = getchar();
#endif

			exit(0);

		}
	}
}

/*
 * Define fzn_obj range as true or false

 * range - if its a variable whose domain is a range

 */
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

 * annot - annotation to add

 */

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((unsigned int) 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) {

		printf("\nPHACT can only work with \"int_search\" or \"bool_search\" annotations (not %s).\n", annot);

#if defined(WIN32) || defined(_WIN32) || defined(__WIN32) && !defined(__CYGWIN__)
		printf("\nPress any key to exit\n");
		int a = getchar();
#endif

		exit(0);

	} 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((unsigned int) fzn_obj.max_elements * 2 * (sizeof(int)));
		fzn_obj.element_is_var_aux = malloc((unsigned int) 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((unsigned int) 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, "\nError: Trying to add an annotation number %d that is empty to array number %d.\n", i, fzn_next_array_posit);

#if defined(WIN32) || defined(_WIN32) || defined(__WIN32) && !defined(__CYGWIN__)
			printf("\nPress any key to exit\n");
			int a = getchar();
#endif

			exit(0);

		}

		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, "\nError: Trying to name array with %s when its name is already %s.\n", fzn_arrays[fzn_next_array_posit].name,
						fzn_obj.annots[i]);

#if defined(WIN32) || defined(_WIN32) || defined(__WIN32) && !defined(__CYGWIN__)
				printf("\nPress any key to exit\n");
				int a = getchar();
#endif

				exit(0);

			}
		}
	}

	// 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((unsigned int) 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, "\nError: Attempting to add a variable with no name to an array.\n");

#if defined(WIN32) || defined(_WIN32) || defined(__WIN32) && !defined(__CYGWIN__)
		printf("\nPress any key to exit\n");
		int a = getchar();
#endif

		exit(0);

	}

	// 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((unsigned int) 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, "\nError: Variable name %s not found when adding it to an array.\n", var_name);

#if defined(WIN32) || defined(_WIN32) || defined(__WIN32) && !defined(__CYGWIN__)
		printf("\nPress any key to exit\n");
		int a = getchar();
#endif

		exit(0);

	}

	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((unsigned int) 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 < 0 || max < 0) {

		printf("\nPHACT 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");

#if defined(WIN32) || defined(_WIN32) || defined(__WIN32) && !defined(__CYGWIN__)
		printf("\nPress any key to exit\n");
		int a = getchar();
#endif

		exit(0);
	}

	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].replace_other_v = false;
	fzn_vars[fzn_next_var_posit].created = false;
#if FZN_SEQ
	fzn_vars[fzn_next_var_posit].label_h = LABEL_MODE_D;
	fzn_vars[fzn_next_var_posit].assign_h = ASSIGN_MODE_D;
#endif
	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 (val < 0) {

		printf("\nPHACT 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");

#if defined(WIN32) || defined(_WIN32) || defined(__WIN32) && !defined(__CYGWIN__)
		printf("\nPress any key to exit\n");
		int a = getchar();
#endif

		exit(0);
	}

	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].max == val && fzn_vars[i].range == true && fzn_vars[i].name == NULL && !fzn_vars[i].ignore) {

				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].replace_other_v = false;
	fzn_vars[fzn_next_var_posit].var_is_introduced = false;
	fzn_vars[fzn_next_var_posit].created = false;
#if FZN_SEQ
	fzn_vars[fzn_next_var_posit].label_h = LABEL_MODE_D;
	fzn_vars[fzn_next_var_posit].assign_h = ASSIGN_MODE_D;
#endif

	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);
	}

	if (fzn_obj.next_element == 0) {
		printf("This FlatZinc model contains variables with a domain not defined, which is not supported by PHACT.\n");

#if defined(WIN32) || defined(_WIN32) || defined(__WIN32) && !defined(__CYGWIN__)
		printf("\nPress any key to exit\n");
		int a = getchar();
#endif

		exit(0);
	}

	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 && !fzn_vars[i].ignore) {

				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].replace_other_v = false;
	fzn_vars[fzn_next_var_posit].var_is_introduced = false;
	fzn_vars[fzn_next_var_posit].created = false;
#if FZN_SEQ
	fzn_vars[fzn_next_var_posit].label_h = LABEL_MODE_D;
	fzn_vars[fzn_next_var_posit].assign_h = ASSIGN_MODE_D;
#endif

	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, "\nError: Trying to name variable with %s when its name is already %s.\n", fzn_vars[fzn_next_var_posit].name,
						fzn_obj.annots[i]);

#if defined(WIN32) || defined(_WIN32) || defined(__WIN32) && !defined(__CYGWIN__)
				printf("\nPress any key to exit\n");
				int a = getchar();
#endif

				exit(0);

			}
		}
	}

	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);

		}

		if (min < 0 || max < 0) {

			printf("\nPHACT 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");

#if defined(WIN32) || defined(_WIN32) || defined(__WIN32) && !defined(__CYGWIN__)
			printf("\nPress any key to exit\n");
			int a = getchar();
#endif

			exit(0);
		}

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

	} else {

		for (i = 0; i < fzn_obj.next_element; i++) {
			if (fzn_obj.elements[i] < 0) {
				printf("\nPHACT 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");

#if defined(WIN32) || defined(_WIN32) || defined(__WIN32) && !defined(__CYGWIN__)
				printf("\nPress any key to exit\n");
				int a = getchar();
#endif

				exit(0);
			}
		}

		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((unsigned int) 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++) {

			if (fzn_obj.elements[i] < 0) {

				printf("\nPHACT 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");

#if defined(WIN32) || defined(_WIN32) || defined(__WIN32) && !defined(__CYGWIN__)
				printf("\nPress any key to exit\n");
				int a = getchar();
#endif

				exit(0);
			}
			fzn_vars[fzn_next_var_posit].values[i] = (unsigned int) 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];

		if (fzn_obj.elements[0] < 0 || fzn_obj.elements[fzn_obj.next_element - 1] < 0) {

			printf("\nPHACT 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");

#if defined(WIN32) || defined(_WIN32) || defined(__WIN32) && !defined(__CYGWIN__)
			printf("\nPress any key to exit\n");
			int a = getchar();
#endif

			exit(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_replace_fzn_v_id(fzn_next_var_posit, 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_vars[fzn_next_var_posit].replace_other_v = false;

	}

	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].replace_other_v = src[i].replace_other_v;

		dest[i].created = src[i].created;

#if FZN_SEQ
		dest[i].label_h = src[i].label_h;
		dest[i].assign_h = src[i].assign_h;
#endif

	}
}

/*
 * 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((unsigned int) 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

 * var_name - name 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((unsigned int) 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(
				(unsigned int) 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((unsigned int) 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_id = -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_id = 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 || strcmp(fzn_obj.annots[i], "bounds") == 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, "\nError: Trying to name constraint with %s when its name is already %s.\n", fzn_constrs[fzn_next_constr_posit].name,
						fzn_obj.annots[i]);

#if defined(WIN32) || defined(_WIN32) || defined(__WIN32) && !defined(__CYGWIN__)
				printf("\nPress any key to exit\n");
				int a = getchar();
#endif

				exit(0);

			}
		}
	}

	if (strcmp(fzn_constrs[fzn_next_constr_posit].name, "int_lt") == 0 || strcmp(fzn_constrs[fzn_next_constr_posit].name, "int_le") == 0
			|| strcmp(fzn_constrs[fzn_next_constr_posit].name, "bool_le") == 0 || strcmp(fzn_constrs[fzn_next_constr_posit].name, "bool_lt") == 0
			|| strcmp(fzn_constrs[fzn_next_constr_posit].name, "bool_not") == 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
			|| strcmp(fzn_constrs[fzn_next_constr_posit].name, "int_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_INT_EQ

			fzn_replace_fzn_v_id(fzn_obj.elements[1], fzn_obj.elements[0]);
			fzn_constrs[fzn_next_constr_posit].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);

#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 if (fzn_obj.element_is_var[0] && !fzn_obj.element_is_var[1]) {

#if FZN_REPLACE_INT_EQ

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

			fzn_constrs[fzn_next_constr_posit].max_vars = 1;
			fzn_constrs[fzn_next_constr_posit].max_consts = 1;

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

			fzn_constrs[fzn_next_constr_posit].ignore = true;

			if (fzn_obj.elements[1]) {

				printf("\nPHACT 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");

#if defined(WIN32) || defined(_WIN32) || defined(__WIN32) && !defined(__CYGWIN__)
				printf("\nPress any key to exit\n");
				int a = getchar();

#endif

				exit(0);
			}

			fzn_vars[fzn_obj.elements[0]].min = fzn_obj.elements[1];
			fzn_vars[fzn_obj.elements[0]].max = fzn_obj.elements[1];

			if (fzn_vars[fzn_obj.elements[0]].ignore) {
				fzn_intersect_fzn_vars(fzn_vars[fzn_obj.elements[0]].replace_by_v_id, fzn_obj.elements[0]);
			}

			if (fzn_vars[fzn_obj.elements[0]].replace_other_v) {

				for (i = 0; i < fzn_next_var_posit; i++) {
					if (fzn_vars[i].replace_by_v_id == fzn_obj.elements[0]) {

						fzn_intersect_fzn_vars(i, fzn_obj.elements[0]);
					}
				}
			}
#else
			fzn_constrs[fzn_next_constr_posit].vars_id = malloc(2 * sizeof(unsigned int));

			fzn_constrs[fzn_next_constr_posit].max_vars = 2;

			fzn_constrs[fzn_next_constr_posit].max_consts = 0;

			fzn_add_fzn_obj_elem_var_to_constr(0);
			fzn_add_fzn_obj_elem_var_to_constr(1);

#endif

		} else {

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

				fprintf(stderr, "\nError: fzn_obj has values instead of variables when ignoring constraint %s (%d).\n", fzn_obj.annots[0],
						fzn_next_constr_posit);

#if defined(WIN32) || defined(_WIN32) || defined(__WIN32) && !defined(__CYGWIN__)
				printf("\nPress any key to exit\n");
				int a = getchar();
#endif

				exit(0);

			} else {
				fzn_constrs[fzn_next_constr_posit].consts = malloc(2 * sizeof(int));
				fzn_constrs[fzn_next_constr_posit].max_consts = 2;

				fzn_add_fzn_obj_elem_val_to_constr(0);
				fzn_add_fzn_obj_elem_val_to_constr(1);
				fzn_constrs[fzn_next_constr_posit].ignore = true;
			}

		}

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

		fzn_constrs[fzn_next_constr_posit].vars_id = malloc((unsigned int) 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_ne") == 0 && fzn_obj.element_is_var[1]) {

		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, "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_div") == 0 || strcmp(fzn_constrs[fzn_next_constr_posit].name, "int_plus") == 0
			|| strcmp(fzn_constrs[fzn_next_constr_posit].name, "int_max") == 0 || strcmp(fzn_constrs[fzn_next_constr_posit].name, "int_min") == 0
			|| strcmp(fzn_constrs[fzn_next_constr_posit].name, "int_mod") == 0 || strcmp(fzn_constrs[fzn_next_constr_posit].name, "bool_and") == 0
			|| strcmp(fzn_constrs[fzn_next_constr_posit].name, "bool_or") == 0 || strcmp(fzn_constrs[fzn_next_constr_posit].name, "bool_xor") == 0
			|| strcmp(fzn_constrs[fzn_next_constr_posit].name, "bool_le_reif") == 0 || strcmp(fzn_constrs[fzn_next_constr_posit].name, "bool_lt_reif") == 0
			|| strcmp(fzn_constrs[fzn_next_constr_posit].name, "bool_not_reif") == 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_eq") == 0) {

		if (fzn_obj.next_element == 1 && !fzn_obj.element_is_var[0] && fzn_obj.elements[0] == 0) {

			fzn_constrs[fzn_next_constr_posit].consts = malloc(sizeof(unsigned int));
			fzn_constrs[fzn_next_constr_posit].max_consts = 1;
			fzn_constrs[fzn_next_constr_posit].consts[0] = fzn_obj.elements[0];
			fzn_constrs[fzn_next_constr_posit].ignore = true;

			fzn_add_fzn_obj_elem_val_to_constr(0);

		} else {

			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((unsigned int) n_consts * sizeof(int));
			fzn_constrs[fzn_next_constr_posit].vars_id = malloc((unsigned int) 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") == 0) {

		if (fzn_obj.next_element == 1 && !fzn_obj.element_is_var[0] && fzn_obj.elements[0] != 0) {

			fzn_constrs[fzn_next_constr_posit].consts = malloc(sizeof(unsigned int));
			fzn_constrs[fzn_next_constr_posit].max_consts = 1;
			fzn_constrs[fzn_next_constr_posit].consts[0] = fzn_obj.elements[0];
			fzn_constrs[fzn_next_constr_posit].ignore = true;

			fzn_add_fzn_obj_elem_val_to_constr(0);

		} else {

			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((unsigned int) n_consts * sizeof(int));
			fzn_constrs[fzn_next_constr_posit].vars_id = malloc((unsigned int) 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_le") == 0) {

		if (fzn_obj.next_element == 1 && !fzn_obj.element_is_var[0] && fzn_obj.elements[0] >= 0) {

			fzn_constrs[fzn_next_constr_posit].consts = malloc(sizeof(unsigned int));
			fzn_constrs[fzn_next_constr_posit].max_consts = 1;
			fzn_constrs[fzn_next_constr_posit].consts[0] = fzn_obj.elements[0];
			fzn_constrs[fzn_next_constr_posit].ignore = true;

			fzn_add_fzn_obj_elem_val_to_constr(0);

		} else {

			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((unsigned int) n_consts * sizeof(int));
			fzn_constrs[fzn_next_constr_posit].vars_id = malloc((unsigned int) 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, "bool_lin_le") == 0) {

		if (fzn_obj.next_element == 1 && !fzn_obj.element_is_var[0] && fzn_obj.elements[0] == 0) {

			fzn_constrs[fzn_next_constr_posit].consts = malloc(sizeof(unsigned int));
			fzn_constrs[fzn_next_constr_posit].max_consts = 1;
			fzn_constrs[fzn_next_constr_posit].consts[0] = fzn_obj.elements[0];
			fzn_constrs[fzn_next_constr_posit].ignore = true;

			fzn_add_fzn_obj_elem_val_to_constr(0);

		} else {

			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((unsigned int) n_consts * sizeof(int));
			fzn_constrs[fzn_next_constr_posit].vars_id = malloc((unsigned int) 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, "bool_lin_eq") == 0) {

		if (fzn_obj.next_element == 1 && !fzn_obj.element_is_var[0] && fzn_obj.elements[0] == 0) {

			fzn_constrs[fzn_next_constr_posit].consts = malloc(sizeof(unsigned int));
			fzn_constrs[fzn_next_constr_posit].max_consts = 1;
			fzn_constrs[fzn_next_constr_posit].consts[0] = fzn_obj.elements[0];
			fzn_constrs[fzn_next_constr_posit].ignore = true;

			fzn_add_fzn_obj_elem_val_to_constr(0);

		} else {

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

			fzn_constrs[fzn_next_constr_posit].consts = malloc((unsigned int) n_consts * sizeof(int));
			fzn_constrs[fzn_next_constr_posit].vars_id = malloc((unsigned int) 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 - 1) / 2; i++) {
				fzn_add_fzn_obj_elem_val_to_constr(i);
			}
			for (; i < fzn_obj.next_element - 1; i++) {
				fzn_add_fzn_obj_elem_var_to_constr(i);
			}
			fzn_add_fzn_obj_elem_var_to_constr(i);
		}

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

		if ((fzn_obj.next_element == 2 && !fzn_obj.element_is_var[0] && fzn_obj.elements[0] == 0 && !fzn_obj.element_is_var[1] && fzn_obj.elements[1] == 1)
				|| (fzn_obj.next_element == 2 && !fzn_obj.element_is_var[0] && fzn_obj.elements[0] != 0 && !fzn_obj.element_is_var[1]
						&& fzn_obj.elements[1] == 0)) {

			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_constrs[fzn_next_constr_posit].ignore = true;

			fzn_add_fzn_obj_elem_val_to_constr(0);
			fzn_add_fzn_obj_elem_var_to_constr(1);

		} else {

			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((unsigned int) n_consts * sizeof(int));
			fzn_constrs[fzn_next_constr_posit].vars_id = malloc((unsigned int) 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, "int_lin_ne_reif") == 0) {

		if ((fzn_obj.next_element == 2 && !fzn_obj.element_is_var[0] && fzn_obj.elements[0] == 0 && !fzn_obj.element_is_var[1] && fzn_obj.elements[1] == 0)
				|| (fzn_obj.next_element == 2 && !fzn_obj.element_is_var[0] && fzn_obj.elements[0] != 0 && !fzn_obj.element_is_var[1]
						&& fzn_obj.elements[1] == 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_constrs[fzn_next_constr_posit].ignore = true;

			fzn_add_fzn_obj_elem_val_to_constr(0);
			fzn_add_fzn_obj_elem_var_to_constr(1);

		} else {

			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((unsigned int) n_consts * sizeof(int));
			fzn_constrs[fzn_next_constr_posit].vars_id = malloc((unsigned int) 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, "int_lin_le_reif") == 0) {

		if ((fzn_obj.next_element == 2 && !fzn_obj.element_is_var[0] && fzn_obj.elements[0] >= 0 && !fzn_obj.element_is_var[1] && fzn_obj.elements[1] == 1)
				|| (fzn_obj.next_element == 2 && !fzn_obj.element_is_var[0] && fzn_obj.elements[0] <= 0 && !fzn_obj.element_is_var[1]
						&& fzn_obj.elements[1] == 0)) {

			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_constrs[fzn_next_constr_posit].ignore = true;

			fzn_add_fzn_obj_elem_val_to_constr(0);
			fzn_add_fzn_obj_elem_var_to_constr(1);

		} else {

			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((unsigned int) n_consts * sizeof(int));
			fzn_constrs[fzn_next_constr_posit].vars_id = malloc((unsigned int) 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
			|| strcmp(fzn_constrs[fzn_next_constr_posit].name, "array_bool_xor") == 0) {

		fzn_constrs[fzn_next_constr_posit].vars_id = malloc((unsigned int) 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
			|| strcmp(fzn_constrs[fzn_next_constr_posit].name, "array_bool_element") == 0
			|| strcmp(fzn_constrs[fzn_next_constr_posit].name, "array_var_bool_element") == 0) {

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

			fzn_constrs[fzn_next_constr_posit].vars_id = malloc((unsigned int) 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(((unsigned int) 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(((unsigned int) 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);

			if (fzn_obj.elements[i] < 0) {
				fprintf(stderr, "\nError: A constraint array_int_element contains negative values in its constants list. This is not supported by PHACT.\n");

#if defined(WIN32) || defined(_WIN32) || defined(__WIN32) && !defined(__CYGWIN__)
				printf("\nPress any key to exit\n");
				int a = getchar();
#endif

				exit(0);
			}

		}
		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, "\nError: Constraint \"%s\" (%d) not recognized when creating FZN constraint.\n", fzn_constrs[fzn_next_constr_posit].name,
				fzn_next_constr_posit);

#if defined(WIN32) || defined(_WIN32) || defined(__WIN32) && !defined(__CYGWIN__)
		printf("\nPress any key to exit\n");
		int a = getchar();
#endif

		exit(0);

	}

	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, "\nError: no variables when constructing fzn constraint %s.\n", fzn_constrs[fzn_next_constr_posit].name);

#if defined(WIN32) || defined(_WIN32) || defined(__WIN32) && !defined(__CYGWIN__)
		printf("\nPress any key to exit\n");
		int a = getchar();
#endif

		exit(0);

	}

	// 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((unsigned int) 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[(unsigned int) fzn_constrs[fzn_next_constr_posit].next_var_to_add] = (unsigned int) 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, "\nError: no constants when constructing fzn constraint %s.\n", fzn_constrs[fzn_next_constr_posit].name);

#if defined(WIN32) || defined(_WIN32) || defined(__WIN32) && !defined(__CYGWIN__)
		printf("\nPress any key to exit\n");
		int a = getchar();
#endif

		exit(0);

	}

	// 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((unsigned int) 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, "\nError: value marked as variable when constructing fzn constraint %s.\n", fzn_constrs[fzn_next_constr_posit].name);

#if defined(WIN32) || defined(_WIN32) || defined(__WIN32) && !defined(__CYGWIN__)
		printf("\nPress any key to exit\n");
		int a = getchar();
#endif

		exit(0);

	}

	// 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_id = src[i].defines_var_id;

		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((unsigned int) 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((unsigned int) 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 a fzn_var to be replaced by another
 * v_id_to_be_replaced - FlatZinc ID of the variable to be replaced
 * v_id_to_replace_the_other - FlatZinc ID of the variable to replace the variabel whose ID is v_id_to_be_replaced
 */
void fzn_replace_fzn_v_id(int v_id_to_be_replaced, int v_id_to_replace_the_other) {

	if (fzn_vars[v_id_to_be_replaced].replace_by_v_id != -1) {

		if (FZN_VERBOSE)
			printf("Replacing variable %s by variable %s\n", fzn_vars[fzn_vars[v_id_to_be_replaced].replace_by_v_id].name,
					fzn_vars[v_id_to_replace_the_other].name);

		if (fzn_vars[v_id_to_be_replaced].to_label || fzn_vars[v_id_to_replace_the_other].to_label
				|| fzn_vars[fzn_vars[v_id_to_be_replaced].replace_by_v_id].to_label) {
			fzn_vars[v_id_to_be_replaced].to_label = true;
			fzn_vars[v_id_to_replace_the_other].to_label = true;
			fzn_vars[fzn_vars[v_id_to_be_replaced].replace_by_v_id].to_label = true;
		}

		if (FZN_VERBOSE)
			printf("Replacing variables %s and %s by variable %s\n", fzn_vars[v_id_to_be_replaced].name,
					fzn_vars[fzn_vars[v_id_to_be_replaced].replace_by_v_id].name, fzn_vars[v_id_to_replace_the_other].name);

		fzn_intersect_fzn_vars(fzn_vars[v_id_to_be_replaced].replace_by_v_id, v_id_to_replace_the_other);
		fzn_intersect_fzn_vars(v_id_to_be_replaced, v_id_to_replace_the_other);
		fzn_intersect_fzn_vars(fzn_vars[v_id_to_be_replaced].replace_by_v_id, v_id_to_be_replaced);

		fzn_vars[fzn_vars[v_id_to_be_replaced].replace_by_v_id].replace_by_v_id = v_id_to_replace_the_other;
		fzn_vars[fzn_vars[v_id_to_be_replaced].replace_by_v_id].ignore = true;

		fzn_vars[v_id_to_be_replaced].replace_by_v_id = v_id_to_replace_the_other;
		fzn_vars[v_id_to_be_replaced].ignore = true;

	} else {

		if (fzn_vars[v_id_to_be_replaced].to_label || fzn_vars[v_id_to_replace_the_other].to_label) {
			fzn_vars[v_id_to_be_replaced].to_label = true;
			fzn_vars[v_id_to_replace_the_other].to_label = true;
		}

		if (FZN_VERBOSE)
			printf("Replacing variable %s by variable %s\n", fzn_vars[v_id_to_be_replaced].name, fzn_vars[v_id_to_replace_the_other].name);

		fzn_intersect_fzn_vars(v_id_to_be_replaced, v_id_to_replace_the_other);

		fzn_vars[v_id_to_be_replaced].replace_by_v_id = v_id_to_replace_the_other;
		fzn_vars[v_id_to_be_replaced].ignore = true;
	}

	fzn_vars[v_id_to_replace_the_other].replace_other_v = true;
}

/*
 * Intersect the domain of two fzn_vars and place the result in the first fzn_var
 * v_id_to_be_replaced - id of the first fzn_var, to be replaced by the intersection result
 * v_id_to_replace_the_other - id if the second fzn_var
 */
void fzn_intersect_fzn_vars(int v_id_to_be_replaced, int v_id_to_replace_the_other) {

	bitmap d_to_be_replaced;
	bitmap d_to_replace_the_other;
	int min, max, n_vals;
	int i;

	if (FZN_VERBOSE)
		printf("Intersecting the domain of variables %s and %s\n", fzn_vars[v_id_to_be_replaced].name, fzn_vars[v_id_to_replace_the_other].name);

	if (fzn_vars[v_id_to_be_replaced].range) {
		b_new_range(&d_to_be_replaced, (unsigned int) fzn_vars[v_id_to_be_replaced].min, (unsigned int) fzn_vars[v_id_to_be_replaced].max);

	} else {
		b_new_vals(&d_to_be_replaced, (unsigned int*) fzn_vars[v_id_to_be_replaced].values, (unsigned int) fzn_vars[v_id_to_be_replaced].max_values);
	}

	if (fzn_vars[v_id_to_replace_the_other].range) {
		b_new_range(&d_to_replace_the_other, (unsigned int) fzn_vars[v_id_to_replace_the_other].min, (unsigned int) fzn_vars[v_id_to_replace_the_other].max);

	} else {
		b_new_vals(&d_to_replace_the_other, (unsigned int*) fzn_vars[v_id_to_replace_the_other].values,
				(unsigned int) fzn_vars[v_id_to_replace_the_other].max_values);
	}

	b_intersect_b(&d_to_be_replaced, &d_to_replace_the_other);
	n_vals = (int) b_cnt_vals(&d_to_be_replaced);
	min = b_get_min_val(&d_to_be_replaced);
	max = b_get_max_val(&d_to_be_replaced);

	if (max - min + 1 == n_vals) {
		if (!fzn_vars[v_id_to_be_replaced].range) {
			free(fzn_vars[v_id_to_be_replaced].values);
			fzn_vars[v_id_to_be_replaced].max_values = 0;
		}
		fzn_vars[v_id_to_be_replaced].range = true;

		if (!fzn_vars[v_id_to_replace_the_other].range) {
			free(fzn_vars[v_id_to_replace_the_other].values);
			fzn_vars[v_id_to_replace_the_other].max_values = 0;
		}
		fzn_vars[v_id_to_replace_the_other].range = true;

	} else {
		if (!fzn_vars[v_id_to_be_replaced].range) {
			free(fzn_vars[v_id_to_be_replaced].values);
		}
		fzn_vars[v_id_to_be_replaced].range = false;

		if (!fzn_vars[v_id_to_replace_the_other].range) {
			free(fzn_vars[v_id_to_replace_the_other].values);
		}
		fzn_vars[v_id_to_replace_the_other].range = false;

		fzn_vars[v_id_to_be_replaced].max_values = n_vals;
		fzn_vars[v_id_to_be_replaced].values = malloc((unsigned int) n_vals * sizeof(unsigned int));
		for (i = 0; i < n_vals; i++) {
			fzn_vars[v_id_to_be_replaced].values[i] = b_get_nth_val(&d_to_be_replaced, (unsigned int) i + 1);
		}

		fzn_vars[v_id_to_replace_the_other].max_values = n_vals;
		fzn_vars[v_id_to_replace_the_other].values = malloc((unsigned int) n_vals * sizeof(unsigned int));
		for (i = 0; i < n_vals; i++) {
			fzn_vars[v_id_to_replace_the_other].values[i] = fzn_vars[v_id_to_be_replaced].values[i];
		}
	}

	fzn_vars[v_id_to_be_replaced].min = min;
	fzn_vars[v_id_to_be_replaced].max = max;
	fzn_vars[v_id_to_replace_the_other].min = min;
	fzn_vars[v_id_to_replace_the_other].max = max;
}

/*

 * Set an array of variables or a variable to label

 * name - name of the array or of the variable

 */

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;

					if (fzn_vars[fzn_vars[fzn_arrays[i].values[j]].replace_by_v_id].min != fzn_vars[fzn_vars[fzn_arrays[i].values[j]].replace_by_v_id].max) {
						vs_to_label_set = true;
					}

#if FZN_SEQ
					fzn_vars[fzn_vars[fzn_arrays[i].values[j]].replace_by_v_id].label_h = LABEL_MODE;
					fzn_vars[fzn_vars[fzn_arrays[i].values[j]].replace_by_v_id].assign_h = ASSIGN_MODE;
#endif

				} 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;

					if (fzn_vars[fzn_arrays[i].values[j]].min != fzn_vars[fzn_arrays[i].values[j]].max) {
						vs_to_label_set = true;
					}

#if FZN_SEQ
					fzn_vars[fzn_arrays[i].values[j]].label_h = LABEL_MODE;
					fzn_vars[fzn_arrays[i].values[j]].assign_h = ASSIGN_MODE;
#endif

				}
			}
			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;

				if (fzn_vars[fzn_vars[i].replace_by_v_id].min != fzn_vars[fzn_vars[i].replace_by_v_id].max) {
					vs_to_label_set = true;
				}

#if FZN_SEQ
				fzn_vars[fzn_vars[i].replace_by_v_id].label_h = LABEL_MODE;
				fzn_vars[fzn_vars[i].replace_by_v_id].assign_h = ASSIGN_MODE;
#endif

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

				fzn_vars[i].to_label = true;

				if (fzn_vars[i].min != fzn_vars[i].max) {
					vs_to_label_set = true;
				}

#if FZN_SEQ
				fzn_vars[i].label_h = LABEL_MODE;
				fzn_vars[i].assign_h = ASSIGN_MODE;
#endif

			}

			return;
		}
	}

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

#if defined(WIN32) || defined(_WIN32) || defined(__WIN32) && !defined(__CYGWIN__)
	printf("\nPress any key to exit\n");
	int a = getchar();
#endif

	exit(0);

}

/*
 * 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) {
				printf("\nPHACT 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");

#if defined(WIN32) || defined(_WIN32) || defined(__WIN32) && !defined(__CYGWIN__)
				printf("\nPress any key to exit\n");
				int a = getchar();
#endif

				exit(0);
			}

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

#if FZN_SEQ
			VS[v_id].label_h = fzn_vars[var_idx].label_h;
			VS[v_id].assign_h = fzn_vars[var_idx].assign_h;
#endif

			// alternated values
		} else {
			v_id = v_new_vals((unsigned int*) fzn_vars[var_idx].values, (unsigned int) fzn_vars[var_idx].next_position, fzn_vars[var_idx].to_label);

#if FZN_SEQ
			VS[v_id].label_h = fzn_vars[var_idx].label_h;
			VS[v_id].assign_h = fzn_vars[var_idx].assign_h;
#endif
		}
		fzn_vars[var_idx].id = (int) 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] = (unsigned int) 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, "\nError: The %d variable of the constraint \"%s\" (%d) is a replacement variable marked as ignored.\n", i,

							fzn_constrs[constr_idx].name, constr_idx);

#if defined(WIN32) || defined(_WIN32) || defined(__WIN32) && !defined(__CYGWIN__)
					printf("\nPress any key to exit\n");
					int a = getchar();
#endif

					exit(0);

				}

				fzn_constrs[constr_idx].vars_id[i] = (unsigned int) 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, "\nError: 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);

#if defined(WIN32) || defined(_WIN32) || defined(__WIN32) && !defined(__CYGWIN__)
				printf("\nPress any key to exit\n");
				int a = getchar();
#endif

				exit(0);

			}

		}

#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 = (int) c_int_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_ne") == 0 && fzn_constrs[constr_idx].next_const_to_add == 0) {

				if (FZN_VERBOSE)
					printf("Adding new CSP (%d) int_ne (c_int_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 = (int) c_int_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 (strcmp(fzn_constrs[constr_idx].name, "int_le") == 0) {

				if (FZN_VERBOSE)

					printf("Adding new CSP (%d) int_le (c_int_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 = (int) c_int_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, "bool_le") == 0) {

				if (FZN_VERBOSE)

					printf("Adding new CSP (%d) bool_le (c_bool_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 = (int) c_bool_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, "bool_lt") == 0) {

				if (FZN_VERBOSE)
					printf("Adding new CSP (%d) bool_lt (c_bool_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 = (int) c_bool_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, "bool_not") == 0) {

				if (FZN_VERBOSE)
					printf("Adding new CSP (%d) bool_not (c_bool_not) 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 = (int) c_bool_not(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 = (int) c_int_le_reif(fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].vars_id[1],
						(int) 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_le_reif") == 0) {

				if (FZN_VERBOSE)
					printf("Adding new CSP (%d) bool_le_reif (c_bool_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 = (int) c_bool_le_reif(fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].vars_id[1],
						(int) 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_lt_reif") == 0) {

				if (FZN_VERBOSE)
					printf("Adding new CSP (%d) bool_lt_reif (c_bool_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 = (int) c_bool_lt_reif(fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].vars_id[1],
						(int) 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_not_reif") == 0) {

				if (FZN_VERBOSE)
					printf("Adding new CSP (%d) bool_not_reif (c_bool_not_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 = (int) c_bool_not_reif(fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].vars_id[1],
						(int) 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 = (int) c_int_lt_reif(fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].vars_id[1],
						(int) 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 = (int) c_int_ne_reif(fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].vars_id[1],
						(int) 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_int_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 = (int) c_int_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_min") == 0) {

				if (FZN_VERBOSE)

					printf("Adding new CSP (%d) constraint int_min (c_int_min) 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 = (int) c_int_min(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_int_lin_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 = (int) c_int_lin_ne(fzn_constrs[constr_idx].consts, (unsigned int*) fzn_constrs[constr_idx].vars_id,
								(unsigned int) 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 int_lin_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 = (int) c_int_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 = (int) 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 = (int) 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_int_lin_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 = (int) c_int_lin_ne(fzn_constrs[constr_idx].consts, (unsigned int*) fzn_constrs[constr_idx].vars_id,
								(unsigned int) 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);

					}

					// int_lin_ne

				} else {

					if (FZN_VERBOSE)

						printf("Adding new CSP (%d) int_lin_ne (c_int_lin_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 = (int) c_int_lin_ne(fzn_constrs[constr_idx].consts, (unsigned int*) fzn_constrs[constr_idx].vars_id,
							(unsigned int) 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 = (int) c_int_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 = (int) c_int_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 {

					bool all_bool = true;
					for (i = 0; i < fzn_constrs[constr_idx].next_var_to_add; i++) {

						if (VS[fzn_constrs[constr_idx].vars_id[i]].max > 1) {
							all_bool = false;
							break;
						}
					}

					if (all_bool) {

						if (FZN_VERBOSE)
							printf("Adding new CSP (%d) int_lin_le (c_bool_lin_le) 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 = (int) c_bool_lin_le(fzn_constrs[constr_idx].consts, (unsigned int*) fzn_constrs[constr_idx].vars_id,
								(unsigned int) fzn_constrs[constr_idx].next_var_to_add,

								fzn_constrs[constr_idx].consts[fzn_constrs[constr_idx].next_var_to_add]);

					} else {

						if (FZN_VERBOSE)
							printf("Adding new CSP (%d) int_lin_le (c_int_lin_le) 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 = (int) c_int_lin_le(fzn_constrs[constr_idx].consts, (unsigned int*) fzn_constrs[constr_idx].vars_id,
								(unsigned int) 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, "bool_lin_le") == 0) {

				if (FZN_VERBOSE)
					printf("Adding new CSP (%d) bool_lin_le (c_bool_lin_le) 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 = (int) c_bool_lin_le(fzn_constrs[constr_idx].consts, (unsigned int*) fzn_constrs[constr_idx].vars_id,
						(unsigned int) 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, "bool_lin_eq") == 0) {

				if (FZN_VERBOSE)
					printf("Adding new CSP (%d) bool_lin_eq (c_bool_lin_eq) with constants %d..., variables %d... and result in 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].id = (int) c_bool_lin_eq(fzn_constrs[constr_idx].consts, (unsigned int*) fzn_constrs[constr_idx].vars_id,
						(unsigned int) 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_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 = (int) c_int_lt_reif(fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].vars_id[1],
							(int) fzn_constrs[constr_idx].vars_id[2]);

					if (FZN_VERBOSE)

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

				} else {

					bool all_bool = true;

					for (i = 0; i < fzn_constrs[constr_idx].next_var_to_add; i++) {
						if (VS[fzn_constrs[constr_idx].vars_id[i]].max > 1) {
							all_bool = false;
							break;
						}
					}

					if (all_bool) {

						if (FZN_VERBOSE)
							printf(
									"Adding new CSP (%d) int_lin_le_reif (c_bool_lin_le_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 = (int) c_bool_lin_le_reif(fzn_constrs[constr_idx].consts, (unsigned int*) fzn_constrs[constr_idx].vars_id,
								(unsigned int) fzn_constrs[constr_idx].next_var_to_add - 1,
								fzn_constrs[constr_idx].consts[fzn_constrs[constr_idx].next_var_to_add - 1],
								(int) fzn_constrs[constr_idx].vars_id[fzn_constrs[constr_idx].next_var_to_add - 1]);
					} else {

						if (FZN_VERBOSE)
							printf(
									"Adding new CSP (%d) int_lin_le_reif (c_int_lin_le_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 = (int) c_int_lin_le_reif(fzn_constrs[constr_idx].consts, (unsigned int*) fzn_constrs[constr_idx].vars_id,
								(unsigned int) fzn_constrs[constr_idx].next_var_to_add - 1,
								fzn_constrs[constr_idx].consts[fzn_constrs[constr_idx].next_var_to_add - 1],
								(int) 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((unsigned int) 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 = (int) c_sum((unsigned int*) vars_idx, (unsigned int) fzn_constrs[constr_idx].next_var_to_add,
							(unsigned int) 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 = (int) c_sum_var((unsigned int*) vars_idx, (unsigned int) 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 = (int) c_sum_var((unsigned int*) vars_idx, (unsigned int) 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 = (int) 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 = (int) 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 = (int) 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_int_lin_eq) 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 = (int) c_int_lin_eq(fzn_constrs[constr_idx].consts, fzn_constrs[constr_idx].vars_id,
							(unsigned int) 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_int_lin_eq) 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 = (int) c_int_lin_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 if (fzn_constrs[constr_idx].next_var_to_add == 2 && fzn_constrs[constr_idx].next_const_to_add == 3) {

					if (FZN_VERBOSE)
						printf("Adding new CSP (%d) int_lin_eq (c_int_lin_eq) 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[2]);

					fzn_constrs[constr_idx].id = (int) c_int_lin_eq(fzn_constrs[constr_idx].consts, fzn_constrs[constr_idx].vars_id,
							(unsigned int) 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 {

					fprintf(stderr, "\nError: Type of constraint \"%s\" (%d) not recognized.\n", fzn_constrs[constr_idx].name, constr_idx);

#if defined(WIN32) || defined(_WIN32) || defined(__WIN32) && !defined(__CYGWIN__)
					printf("\nPress any key to exit\n");
					int a = getchar();
#endif

					exit(0);

				}

				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 = (int) c_int_eq_c_reif(fzn_constrs[constr_idx].vars_id[0], (unsigned int) fzn_constrs[constr_idx].consts[0],
						(int) 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_int_eq_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 = (int) c_int_eq_reif(fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].vars_id[1],
						(int) 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_bool_eq_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 = (int) c_bool_eq_reif(fzn_constrs[constr_idx].vars_id[0], fzn_constrs[constr_idx].vars_id[1],
						(int) 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)