/*
 * bool_clause.c
 *
 *  Created on: 19/10/2018

 *      Author: Pedro

 */

#ifndef __OPENCL_VERSION__

#include <stddef.h>
#include <stdio.h>

#include "bool_clause.h"

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

#endif

#include "../kernels/cl_aux_functions.h"
#if CL_D_TYPE == CL_BITMAP
#include "../kernels/cl_bitmaps.h"
#elif CL_D_TYPE == CL_INTERVAL
#include  "../kernels/cl_intervals.h"
#endif
#include "../kernels/cl_constraints.h"
#include "../kernels/cl_variables.h"
#include "../kernels/cl_ttl.h"

#ifndef __OPENCL_VERSION__

/*
 * Creates a new constraint of the type bool_clause and return the constraint ID
 * (∃ i ∈ 1..nx : X[i]) ∨ (∃ i ∈ 1..ny : ¬Y[i])
 * X_ids - IDs of variables x
 * n_x - number of variables in X_ids
 * Y_ids - IDs of variable y
 * n_y - number of variables in Y_ids
 */

unsigned int c_bool_clause(unsigned int *X_ids, unsigned int n_x, unsigned int *Y_ids, unsigned int n_y) {

	unsigned int i, j;

	for (i = 0; i < n_x; i++) {
		if (VS[X_ids[i]].max > 1) {
			v_del_gt(&VS[X_ids[i]], 1);

			if (VS[X_ids[i]].n_vals == 0) {

				printf("\nConstraint BOOL_CLAUSE makes model inconsistent at creation. No solution found.\n");

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

				exit(0);

			}
		}
	}
	for (i = 0; i < n_y; i++) {
		if (VS[Y_ids[i]].max > 1) {
			v_del_gt(&VS[Y_ids[i]], 1);

			if (VS[Y_ids[i]].n_vals == 0) {

				printf("\nConstraint BOOL_CLAUSE makes model inconsistent at creation. No solution found.\n");

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

				exit(0);

			}
		}
	}

	// set to include in kernel compilation
	USE_CS[BOOL_CLAUSE] = 1;
	USE_NON_CS_REIFI[BOOL_CLAUSE] = 1;
	REV = 1;

	unsigned int *c_vs = malloc((n_x + n_y) * sizeof(unsigned int));

	for (i = 0; i < n_x; i++) {
		c_vs[i] = X_ids[i];
	}
	for (j = 0; j < n_y; j++) {
		c_vs[i++] = Y_ids[j];
	}

	// creates a new generic constraint
	unsigned int c_id = c_new(c_vs, n_x + n_y, NULL, 0, -1);

	// pointers to this type of constraint functions
	CS[c_id].kind = BOOL_CLAUSE;
	CS[c_id].check_sol_f = &bool_clause_check;

	CS[c_id].constant_val = (int) n_x;	// begin of second array

	free(c_vs);

	return c_id;
}

/*
 * Creates a new constraint of the type bool_clause and return the constraint ID
 * (∃ i ∈ 1..nx : X[i]) ∨ (∃ i ∈ 1..ny : ¬Y[i])
 * X_ids - IDs of variables x
 * n_x - number of variables in X_ids
 * Y_ids - IDs of variable y
 * n_y - number of variables in Y_ids
 * reif_v_id - ID of the reification variable
 */

unsigned int c_bool_clause_reif(unsigned int *X_ids, unsigned int n_x, unsigned int *Y_ids, unsigned int n_y, int reif_v_id) {

	unsigned int i, j;

	if (VS[reif_v_id].max > 1) {
		v_del_gt(&VS[reif_v_id], 1);

		if (VS[reif_v_id].n_vals == 0) {

			printf("\nConstraint BOOL_CLAUSE_REIF makes model inconsistent at creation. No solution found.\n");

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

			exit(0);

		}
	}

	for (i = 0; i < n_x; i++) {
		if (VS[X_ids[i]].max > 1) {
			v_del_gt(&VS[X_ids[i]], 1);

			if (VS[X_ids[i]].n_vals == 0) {

				printf("\nConstraint BOOL_CLAUSE_REIF makes model inconsistent at creation. No solution found.\n");

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

				exit(0);

			}
		}
	}
	for (i = 0; i < n_y; i++) {
		if (VS[Y_ids[i]].max > 1) {
			v_del_gt(&VS[Y_ids[i]], 1);

			if (VS[Y_ids[i]].n_vals == 0) {

				printf("\nConstraint BOOL_CLAUSE_REIF makes model inconsistent at creation. No solution found.\n");

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

				exit(0);

			}
		}
	}

	// set to include in kernel compilation
	USE_CS[BOOL_CLAUSE] = 1;
	USE_CS_REIFI[BOOL_CLAUSE] = 1;
	REV = 1;

	unsigned int *c_vs = malloc((n_x + n_y) * sizeof(unsigned int));

	for (i = 0; i < n_x; i++) {
		c_vs[i] = X_ids[i];
	}
	for (j = 0; j < n_y; j++) {
		c_vs[i++] = Y_ids[j];
	}

	// creates a new generic constraint
	unsigned int c_id = c_new(c_vs, n_x + n_y, NULL, 0, reif_v_id);

	// pointers to this type of constraint functions
	CS[c_id].kind = BOOL_CLAUSE;
	CS[c_id].check_sol_f = &bool_clause_check;

	CS[c_id].constant_val = (int) n_x;	// begin of second array

	free(c_vs);

	return c_id;
}

