/*
 * constraints.c
 *
 *  Created on: 25/08/2014
 *      Author: Pedro
 */

#include "constraints.h"

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

#include "config.h"
#include "variables.h"
#include "bitmaps.h"

/*
 * Creates a new generic constraint that constrains the received variables
 * vs_id - array with the IDs of the variables that are constrained by this constraint
 * n_vs - number of ID variables in vs_id
 * consts - constrained constants (if more than one)
 * n_consts - number of constant values constrained by this constraint in consts vector (if more than one)
 * reif_v_id - -1 if not reified, or the ID of the reification variable if reified
 */
unsigned int c_new(unsigned int *vs_id, unsigned int n_vs, int *consts, unsigned int n_consts, int reif_v_id) {
	unsigned int i, j;

	// if more constraints are needed, allocate a new vector and updates the variables pointers
	if (C_ID_CNTR == N_CS) {
		CS_AUX = (constr*) malloc(N_CS * 2 * (sizeof(constr)));

		cs_copy(CS_AUX, CS, N_CS);

		for (i = 0; i < V_ID_CNTR; i++) {
			for (j = 0; j < VS[i].n_cs; j++) {
				VS[i].cs[j] = &CS_AUX[VS[i].cs[j]->c_id];
			}
		}

		free(CS);
		CS = CS_AUX;

		N_CS *= 2;
	}

	CS[C_ID_CNTR].c_id = C_ID_CNTR;
	CS[C_ID_CNTR].n_c_vs = (unsigned short) n_vs;
	CS[C_ID_CNTR].n_c_consts = (unsigned short) n_consts;
	CS[C_ID_CNTR].ignore = false;

	if (reif_v_id == -1) {
		CS[C_ID_CNTR].reif_v_id = 0;
		CS[C_ID_CNTR].reified = false;
	} else {
		CS[C_ID_CNTR].reif_v_id = (unsigned int) reif_v_id;
		CS[C_ID_CNTR].reified = true;

		v_add_constr(&VS[reif_v_id], &CS[C_ID_CNTR]);
		VS[reif_v_id].reif = true;
	}

	if (n_consts > 0) {
		CS[C_ID_CNTR].c_consts = (int*) malloc(n_consts * sizeof(int));

		for (i = 0; i < n_consts; i++) {
			CS[C_ID_CNTR].c_consts[i] = consts[i];
		}
	} else {
		CS[C_ID_CNTR].c_consts = NULL;
	}

	CS[C_ID_CNTR].c_vs = (var**) malloc(n_vs * sizeof(var*));

	for (i = 0; i < n_vs; i++) {
		CS[C_ID_CNTR].c_vs[i] = &VS[vs_id[i]];

	}

	CS[C_ID_CNTR].boolean = true;
	for (i = 0; i < n_vs; i++) {
		v_add_constr(&VS[vs_id[i]], &CS[C_ID_CNTR]);

		if (!VS[vs_id[i]].boolean) {
			CS[C_ID_CNTR].boolean = false;
		}
	}

	return C_ID_CNTR++;
}

/*
 * copy n_cs constraints from cs_src to cs_dest
 * cs_dest - where to copy the constraints
 * cs_src - where from to copy the constraints
 * n_cs - number of constraints to copy
 */
void cs_copy(constr *cs_dest, constr *cs_src, unsigned int n_cs) {
	unsigned int i;

	for (i = 0; i < n_cs; i++) {
		cs_dest[i].constant_val = cs_src[i].constant_val;
		cs_dest[i].c_consts = cs_src[i].c_consts;
		cs_dest[i].c_id = cs_src[i].c_id;
		cs_dest[i].c_vs = cs_src[i].c_vs;
		cs_dest[i].check_sol_f = cs_src[i].check_sol_f;
		cs_dest[i].kind = cs_src[i].kind;
		cs_dest[i].n_c_consts = cs_src[i].n_c_consts;
		cs_dest[i].n_c_vs = cs_src[i].n_c_vs;
		cs_dest[i].reif_v_id = cs_src[i].reif_v_id;
		cs_dest[i].reified = cs_src[i].reified;
		cs_dest[i].ignore = cs_src[i].ignore;
		cs_dest[i].boolean = cs_src[i].boolean;
	}
}

/*
 * Return the count of values inside all variables of the constraints vector
 * cs - constraints vector to count variables values in all constraints
 * n_cs - number of constraints in the vector
 * */
int cs_cnt_vals(constr *cs, unsigned int n_cs) {
	unsigned int i, j;
	int cnt = 0;

	for (i = 0; i < n_cs; i++) {
		for (j = 0; j < cs[i].n_c_vs; j++) {
			cnt += cs[i].c_vs[j]->n_vals;
		}
	}
	return cnt;
}

