/*
 * main.c
 *
 *  Created on: 03/01/2015
 *      Author: Pedro
 */

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

#include "domains.h"
#include "variables.h"
#include "devices.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 "config.h"
#include "kernels/cl_constraints.h"
#include "constraints.h"
#include "csps/CSP.h"
#include "csps/all_diff.h"
#include "csps/all_interval.h"
#include "csps/costas.h"
#include "csps/golomb.h"
#include "csps/langford.h"
#include "csps/latin_squares.h"
#include "csps/market_split.h"
#include "csps/queens.h"
#include "csps/qap.h"
#include "csps/sudoku.h"
#include "csps/schurs.h"
#include "csps/steiner.h"
#include "utils/benchmark.h"

#if COMPILE_FZN
#include "utils/flatzinc/parser.tab.h"
#endif

#define MAX_COMMAND_SIZE 500

int main(int argc, char *argv[]) {
	struct timeval start, end;	// for elapse time calculation
	char start_time[40];		// for elapse time calculation
	char end_time[40];			// for elapse time calculation
	char elapsed_time[40];		// for elapse time calculation
	int csp_dims[MAX_CSP_DIM_ARGS];	// argument indicating the dimensions of the CSP to solve
	char *csp_inst_name = malloc(20 * sizeof(char));	// argument indicating the CSP instance to solve
	strcpy(csp_inst_name, "No name given");
	unsigned int i;

	gettimeofday(&start, NULL);
	init_sec = start.tv_sec;
	init_usec = start.tv_usec;

	// parse arguments
	parse_args(&argc, argv, csp_dims, csp_inst_name);

	// CSP variables and constraints
	VS = (var*) malloc(N_VS * sizeof(var));
	CS = (constr*) malloc(N_CS * sizeof(constr));
	CONST_VS_ID = (int*) malloc(H_BITS * sizeof(int));
	memset(CONST_VS_ID, -1, sizeof(unsigned int) * H_BITS);

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

	if (PRINT_STATS) {
		STATS.nodes_fail = 0;
		STATS.nodes_expl = 0;
		STATS.backtracks = 0;
		STATS.labels = 0;
		STATS.pruning = 0;
		STATS.props_ok = 0;
		STATS.max_depth = 0;
		STATS.solve_time = 0;
		STATS.n_solutions = 0;
		STATS.search_spaces = 0;
	}

	// if an example must be executed
	if (CSP != NULL) {

		if (WORK == DEFAULT_W) {
			WORK = WORK_D;
		}

		if (WORK == ONE) {
			FINDING_ONE_SOLUTION = true;
		} else if (WORK == CNT) {
			COUNTING_SOLUTIONS = true;
		} else {
			OPTIMIZING = true;
			VS_LOCK = malloc(N_VS * sizeof(var));
			VS_LOCK_BEST = malloc(N_VS * sizeof(var));
		}

		// Select and solve the CSP example
		if (!strcmp(CSP, "QUEENS")) {
			run_n_queens(csp_dims);
		} else if (!strcmp(CSP, "COSTAS")) {
			run_costas(csp_dims);
		} else if (!strcmp(CSP, "GOLOMB")) {
			run_golomb(csp_dims);
		} else if (!strcmp(CSP, "SUDOKU")) {
			run_sudoku(csp_dims);
		} else if (!strcmp(CSP, "QAP")) {
			if (csp_inst_name != NULL) {
				run_qap(csp_inst_name);
			} else {
				printf("\nPlease select a QAP instance from \"csps/qap.c\" file.\n");
			}
		} else if (!strcmp(CSP, "ALL-DIFF")) {
			run_all_diff(csp_dims);
		} else if (!strcmp(CSP, "LANGFORD")) {
			run_langford(csp_dims);
		} else if (!strcmp(CSP, "STEINER")) {
			run_steiner(csp_dims);
		} else if (!strcmp(CSP, "LATIN")) {
			run_latin_squares(csp_dims);
		} else if (!strcmp(CSP, "ALL-INTERVAL")) {
			run_all_interval(csp_dims);
		} else if (!strcmp(CSP, "MARKET-SPLIT")) {
			if (csp_inst_name != NULL) {
				run_market_split(csp_inst_name);
			} else {
				printf("\nPlease select a Market split instance from \"csps/market_split.c\" file.\n");
			}
		} else if (!strcmp(CSP, "SCHURS")) {
			run_schurs(csp_dims);
		} else {
			printf("\nThe requested CSP (%s) example is not implemented.\n", CSP);
			print_help();

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

			exit(0);
		}

	}
#if COMPILE_FZN
	// Solve a Minizinc model after converting it to Flatzinc
	// MZN and DZN files
	else if (MZN_FILE_NAME != NULL && DZN_FILE_NAME != NULL) {
		int len = (int) strlen(MZN_FILE_NAME);
		const char *last_four_mzn = &MZN_FILE_NAME[len - 4];
		len = (int) strlen(DZN_FILE_NAME);
		const char *last_four_dzn = &DZN_FILE_NAME[len - 4];

		if (strcmp(last_four_mzn, ".mzn") == 0 && strcmp(last_four_dzn, ".dzn") == 0) {
			char command[MAX_COMMAND_SIZE];

			FZN_FILE_NAME = malloc((strlen(DZN_FILE_NAME) + 1) * sizeof(char));
			strcpy(FZN_FILE_NAME, DZN_FILE_NAME);
			FZN_FILE_NAME[len - 3] = 'f';

			if (strchr(FZN_FILE_NAME, '/') == NULL) {
				snprintf(command, MAX_COMMAND_SIZE, "mzn2fzn --no-output-ozn -o src/csps/%s src/csps/%s src/csps/%s", FZN_FILE_NAME, MZN_FILE_NAME,
						DZN_FILE_NAME);
			} else {
				snprintf(command, MAX_COMMAND_SIZE, "mzn2fzn --no-output-ozn -o %s %s %s", FZN_FILE_NAME, MZN_FILE_NAME, DZN_FILE_NAME);
			}

			// check if mzn2fzn is available
			if (!can_run_command("mzn2fzn")) {
				printf("\nThe program mzn2fzn is not available.\n");

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

				exit(0);
			}

			if (system(command) != 0) {

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

				exit(0);
			}

			// copy fzn file to the Debug or src folder, depending if run from Debug or from Eclipse
			char command_cp[MAX_COMMAND_SIZE];
			snprintf(command_cp, MAX_COMMAND_SIZE, "cp -rf src/csps/%s Debug/src/csps/ > /dev/null 2>&1", FZN_FILE_NAME);
			if (system(command_cp) != 0) {
				snprintf(command_cp, MAX_COMMAND_SIZE, "cp -rf src/csps/%s ../src/csps/ > /dev/null 2>&1", FZN_FILE_NAME);
				if (system(command_cp) != 0) {
				}
			}

			if (MZN2FZN_ONLY) {
				printf("\n%s %s successfully converted to %s.\nNow exiting.\n\n", MZN_FILE_NAME, DZN_FILE_NAME, FZN_FILE_NAME);

				free(MZN_FILE_NAME);
				free(DZN_FILE_NAME);

				return 0;
			}

			if (strchr(FZN_FILE_NAME, '/') == NULL) {
				snprintf(command, MAX_COMMAND_SIZE, "src/csps/%s", FZN_FILE_NAME);

			} else {
				snprintf(command, MAX_COMMAND_SIZE, "%s", FZN_FILE_NAME);
			}

			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 converted from MiniZinc to FlatZinc\n", start_time, end_time, elapsed_time);

				gettimeofday(&start, NULL);
			}

			run_fzn_model(command);

			free(MZN_FILE_NAME);
			free(DZN_FILE_NAME);

		} else {
			printf("\nFiles \"%s\" and \"%s\" are not a Minizinc model.\n", MZN_FILE_NAME, DZN_FILE_NAME);

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

			exit(0);
		}

		// only MZN file
	} else if (MZN_FILE_NAME != NULL && DZN_FILE_NAME == NULL) {

		int len = (int) strlen(MZN_FILE_NAME);
		const char *last_four_mzn = &MZN_FILE_NAME[len - 4];

		if (strcmp(last_four_mzn, ".mzn") == 0) {
			char command[MAX_COMMAND_SIZE];

			FZN_FILE_NAME = malloc((strlen(MZN_FILE_NAME) + 1) * sizeof(char));
			strcpy(FZN_FILE_NAME, MZN_FILE_NAME);
			FZN_FILE_NAME[len - 3] = 'f';

			if (strchr(FZN_FILE_NAME, '/') == NULL) {
				snprintf(command, MAX_COMMAND_SIZE, "mzn2fzn --no-output-ozn -o src/csps/%s src/csps/%s", FZN_FILE_NAME, MZN_FILE_NAME);
			} else {
				snprintf(command, MAX_COMMAND_SIZE, "mzn2fzn --no-output-ozn -o %s %s", FZN_FILE_NAME, MZN_FILE_NAME);
			}

			// check if mzn2fzn is available
			if (!can_run_command("mzn2fzn")) {
				printf("\nThe program mzn2fzn is not available.\n");

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

				exit(0);
			}

			if (system(command) != 0) {

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

				exit(0);
			}

			// copy fzn file to the Debug or src folder, depending if run from Debug or from Eclipse
			char command_cp[MAX_COMMAND_SIZE];
			snprintf(command_cp, MAX_COMMAND_SIZE, "cp -rf src/csps/%s Debug/src/csps/ > /dev/null 2>&1", FZN_FILE_NAME);
			if (system(command_cp) != 0) {
				snprintf(command_cp, MAX_COMMAND_SIZE, "cp -rf src/csps/%s ../src/csps/ > /dev/null 2>&1", FZN_FILE_NAME);
			}

			if (MZN2FZN_ONLY) {
				printf("\n%s successfully converted to %s.\nNow exiting.\n\n", MZN_FILE_NAME, FZN_FILE_NAME);

				free(MZN_FILE_NAME);

				return 0;
			}

			if (strchr(FZN_FILE_NAME, '/') == NULL) {
				snprintf(command, MAX_COMMAND_SIZE, "src/csps/%s", FZN_FILE_NAME);

			} else {
				snprintf(command, MAX_COMMAND_SIZE, "%s", FZN_FILE_NAME);
			}

			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 converted from MiniZinc to FlatZinc\n", start_time, end_time, elapsed_time);

				gettimeofday(&start, NULL);
			}

			run_fzn_model(command);

			free(MZN_FILE_NAME);

		} else {
			printf("\nFile \"%s\" is not a Minizinc model.\n", MZN_FILE_NAME);

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

			exit(0);
		}

		// Solve a Flatzinc model
		// FZN file
	} else if (FZN_FILE_NAME != NULL) {
		int len = (int) strlen(FZN_FILE_NAME);
		const char *last_four = &FZN_FILE_NAME[len - 4];

		if (strcmp(last_four, ".fzn") == 0) {
			char command[MAX_COMMAND_SIZE];

			if (strchr(FZN_FILE_NAME, '/') == NULL) {
				snprintf(command, MAX_COMMAND_SIZE, "src/csps/%s", FZN_FILE_NAME);

			} else {
				snprintf(command, MAX_COMMAND_SIZE, "%s", FZN_FILE_NAME);
			}

			run_fzn_model(command);
			free(FZN_FILE_NAME);
		} else {
			printf("\nThe file \"%s\" is not a Flatzinc model.\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);
		}
	}
#endif
	// Solve a CSP modeled in src/csps/CSP.c
	else {

#if !COMPILE_FZN
		if (MZN_FILE_NAME != NULL || DZN_FILE_NAME != NULL || FZN_FILE_NAME != NULL) {
			printf("The compilation of the FlatZinc interpreter is disabled.\n"
					"Please enable it in \"config.h\" file, by setting \"COMPILE_FZN 1\" to load FlatZinc/MiniZinc models.\n");

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

			exit(0);
		}
#endif

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

		// load CSP and solve it
		load_and_solve_CSP(csp_dims);
	}

	// Print elapsed time
	gettimeofday(&end, NULL);
	format_time_s_ms(start_time, start.tv_sec, start.tv_usec);
	format_time_s_ms(end_time, end.tv_sec, end.tv_usec);
	format_elapsed_time_s_ms(elapsed_time, start.tv_sec, start.tv_usec, end.tv_sec, end.tv_usec);

	if (!PRINT_STATS) {
		if (!QUIET) {
			printf("\nTotal elapsed time: %s (s.ms)\n\n", elapsed_time);
		}

	} else {

		int n_constraint_types = 0;

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

			if (USE_CS_REIFI[i]) {
				n_constraint_types++;

			}
			if (USE_NON_CS_REIFI[i]) {
				n_constraint_types++;
			}
		}

		unsigned int n_boolean_vs = 0;
		for (i = 0; i < N_VS; i++) {
			if (VS[i].boolean) {
				n_boolean_vs++;
			}
		}
		unsigned int n_boolean_cs = 0;
		for (i = 0; i < N_CS; i++) {
			if (CS[i].boolean) {
				n_boolean_cs++;
			}
		}

		unsigned int n_total_threads = 0;
		for (i = 0; i < N_DEVS; i++) {
			n_total_threads += (unsigned int) (DEVICES_INFO[i].n_wg * DEVICES_INFO[i].n_wi_wg);
		}

		printf("\nStatistics:\n");
		printf(" - Threads:       	%u\n", n_total_threads);

		if (N_DEVS > 1) {
			for (i = 0; i < N_DEVS; i++) {
				if (DEVICES_INFO[i].type == CL_DEVICE_TYPE_CPU) {
					printf("   - CPU (%d):           %lu\n", DEVICES_INFO[i].dev_type_n, DEVICES_INFO[i].n_wg * DEVICES_INFO[i].n_wi_wg);

				} else if (DEVICES_INFO[i].type == CL_DEVICE_TYPE_GPU) {
					printf("   - GPU (%d):           %lu\n", DEVICES_INFO[i].dev_type_n, DEVICES_INFO[i].n_wg * DEVICES_INFO[i].n_wi_wg);

				} else if (DEVICES_INFO[i].type == CL_DEVICE_TYPE_ACCELERATOR) {
					printf("   - ACC (%d):           %lu\n", DEVICES_INFO[i].dev_type_n, DEVICES_INFO[i].n_wg * DEVICES_INFO[i].n_wi_wg);

				}
			}
		}

		printf(" - Total time:       	%s s\n", elapsed_time);
		printf(" - Solve time:       	%.03f s\n", (double) STATS.solve_time / 1000.0);
		printf(" - Solutions:        	%lu\n", STATS.n_solutions);
		printf(" - Search spaces:       %lu\n", STATS.search_spaces);
		printf(" - Variables:        	%u (%u)\n", N_VS, N_VS_ORIGINAL);
		printf("   - Boolean:           %u\n", n_boolean_vs);
		printf("   - To label:	        %u\n", N_VS_TO_LABEL);
		printf(" - Domains range:    	[%u,%u]\n", D_MIN, D_MAX);
		printf(" - Constraints:      	%u (%u)\n", N_CS, N_CS_ORIGINAL);
		printf("   - Boolean:           %u\n", n_boolean_cs);
		printf(" - Constraint types: 	%u:\n", n_constraint_types);
		cs_print_used();
		printf(" - Maximum depth:    	%lu\n", STATS.max_depth);
		printf(" - Labels:           	%lu\n", STATS.labels + STATS.search_spaces);
		printf(" - Nodes explored:   	%lu\n", STATS.labels + STATS.search_spaces - STATS.nodes_fail);
		printf(" - Nodes failed:     	%lu\n", STATS.nodes_fail);
		printf(" - Backtracks:       	%lu\n", STATS.backtracks);
		printf(" - Prunings (approx.):  %lu\n", STATS.pruning);
		printf(" - Propagations:     	%lu\n", STATS.props_ok);
	}

	// Clear memory
	clear_csp();
	free(csp_inst_name);

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

	return 0;
}