/*
 * Return true if the bool_clause constraint is respected or false if not
 * (∃ i ∈ 1..nx : X[i]) ∨ (∃ i ∈ 1..ny : ¬Y[i])
 * c - constraint to check if is respected
 * explored - if the CSP was already explored, which mean that all the variables must already be singletons
 * */

#pragma GCC diagnostic push
#pragma GCC diagnostic ignored "-Wunused-parameter"

bool bool_clause_check(constr *c, bool explored) {

	int y_begin = c->constant_val;
	int n = c->n_c_vs;
	int i;

	if (!explored) {
		for (i = 0; i < c->n_c_vs; i++) {
			if (c->c_vs[i]->n_vals > 1) {
				return false;
			}
		}
	}

	if (c->reified && VS[c->reif_v_id].n_vals > 1) {
		if (explored) {
			fprintf(stderr, "\nError: Reification variable of constraint BOOL_CLAUSE_REIF (%d) has 2 values.\n", c->c_id);
			return false;
		}
	}

	if (((!c->reified || (c->reified && VS[c->reif_v_id].min == 1)) && c->reified && VS[c->reif_v_id].n_vals > 1)
			|| (c->reified && VS[c->reif_v_id].min == 0 && c->reified && VS[c->reif_v_id].n_vals <= 1)) {

		if (explored) {

			if (c->reified) {
				fprintf(stderr, "\nError: Constraint BOOL_CLAUSE_REIF (%d) not respected:\n", c->c_id);
				fprintf(stderr, "Reif ID=%u -> minimum=%u, maximum=%u, number of values=%u\n\n", c->reif_v_id, b_get_min_val(&VS[c->reif_v_id].domain_b),
						b_get_max_val(&VS[c->reif_v_id].domain_b), b_cnt_vals(&VS[c->reif_v_id].domain_b));

			} else {
				fprintf(stderr, "\nError: Constraint BOOL_CLAUSE (%d) not respected:\n", c->c_id);

			}
			return false;
		}
	}

	for (i = 0; i < y_begin; i++) {
		if (c->c_vs[i]->min == 1) {
			return true;
		}
	}
	for (i = 0; i < n; i++) {
		if (c->c_vs[i]->min == 0) {
			return true;
		}
	}
	return false;
}
#pragma GCC diagnostic pop

#endif

#if CS_BOOL_CLAUSE == 1
/*
 * Propagate the domain of the variable with the ID prop_v_id through all the other variables on the same c_numb ID bool_clause constraint
 * (∃ i ∈ 1..nx : X[i]) ∨ (∃ i ∈ 1..ny : ¬Y[i])

 * vs_per_c_idx - vector with all constrained variables ID per constraint, per constraint ID order
 * vs_prop_ - all CSP variables with current step values

 * current_cs - constraint that should be propagated for the variable with prop_v_id ID
 * vs_id_to_prop_ - circular vector with the ids of the variables to propagate

 * prop_ok - will be set to 1 or 0 if the constraint is respected or not

 */