/*
 * Return the count of variables inside a constraints vector
 * cs - constraints vector to count variables in
 * n_cs - number of constraints in the vector
 * */
int cs_cnt_vs(constr *cs, unsigned int n_cs) {
	unsigned int i;
	unsigned int cnt = 0;

	for (i = 0; i < n_cs; i++) {
		cnt += cs[i].n_c_vs;
	}
	return (int) cnt;
}

/*
 * Return the count of different variables inside a constraints vector
 * cs - constraints vector to count different variables in
 * n_cs - number of constraints in the vector
 * */
int cs_cnt_diff_vs(constr *cs, unsigned int n_cs) {
	unsigned int i, j;
	unsigned int v_max_id = 0;

	for (i = 0; i < n_cs; i++) {
		for (j = 0; j < cs[i].n_c_vs; j++) {
			if (v_max_id < cs[i].c_vs[j]->v_id) {
				v_max_id = cs[i].c_vs[j]->v_id;
			}
		}
	}
	return (int) v_max_id + 1;
}

/*
 * Return the count of constant values (more than one per constraint) inside a constraints vector
 * cs - constraints vector to count constant values in
 * n_cs - number of constraints in the vector
 * */
int cs_cnt_constants(constr *cs, unsigned int n_cs) {
	unsigned int i;
	unsigned int cnt = 0;

	for (i = 0; i < n_cs; i++) {
		cnt += cs[i].n_c_consts;
	}
	return (int) cnt;
}

/*
 * Remove all constraints marked as ignored after filtering the CSP
 */
void cs_remove_ignored() {
	int ignored_ctr = 0;
	int cs_count = 0;
	unsigned int i, j, k, l;

	for (i = 0; i < C_ID_CNTR; i++) {
		if (CS[i].ignore) {

			ignored_ctr++;

			// remove constraint pointer from variables
			for (j = 0; j < CS[i].n_c_vs; j++) {
				v_rem_constr(CS[i].c_vs[j], &CS[i]);
			}
			if (CS[i].reified) {
				if (VS[CS[i].reif_v_id].v_id == CS[i].reif_v_id) {
					v_rem_constr(&VS[CS[i].reif_v_id], &CS[i]);

				} else {
					for (k = 0; k < N_VS; k++) {
						if (VS[k].v_id == CS[i].reif_v_id) {
							v_rem_constr(&VS[k], &CS[i]);
							break;
						}
					}
				}
			}
		}
	}

	CS_AUX = malloc((C_ID_CNTR - (unsigned long) ignored_ctr) * sizeof(constr));

	for (i = 0; i < C_ID_CNTR; i++) {
		if (!CS[i].ignore) {

			cs_copy(&CS_AUX[cs_count], &CS[i], 1);

			// update constraint pointer from variables
			for (j = 0; j < CS_AUX[cs_count].n_c_vs; j++) {

				for (k = 0; k < CS_AUX[cs_count].c_vs[j]->n_cs; k++) {

					if (CS_AUX[cs_count].c_vs[j]->cs[k]->c_id == CS_AUX[cs_count].c_id) {
						CS_AUX[cs_count].c_vs[j]->cs[k] = &CS_AUX[cs_count];
					}
				}

				if (CS_AUX[cs_count].reified) {

					if (VS[CS_AUX[cs_count].reif_v_id].v_id == CS_AUX[cs_count].reif_v_id) {

						for (l = 0; l < VS[CS_AUX[cs_count].reif_v_id].n_cs; l++) {

							if (VS[CS_AUX[cs_count].reif_v_id].cs[l]->c_id == CS_AUX[cs_count].c_id) {
								VS[CS_AUX[cs_count].reif_v_id].cs[l] = &CS_AUX[cs_count];
								break;
							}
						}
					} else {
						for (k = 0; k < N_VS; k++) {

							if (VS[k].v_id == CS_AUX[cs_count].reif_v_id) {

								for (l = 0; l < VS[k].n_cs; l++) {

									if (VS[k].cs[l]->c_id == CS_AUX[cs_count].c_id) {
										VS[k].cs[l] = &CS_AUX[cs_count];
										break;
									}
								}
								break;
							}
						}
					}
				}
			}

			CS_AUX[cs_count].c_id = (unsigned int) cs_count;
			cs_count++;

		} else {
			free(CS[i].c_consts);
			free(CS[i].c_vs);
		}
	}

	N_CS = (unsigned int) cs_count;
	C_ID_CNTR = (unsigned int) cs_count;

	free(CS);
	CS = CS_AUX;
}

/*
 * Return true if all constraints are met (solution found) and false otherwise
 * explored - if not in prefiltering phase
 */
