/*
 * 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++;
}

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
 */
bool cs_check(bool explored) {
	unsigned int i;
	bool result = true;

	for (i = 0; i < N_CS && result; i++) {

		if (result && (!CS[i].reified || (CS[i].reified && VS[CS[i].reif_v_id].n_vals == 1 && VS[CS[i].reif_v_id].min == 1))) {
			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 AT_LEAST:

			printf("AT_LEAST");

			break;

		case AT_MOST:
			printf("AT_MOST");
			break;
		case AT_MOST_ONE:
			printf("AT_MOST_ONE");
			break;
		case ELEMENT:
			printf("ELEMENT");
			break;
		case ELEMENT_INT_VAR:
			printf("ELEMENT_INT_VAR");
			break;
		case ELEMENT_VAR:
			printf("ELEMENT_VAR");
			break;
		case EQ:
			printf("EQ");
			break;
		case EQ_VAR:
			printf("EQ_VAR");
			break;
		case EXACTLY:
			printf("EXACTLY");
			break;
		case EXACTLY_VAR:
			printf("EXACTLY_VAR");
			break;
		case LE:
			printf("LE");
			break;
		case LINEAR:
			printf("LINEAR");
			break;
		case LINEAR_VAR:
			printf("LINEAR_VAR");
			break;
		case LT:
			printf("LT");
			break;
		case MAX:
			printf("MAX");
			break;
		case MAXIMIZE:
			printf("MAXIMIZE");
			break;
		case MIN:
			printf("MIN");
			break;
		case MINIMIZE:
			printf("MINIMIZE");
			break;
		case MINUS_EQ:
			printf("MINUS_EQ");
			break;
		case MINUS_NE:
			printf("MINUS_NE");
			break;
		case NE:
			printf("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_PLUS:
			printf("VAR_EQ_PLUS");
			break;
		case VAR_EQ_TIMES:
			printf("VAR_EQ_TIMES");
			break;
		case VAR_EQ_MINUS_ABS:
			printf("VAR_EQ_MINUS_ABS");
			break;
		case LINEAR_NE:
			printf("LINEAR_NE");
			break;
		case LINEAR_LT:
			printf("LINEAR_LT");
			break;
		case BOOL_OR:
			printf("BOOL_OR");
			break;
		case BOOL_AND:
			printf("BOOL_AND");
			break;
		case BOOL_CLAUSE:
			printf("BOOL_CLAUSE");
			break;
		case BOOL2INT:
			printf("BOOL2INT");
			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 AT_LEAST:
			return"AT_LEAST";
			break;
		case AT_MOST:
			return "AT_MOST";
			break;
		case AT_MOST_ONE:
			return "AT_MOST_ONE";
			break;
		case ELEMENT:
			return "ELEMENT";
			break;
		case ELEMENT_INT_VAR:
			return "ELEMENT_INT_VAR";
			break;
		case ELEMENT_VAR:
			return "ELEMENT_VAR";
			break;
		case EQ:
			return "EQ";
			break;
		case EQ_VAR:
			return "EQ_VAR";
			break;
		case EXACTLY:
			return "EXACTLY";
			break;
		case EXACTLY_VAR:
			return "EXACTLY_VAR";

			break;
		case LE:
			return "LE";
			break;
		case LINEAR:
			return "LINEAR";
			break;
		case LINEAR_VAR:
			return "LINEAR_VAR";
			break;
		case LT:
			return "LT";
			break;

		case MAX:
			return "MAX";
			break;
		case MAXIMIZE:
			return "MAXIMIZE";
			break;
		case MIN:
			return "MIN";
			break;
		case MINIMIZE:
			return "MINIMIZE";
			break;
		case MINUS_EQ:
			return "MINUS_EQ";
			break;
		case MINUS_NE:
			return "MINUS_NE";
			break;
		case NE:
			return "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_PLUS:
			return "VAR_EQ_PLUS";
			break;
		case VAR_EQ_TIMES:
			return "VAR_EQ_TIMES";
			break;
		case VAR_EQ_MINUS_ABS:
			return "VAR_EQ_MINUS_ABS";
			break;
		case LINEAR_NE:
			return "LINEAR_NE";
			break;
		case LINEAR_LT:
			return "LINEAR_LT";
			break;
		case BOOL_OR:
			return "BOOL_OR";
			break;
		case BOOL_AND:
			return "BOOL_AND";
			break;
		case BOOL_CLAUSE:
			return "BOOL_CLAUSE";
			break;
		case BOOL2INT:
			return "BOOL2INT";
			break;
		default:
			return "NOT_RECOGNIZED";
			break;
	}
}

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