CUDA_FUNC void bool_clause_prop(CL_INTS_MEM int *vs_per_c_idx, CL_MEMORY VARS_PROP *vs_prop_, CL_CS_MEM cl_constr *current_cs,
		CL_MEMORY unsigned short *vs_id_to_prop_, bool *prop_ok CS_IGNORE_FUNC TTL_CTR) {

	int y_begin_id = current_cs->constant_val;
	int n_vs = current_cs->n_c_vs;
	int x_not_singl_ctr = 0;
	int x_not_singl_id = -1;
	int y_not_singl_ctr = 0;
	int y_not_singl_id = -1;
	int x_id, y_id;
	int i;

	for (i = 0; i < y_begin_id; i++) {
		x_id = vs_per_c_idx[i];

		if (V_N_VALS(vs_prop_[x_id]) == 1) {

			if (V_MIN(vs_prop_[x_id]) == 1) {

#if CL_CS_IGNORE

				cs_ignore[current_cs->c_id] = 1;

#endif

				return;
			}

		} else {
			x_not_singl_ctr++;
			x_not_singl_id = x_id;
		}
	}

	for (i = 0; i < n_vs - y_begin_id; i++) {
		y_id = vs_per_c_idx[y_begin_id + i];

		if (V_N_VALS(vs_prop_[y_id]) == 1) {

			if (V_MIN(vs_prop_[y_id]) == 0) {

#if CL_CS_IGNORE

				cs_ignore[current_cs->c_id] = 1;

#endif

				return;
			}

		} else {
			y_not_singl_ctr++;
			y_not_singl_id = y_id;
		}
	}

	if (x_not_singl_ctr == 0 && y_not_singl_ctr == 0) {
		*prop_ok = 0;
		return;
	}

	if (x_not_singl_ctr == 1 && y_not_singl_ctr == 0) {
		cl_v_bool_del_val_m(&vs_prop_[x_not_singl_id], 0 TTL_CTR_V);
		v_add_to_prop(vs_id_to_prop_, vs_prop_, x_not_singl_id);

#if CL_CS_IGNORE
		cs_ignore[current_cs->c_id] = 1;
#endif

	} else if (x_not_singl_ctr == 0 && y_not_singl_ctr == 1) {
		cl_v_bool_del_val_m(&vs_prop_[y_not_singl_id], 1 TTL_CTR_V);
		v_add_to_prop(vs_id_to_prop_, vs_prop_, y_not_singl_id);

#if CL_CS_IGNORE
		cs_ignore[current_cs->c_id] = 1;
#endif
	}
}

#if CS_R_BOOL_CLAUSE == 1
/*
 * Validate bool_clause constraint to be normally propagated, when reified
 * (∃ i ∈ 1..nx : X[i]) ∨ (∃ i ∈ 1..ny : ¬Y[i])
 * vs_per_c_idx - vector with all constrained variables ID per constraint, per constraint ID order
 * vs_prop_ - all CSP variables with current step values
 * current_cs - constraint that should be propagated for the variable with prop_v_id ID
 * vs_id_to_prop_ - circular vector with the ids of the variables to propagate
 */

CUDA_FUNC void bool_clause_reif( CL_INTS_MEM int *vs_per_c_idx, CL_MEMORY VARS_PROP *vs_prop_, CL_CS_MEM cl_constr *current_cs,
		CL_MEMORY unsigned short *vs_id_to_prop_ CS_IGNORE_FUNC TTL_CTR) {

	int y_begin_id = current_cs->constant_val;
	int n_vs = current_cs->n_c_vs;
	int x_not_singl_ctr = 0;
	int y_not_singl_ctr = 0;
	int x_id, y_id;
	int i;

	for (i = 0; i < y_begin_id; i++) {
		x_id = vs_per_c_idx[i];

		if (V_N_VALS(vs_prop_[x_id]) == 1) {
			if (V_MIN(vs_prop_[x_id]) == 1 || x_not_singl_ctr > 1) {

				cl_v_bool_del_val_m(&vs_prop_[current_cs->reif_var_id], 0 TTL_CTR_V);

				v_add_to_prop(vs_id_to_prop_, vs_prop_, convert_int (current_cs->reif_var_id));

#if CL_CS_IGNORE
				cs_ignore[current_cs->c_id] = 1;
#endif
				return;
			}

			x_not_singl_ctr++;
		}
	}

	for (i = 0; i < n_vs - y_begin_id; i++) {
		y_id = vs_per_c_idx[i + y_begin_id];

		if (V_N_VALS(vs_prop_[y_id]) == 1) {
			if (V_MIN(vs_prop_[y_id]) == 0 || y_not_singl_ctr > 1) {

				cl_v_bool_del_val_m(&vs_prop_[current_cs->reif_var_id], 0 TTL_CTR_V);

				v_add_to_prop(vs_id_to_prop_, vs_prop_, convert_int (current_cs->reif_var_id));

#if CL_CS_IGNORE
				cs_ignore[current_cs->c_id] = 1;
#endif
				return;
			}
		} else {
			y_not_singl_ctr++;
		}
	}

	if (x_not_singl_ctr == 0 && y_not_singl_ctr == 0) {
		cl_v_bool_del_val_m(&vs_prop_[current_cs->reif_var_id], 1 TTL_CTR_V);

		v_add_to_prop(vs_id_to_prop_, vs_prop_, convert_int (current_cs->reif_var_id));

#if CL_CS_IGNORE
		cs_ignore[current_cs->c_id] = 1;
#endif
	}
}

