/*
 * bool_and.c
 *

 *  Created on: 20/01/2018
 *      Author: pedro

 */

#ifndef __OPENCL_VERSION__

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

#include "bool_and.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_and and return the constraint ID

 * (∀ i ∈ 1..n : X[i]) ↔ y
 * X_ids - vector with the ID of the boolean variables that must be assigned with 1 (true)
 * n_vs - maximum number of boolean variables in X vector
 * y - boolean variable whose assignment is the result of the binary AND between X variables

 */

unsigned int c_bool_and(unsigned int* X_ids, unsigned int n_vs, unsigned int y_id) {

	unsigned int i;

	for (i = 0; i < n_vs + 1; i++) {

		if (VS[X_ids[i]].max > 1) {

			v_del_gt(&VS[X_ids[i]], 1);

			if (VS[X_ids[i]].n_vals == 0) {
				fprintf(stderr, "\nError: Constraint BOOL_AND makes model inconsistent at creation:\n");
				exit(-1);
			}
		}
	}

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

	unsigned int* c_vs = malloc((n_vs + 1) * sizeof(unsigned int));

	for (i = 0; i < n_vs; i++) {
		c_vs[i] = X_ids[i];
	}
	c_vs[i] = y_id;

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

	// pointers to this type of constraint functions
	CS[c_id].kind = BOOL_AND;
	CS[c_id].check_sol_f = &bool_and_check;
	CS[c_id].constant_val = 0;

	free(c_vs);

	return c_id;
}

/*
 * Creates a new reified constraint of the bool_and type
 * (∀ i ∈ 1..n : X[i]) ↔ y

 * X_ids - vector with the ID of the boolean variables that must be assigned with 1 (true)
 * n_vs - maximum number of boolean variables in X vector
 * y - boolean variable whose assignment must be equal to all the X variables
 * reif_v_id - ID of the reification variable
 */
unsigned int c_bool_and_reif(unsigned int* X_ids, unsigned int n_vs, unsigned int y_id, int reif_v_id) {
	unsigned int i;

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

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

			fprintf(stderr, "\nError: Constraint BOOL_AND_REIF makes model inconsistent at creation:\n");
			exit(-1);

		}

	}

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

			if (VS[X_ids[i]].n_vals == 0) {
				fprintf(stderr, "\nError: Constraint BOOL_AND_REIF makes model inconsistent at creation:\n");
				exit(-1);
			}
		}

	}

	// set to include in kernel compilation
	USE_CS[BOOL_AND] = 1;

	USE_CS_REIFI[BOOL_AND] = 1;
	REV = 1;

	unsigned int* c_vs = malloc((n_vs + 1) * sizeof(unsigned int));

	for (i = 0; i < n_vs; i++) {
		c_vs[i] = X_ids[i];
	}
	c_vs[i] = y_id;

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

	// pointers to this type of constraint functions
	CS[c_id].kind = BOOL_AND;
	CS[c_id].check_sol_f = &bool_and_check;
	CS[c_id].constant_val = 0;

	free(c_vs);

	return c_id;
}

/*
 * Return true if the bool_and constraint is respected or false if not
 * (∀ i ∈ 1..n : X[i]) ↔ y
 * c - constraint to check if is respected
 * explored - if the CSP was already explored, which mean that all the variables must already be singletons
 * */