bool cs_check(bool explored) {
	unsigned int i;
	bool result = true;

	for (i = 0; i < N_CS && result; i++) {
		if (result) {
			result = CS[i].check_sol_f(&CS[i], explored);

		} else if (!explored) {
			result = false;
		}
	}

	return result;
}

/*
 * Clear constraints memory
 */
void cs_clear() {
	unsigned int i;

	for (i = 0; i < N_CS; i++) {
		free(CS[i].c_vs);

		if (CS[i].n_c_consts > 0) {
			free(CS[i].c_consts);
		}
	}
}

/*
 * print all the variables ID that are constrained by all the CSP constraints, per contraint order
 */
void cs_print_all_vs_id() {
	unsigned int i;
	int j;

	printf("\n");
	for (i = 0; i < C_ID_CNTR; i++) {
		printf("Constraint (%d) %u -> ", CS[i].kind, i);
		for (j = 0; j < CS[i].n_c_vs - 1; j++) {
			printf("%u,", CS[i].c_vs[j]->v_id);
		}
		printf("%u\n", CS[i].c_vs[j]->v_id);
	}
}

/*
 * Print the name of the constraint
 * cs -constraint to print the name
 */
void cs_print_type(constr *cs) {
	switch (cs->kind) {
	case ALL_DIFFERENT:
		printf("ALL_DIFFERENT");
		break;
	case ARRAY_BOOL_AND:
		printf("ARRAY_BOOL_AND");
		break;
	case ARRAY_BOOL_ELEMENT:
		printf("ARRAY_BOOL_ELEMENT");
		break;
	case ARRAY_BOOL_OR:
		printf("ARRAY_BOOL_OR");
		break;
	case ARRAY_BOOL_XOR:
		printf("ARRAY_BOOL_XOR");
		break;
	case ARRAY_INT_ELEMENT:
		printf("ARRAY_INT_ELEMENT");
		break;
	case ARRAY_VAR_INT_ELEMENT:
		printf("ARRAY_VAR_INT_ELEMENT");
		break;
	case AT_LEAST:
		printf("AT_LEAST");
		break;
	case AT_MOST:
		printf("AT_MOST");
		break;
	case AT_MOST_ONE:
		printf("AT_MOST_ONE");
		break;
	case BOOL_AND:
		printf("BOOL_AND");
		break;
	case BOOL_CLAUSE:
		printf("BOOL_CLAUSE");
		break;
	case BOOL_EQ:
		printf("BOOL_EQ");
		break;
	case BOOL_LE:
		printf("BOOL_LE");
		break;
	case BOOL_LIN_EQ:
		printf("BOOL_LIN_EQ");
		break;
	case BOOL_LIN_LE:
		printf("BOOL_LIN_LE");
		break;
	case BOOL_LT:
		printf("BOOL_LT");
		break;
	case BOOL_NOT:
		printf("BOOL_NOT");
		break;
	case BOOL_OR:
		printf("BOOL_OR");
		break;
	case BOOL_XOR:
		printf("BOOL_XOR");
		break;
	case BOOL2INT:
		printf("BOOL2INT");
		break;
	case ELEMENT:
		printf("ELEMENT");
		break;
	case EXACTLY:
		printf("EXACTLY");
		break;
	case EXACTLY_VAR:
		printf("EXACTLY_VAR");
		break;
	case INT_DIV:
		printf("INT_DIV");
		break;
	case INT_EQ:
		printf("INT_EQ");
		break;
	case INT_EQ_C:
		printf("INT_EQ_C");
		break;
	case INT_LE:
		printf("INT_LE");
		break;
	case INT_LIN_EQ:
		printf("INT_LIN_EQ");
		break;
	case INT_LIN_LE:
		printf("INT_LIN_LE");
		break;
	case INT_LIN_NE:
		printf("INT_LIN_NE");
		break;
	case INT_LIN_VAR:
		printf("INT_LIN_VAR");
		break;
	case INT_LT:
		printf("INT_LT");
		break;
	case INT_MAX_:
		printf("INT_MAX_");
		break;
	case INT_MIN_:
		printf("INT_MIN_");
		break;
	case INT_MOD:
		printf("INT_MOD");
		break;
	case INT_NE:
		printf("INT_NE");
		break;
	case INT_PLUS:
		printf("INT_PLUS");
		break;
	case INT_TIMES:
		printf("INT_TIMES");
		break;
	case MAXIMIZE:
		printf("MAXIMIZE");
		break;
	case MINIMIZE:
		printf("MINIMIZE");
		break;
	case MINUS_EQ:
		printf("MINUS_EQ");
		break;
	case MINUS_NE:
		printf("MINUS_NE");
		break;
	case SUM:
		printf("SUM");
		break;
	case SUM_PROD:
		printf("SUM_PROD");
		break;
	case SUM_VAR:
		printf("SUM_VAR");
		break;
	case VAR_EQ_MINUS:
		printf("VAR_EQ_MINUS");
		break;
	case VAR_EQ_MINUS_ABS:
		printf("VAR_EQ_MINUS_ABS");
		break;
	default:
		printf("NOT_RECOGNIZED");
		break;
	}

	if (cs->reified) {
		printf("_REIF");
	}
}