/*
 * Propagate the domain of the variable with the ID prop_v_id through all the other variables on the same c_numb ID bool_clause opposite constraint
 * !((∃ i ∈ 1..nx : X[i]) ∨ (∃ i ∈ 1..ny : ¬Y[i]))
 * vs_per_c_idx - vector with all constrained variables ID per constraint, per constraint ID order
 * vs_prop_ - all CSP variables with current step values

 * current_cs - constraint that should be propagated for the variable with prop_v_id ID
 * vs_id_to_prop_ - circular vector with the ids of the variables to propagate

 * prop_ok - will be set to 1 or 0 if the constraint is respected or not

 */

CUDA_FUNC void bool_clause_prop_opposite( CL_INTS_MEM int *vs_per_c_idx, CL_MEMORY VARS_PROP *vs_prop_, CL_CS_MEM cl_constr *current_cs,
		CL_MEMORY unsigned short *vs_id_to_prop_, bool *prop_ok CS_IGNORE_FUNC TTL_CTR) {

	int y_begin_id = current_cs->constant_val;
	int n_vs = current_cs->n_c_vs;
	int x_id, y_id;
	int i;

	for (i = 0; i < y_begin_id; i++) {
		x_id = vs_per_c_idx[i];

		if (V_N_VALS(vs_prop_[x_id]) > 1) {
			cl_v_bool_del_val_m(&vs_prop_[x_id], 1 TTL_CTR_V);
			v_add_to_prop(vs_id_to_prop_, vs_prop_, x_id);

		} else if (V_MIN(vs_prop_[x_id]) == 1) {
			*prop_ok = 0;
			return;
		}
	}

	for (; i < n_vs - y_begin_id; i++) {
		y_id = vs_per_c_idx[i + y_begin_id];

		if (V_N_VALS(vs_prop_[y_id]) > 1) {
			cl_v_bool_del_val_m(&vs_prop_[y_id], 0 TTL_CTR_V);
			v_add_to_prop(vs_id_to_prop_, vs_prop_, y_id);

		} else if (V_MIN(vs_prop_[y_id]) == 0) {
			*prop_ok = 0;
			return;
		}
	}

#if CL_CS_IGNORE
	cs_ignore[current_cs->c_id] = 1;

#endif
}

#endif

/*
 * Decides the propagator to call for this constraint
 * vs_per_c_idx - vector with all constrained variables ID per constraint, per constraint ID order
 * vs_prop_ - all CSP variables with current step values
 * current_cs - constraint that should be propagated for the variable with prop_v_id ID
 * vs_id_to_prop_ - circular vector with the ids of the variables to propagate
 * prop_ok - will be set to 1 or 0 if the constraint is respected or not
 */
CUDA_FUNC void bool_clause_propagate(CL_INTS_MEM int *vs_per_c_idx, CL_MEMORY VARS_PROP *vs_prop_, CL_CS_MEM cl_constr *current_cs,
		CL_MEMORY unsigned short *vs_id_to_prop_, bool *prop_ok PROPAGATED_FUNC CS_IGNORE_FUNC TTL_CTR) {

#if CS_R_BOOL_CLAUSE == 0
	bool_clause_prop(vs_per_c_idx, vs_prop_, current_cs, vs_id_to_prop_, prop_ok CS_IGNORE_CALL TTL_CTR_V);
#if CL_STATS == 1
	*propagated = true;
#endif

#elif CS_R_BOOL_CLAUSE == 1
	if (current_cs->reified == 1) {
		if (V_N_VALS(vs_prop_[current_cs->reif_var_id]) > 1) {
			bool_clause_reif(vs_per_c_idx, vs_prop_, current_cs, vs_id_to_prop_ CS_IGNORE_CALL TTL_CTR_V);

		} else {
			if (V_MIN(vs_prop_[current_cs->reif_var_id]) == 1) {
				bool_clause_prop(vs_per_c_idx, vs_prop_, current_cs, vs_id_to_prop_, prop_ok CS_IGNORE_CALL TTL_CTR_V);
			} else {
				bool_clause_prop_opposite(vs_per_c_idx, vs_prop_, current_cs, vs_id_to_prop_, prop_ok CS_IGNORE_CALL TTL_CTR_V);
			}
#if CL_STATS == 1
			*propagated = true;
#endif
		}
	} else {
		bool_clause_prop(vs_per_c_idx, vs_prop_, current_cs, vs_id_to_prop_, prop_ok CS_IGNORE_CALL TTL_CTR_V);
#if CL_STATS == 1
		*propagated = true;
#endif
	}
#endif
}

#endif