bool bool_and_check(constr* c, bool explored) {
	var** X = c->c_vs;
	var* y = c->c_vs[c->n_c_vs - 1];
	int sum = 0;
	unsigned int i;

	for (i = 0; i < c->n_c_vs; i++) {

#if CHECK_SOL_N_VALS
		if (X[i]->to_label && X[i]->n_vals != 1) {

			if (explored) {
				fprintf(stderr, "\nError: Constraint BOOL_AND (%d) not respected:\n", c->c_id);

				for (i = 0; i < c->n_c_vs; i++) {
					fprintf(stderr, "Variable ID=%u -> minimum=%u, maximum=%u, number of values=%u\n\n", c->c_vs[i]->v_id, b_get_min_val(&c->c_vs[i]->domain_b),
							b_get_max_val(&c->c_vs[i]->domain_b),

							b_cnt_vals(&c->c_vs[i]->domain_b));
				}
			}
			return false;
		}

#endif

		sum += X[i]->min;

	}

	if (sum == c->n_c_vs - 1 && y->min == 0) {

		if (explored) {

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

			for (i = 0; i < c->n_c_vs; i++) {
				fprintf(stderr, "Variable ID=%u -> minimum=%u, maximum=%u, number of values=%u\n\n", c->c_vs[i]->v_id, b_get_min_val(&c->c_vs[i]->domain_b),
						b_get_max_val(&c->c_vs[i]->domain_b),
						b_cnt_vals(&c->c_vs[i]->domain_b));
			}
		}
		return false;

	}

	return true;
}

#endif

#if CS_BOOL_AND == 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_and constraint
 * (∀ i ∈ 1..n : X[i]) ↔ y
 * prop_ok will be set to 1 if success or to 0 if any domain became empty
 * 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
 * prop_v_id - variable ID to propagate
 * 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_and_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_id = vs_per_c_idx[current_cs->n_c_vs - 1];

	int x_id;

	int zero_v_id;

	int zeros_ctr = 0;
	int ones_ctr = 0;
	bool changed;
	int i;

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

		for (i = 0; i < current_cs->n_c_vs - 1; i++) {
			x_id = vs_per_c_idx[i];

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

				// if y has 2 values and an x is already 0
				if (V_MIN(vs_prop_[x_id]) == 0) {
					cl_v_bool_del_val_m(&vs_prop_[y_id], 1 TTL_CTR_V);
					v_add_to_prop(vs_id_to_prop_, vs_prop_, y_id);

#if CL_CS_IGNORE

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

					return;

				} else {

					ones_ctr++;
				}

			}
		}

		// if y has 2 values and all x are already 1
		if (ones_ctr == current_cs->n_c_vs - 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);

#if CL_CS_IGNORE

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

	// y is 0

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

		for (i = 0; i < current_cs->n_c_vs - 1; i++) {
			x_id = vs_per_c_idx[i];

			if (V_MIN(vs_prop_[x_id]) == 0) {
				zero_v_id = x_id;
				zeros_ctr++;

				// if y is 0 and an x is already 0 or more than one x can yet be 0
				if (zeros_ctr == 2 || V_N_VALS(vs_prop_[x_id]) == 1) {

#if CL_CS_IGNORE

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

						cs_ignore[current_cs->c_id] = 1;
					}

#endif
					return;

				}

			}

		}

		// if y is 0 and and no x can be 0
		if (zeros_ctr == 0) {
			*prop_ok = 0;

		// if y is 0 and only one x can be 0
		} else {

			cl_v_bool_del_val_m(&vs_prop_[zero_v_id], 1 TTL_CTR_V);

			v_add_to_prop(vs_id_to_prop_, vs_prop_, zero_v_id);

#if CL_CS_IGNORE

			cs_ignore[current_cs->c_id] = 1;

#endif
		}

	// if y is 1 set all x to 1
	} else {
		for (i = 0; i < current_cs->n_c_vs - 1; i++) {
			x_id = vs_per_c_idx[i];

			cl_v_del_all_except_val_m(&changed, &vs_prop_[x_id], 1 TTL_CTR_V);

			if (changed) {

				// if the removal of the value resulted in an empty domain return 0
				if (V_IS_EMPTY(vs_prop_[x_id])) {
					*prop_ok = 0;
					return;

				}

				v_add_to_prop(vs_id_to_prop_, vs_prop_, x_id);
			}
		}
#if CL_CS_IGNORE
		cs_ignore[current_cs->c_id] = 1;
#endif
	}
}