/*
 * Return the name of the constraint
 * kind -kind of the constraint to return the name
 */
char* cs_get_type(c_kind kind) {
	switch (kind) {
	case ALL_DIFFERENT:
		return "ALL_DIFFERENT";
		break;
	case ARRAY_BOOL_AND:
		return "ARRAY_BOOL_AND";
		break;
	case ARRAY_BOOL_ELEMENT:
		return "ARRAY_BOOL_ELEMENT";
		break;
	case ARRAY_BOOL_OR:
		return "ARRAY_BOOL_OR";
		break;
	case ARRAY_BOOL_XOR:
		return "ARRAY_BOOL_XOR";
		break;
	case ARRAY_INT_ELEMENT:
		return "ARRAY_INT_ELEMENT";
		break;
	case ARRAY_VAR_INT_ELEMENT:
		return "ARRAY_VAR_INT_ELEMENT";
		break;
	case AT_LEAST:
		return "AT_LEAST";
		break;
	case AT_MOST:
		return "AT_MOST";
		break;
	case AT_MOST_ONE:
		return "AT_MOST_ONE";
		break;
	case BOOL_AND:
		return "BOOL_AND";
		break;
	case BOOL_CLAUSE:
		return "BOOL_CLAUSE";
		break;
	case BOOL_EQ:
		return "BOOL_EQ";
		break;
	case BOOL_LE:
		return "BOOL_LE";
		break;
	case BOOL_LIN_EQ:
		return "BOOL_LIN_EQ";
		break;
	case BOOL_LIN_LE:
		return "BOOL_LIN_LE";
		break;
	case BOOL_LT:
		return "BOOL_LT";
		break;
	case BOOL_NOT:
		return "BOOL_NOT";
		break;
	case BOOL_OR:
		return "BOOL_OR";
		break;
	case BOOL_XOR:
		return "BOOL_XOR";
		break;
	case BOOL2INT:
		return "BOOL2INT";
		break;
	case ELEMENT:
		return "ELEMENT";
		break;
	case EXACTLY:
		return "EXACTLY";
		break;
	case EXACTLY_VAR:
		return "EXACTLY_VAR";
		break;
	case INT_DIV:
		return "INT_DIV";
		break;
	case INT_EQ:
		return "INT_EQ";
		break;
	case INT_EQ_C:
		return "INT_EQ_C";
		break;
	case INT_LE:
		return "INT_LE";
		break;
	case INT_LIN_EQ:
		return "INT_LIN_EQ";
		break;
	case INT_LIN_LE:
		return "INT_LIN_LE";
		break;
	case INT_LIN_NE:
		return "INT_LIN_NE";
		break;
	case INT_LIN_VAR:
		return "INT_LIN_VAR";
		break;
	case INT_LT:
		return "INT_LT";
		break;
	case INT_MAX_:
		return "INT_MAX_";
		break;
	case INT_MIN_:
		return "INT_MIN_";
		break;
	case INT_MOD:
		return "INT_MOD";
		break;
	case INT_NE:
		return "INT_NE";
		break;
	case INT_PLUS:
		return "INT_PLUS";
		break;
	case INT_TIMES:
		return "INT_TIMES";
		break;
	case MAXIMIZE:
		return "MAXIMIZE";
		break;
	case MINIMIZE:
		return "MINIMIZE";
		break;
	case MINUS_EQ:
		return "MINUS_EQ";
		break;
	case MINUS_NE:
		return "MINUS_NE";
		break;
	case SUM:
		return "SUM";
		break;
	case SUM_PROD:
		return "SUM_PROD";
		break;
	case SUM_VAR:
		return "SUM_VAR";
		break;
	case VAR_EQ_MINUS:
		return "VAR_EQ_MINUS";
		break;
	case VAR_EQ_MINUS_ABS:
		return "VAR_EQ_MINUS_ABS";
		break;
	default:
		return "NOT_RECOGNIZED";
		break;
	}
}

/*
 * print the kind of the constraints that were used
 */
void cs_print_used() {
	int i;

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

		if (USE_CS[i]) {
			printf("   - %s", cs_get_type((c_kind) i));

			if (USE_CS_REIFI[i]) {
				printf("_REIF\n");

				if (USE_NON_CS_REIFI[i]) {
					printf("   - %s\n", cs_get_type((c_kind) i));
				}

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