#if CS_R_BOOL_AND == 1
/*
 * Validate bool_and constraint to be normally propagated, when reified
 * (∀ i ∈ 1..n : X[i]) ↔ y

 * 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_and_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_id = vs_per_c_idx[current_cs->n_c_vs - 1];
	int x_id;
	bool all_singleton = true;
	int i;

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

		// if y=1 than all X variables must contain 1

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

			for (i = 0; i < current_cs->n_c_vs - 1; i++) {

				x_id = vs_per_c_idx[i];

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

					if (V_MIN(vs_prop_[x_id]) == 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
					return;

					}
				} else {
					all_singleton = false;
				}

			}
			if (all_singleton) {

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

		// if y=0, than at least one X variable must contain 0
		if (V_MIN(vs_prop_[y_id]) == 0) {

			for (i = 0; i < current_cs->n_c_vs - 1; i++) {
				x_id = vs_per_c_idx[i];

				// one x is 0
				if (V_N_VALS(vs_prop_[x_id]) == 1 && V_MIN(vs_prop_[x_id]) == 0) {

					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;

				// an x can yet be 0

				} else if (V_N_VALS(vs_prop_[x_id]) > 1) {

					return;
				}
			}

			// all x are 1
			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_and opposite constraint

 * (∀ i !∈ 1..n : X[i]) ↔ y

 * 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
 * prop_v_id - variable ID to propagate
 * 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_and_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_id = vs_per_c_idx[current_cs->n_c_vs - 1];
	int x_id;

	int zero_v_id;

	int zeros_ctr = 0;
	int ones_ctr = 0;
	bool changed;

	int i;

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

		for (i = 0; i < current_cs->n_c_vs - 1; i++) {
			x_id = vs_per_c_idx[i];

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

				// if y has 2 values and an x is already 0
				if (V_MIN(vs_prop_[x_id]) == 0) {
					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);

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

					return;

				} else {

					ones_ctr++;

				}
			}

		}

		// if y has 2 values and all x are already 1
		if (ones_ctr == current_cs->n_c_vs - 1) {
			cl_v_bool_del_val_m(&vs_prop_[y_id], 1 TTL_CTR_V);

			v_add_to_prop(vs_id_to_prop_, vs_prop_, y_id);

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

	// y is 0
	} else if (V_MIN(vs_prop_[y_id]) == 1) {

		for (i = 0; i < current_cs->n_c_vs - 1; i++) {
			x_id = vs_per_c_idx[i];

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

				zero_v_id = x_id;
				zeros_ctr++;

				// if y is 0 and an x is already 0 or more than one x can yet be 0
				if (zeros_ctr == 2 || V_N_VALS(vs_prop_[x_id]) == 1) {

#if CL_CS_IGNORE

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

						cs_ignore[current_cs->c_id] = 1;

					}

#endif
					return;
				}
			}
		}

		// if y is 0 and and no x can be 0

		if (zeros_ctr == 0) {

			*prop_ok = 0;

		// if y is 0 and only one x can be 0
		} else {

			cl_v_bool_del_val_m(&vs_prop_[zero_v_id], 1 TTL_CTR_V);

			v_add_to_prop(vs_id_to_prop_, vs_prop_, zero_v_id);

#if CL_CS_IGNORE

			cs_ignore[current_cs->c_id] = 1;

#endif

		}

	// if y is 1 set all x to 0
	} else {
		for (i = 0; i < current_cs->n_c_vs - 1; i++) {
			x_id = vs_per_c_idx[i];

			cl_v_del_val_m(&changed, &vs_prop_[x_id], 1 TTL_CTR_V);

			if (changed) {

				// if the removal of the value resulted in an empty domain return 0

				if (V_IS_EMPTY(vs_prop_[x_id])) {

					*prop_ok = 0;

					return;
				} else {
					v_add_to_prop(vs_id_to_prop_, vs_prop_, x_id);
				}
			}

		}

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

#endif
	}

}

#endif

CUDA_FUNC void bool_and_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_AND == 0
	bool_and_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_AND == 1

	if (current_cs->reified == 1) {

		if (V_N_VALS(vs_prop_[current_cs->reif_var_id]) > 1) {
			bool_and_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_and_prop(vs_per_c_idx, vs_prop_, current_cs, vs_id_to_prop_, prop_ok CS_IGNORE_CALL TTL_CTR_V);
			} else {
				bool_and_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_and_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