/*
 * at_most.c
 *
 *  Created on: 26/03/2017
 *      Author: pedro
 */

#ifndef __OPENCL_VERSION__

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

#include "at_most.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 at_most type and return the constraint ID
 * #{i | X[i] = k} <= n
 * n - maximum number of variables in X that may contain k
 * X_ids - vector with the ID of the variables that may contain k
 * n_vs - maximum number of variables in X vector
 * k - Value that should be set in at most n variables of X
 */
unsigned int c_at_most(unsigned int n, unsigned int* X_ids, unsigned int n_vs, unsigned int k) {
	unsigned int i;

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

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

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

	int consts[2];
	consts[0] = (int)n;
	consts[1] = (int)k;

	// creates a new generic constraint
	unsigned int c_id = c_new(c_vs, n_vs, consts, 2, -1);

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

	free(c_vs);

	return c_id;
}

/*
 * Creates a new reified constraint of the at_most type and return the constraint ID
 * #{i | X[i] = k} <= n
 * n - maximum number of variables in X that may contain k
 * X_ids - vector with the ID of the variables that may contain k
 * n_vs - maximum number of variables in X vector
 * k - Value that should be set in at most n variables of X
 * reif_v_id - ID of the reification variable
 */
unsigned int c_at_most_reif(unsigned int n, unsigned int* X_ids, unsigned int n_vs, unsigned int k, 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 AT_MOST_REIF makes model inconsistent at creation:\n");
			exit(-1);
		}
	}

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

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

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

	int consts[2];
	consts[0] = (int)n;
	consts[1] = (int)k;

	// creates a new generic constraint
	unsigned int c_id = c_new(c_vs, n_vs, consts, 2, reif_v_id);

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

	free(c_vs);

	return c_id;
}

/*
 * Return true if the at_most constraint is respected or false if not
 * #{i | X[i] = k} <= n
 * 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 at_most_check(constr* c, bool explored) {
	var** X = c->c_vs;
	var* x;
	int n = c->c_consts[0];
	int k = c->c_consts[1];
	int set = 0;
	unsigned int i;

	for (i = 0; i < c->n_c_vs; i++) {
		x = X[i];

#if CHECK_SOL_N_VALS
		if (x->to_label && x->n_vals != 1) {

			if (explored) {
				fprintf(stderr, "\nError: Constraint AT_MOST (%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;

		} else
#endif

		if (x->min == k) {
			set++;
		}
	}

	// if more than n variables are set to k
	if (set > n) {

		if (explored) {
			fprintf(stderr, "\nError: Constraint AT_MOST (%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_AT_MOST == 1
/*
 * Propagate the domain of the variable with the ID prop_v_id through all the other variables on the same c_numb ID at_most constraint
 * #{i | X[i] = k} <= n
 * 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
 * c_consts - vector with all constrained constants 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 at_most_prop(CL_INTS_MEM int* vs_per_c_idx, CL_INTS_MEM int* c_consts, 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 n = c_consts[0];
	int k = c_consts[1];
	int set = 0;
	int possible = 0;
	bool contains;
	int x_id;
	bool changed = 0;
	int i;

	for (i = 0; i < current_cs->n_c_vs; i++) {
		CHECK_TTL(ttl_ctr, 40)
		x_id = vs_per_c_idx[i];

		// if more than n variables are already set to k, return 0
		if (V_N_VALS(vs_prop_[x_id]) == 1 && V_MIN(vs_prop_[x_id]) == k) {
			if (++set > n) {
				*prop_ok = 0;
				return;
			}
			// number of variables that may be set to k
		} else {
			cl_v_contains_val_m(&contains, &vs_prop_[x_id], k TTL_CTR_V);
			if (contains) {
				possible++;
			}
		}
	}

	// if all the variables already assigned to k are n, remove k from the other variables
	if (set == n) {

		for (i = 0; possible > 0; i++) {
			x_id = vs_per_c_idx[i];

			CHECK_TTL(ttl_ctr, 41)
			if (V_N_VALS(vs_prop_[x_id]) > 1) {

				cl_v_del_val_m(&changed, &vs_prop_[x_id], k TTL_CTR_V);
				if (changed) {
					possible--;
					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_AT_MOST == 1
/*
 * Validate at_most constraint to be normally propagated, when reified
 * #{i | X[i] = k} <= n
 * vs_per_c_idx - vector with all constrained variables ID per constraint, per constraint ID order
 * c_consts - vector with all constrained constants 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 at_most_reif( CL_INTS_MEM int* vs_per_c_idx, CL_INTS_MEM int* c_consts, 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 n = c_consts[0];
	int k = c_consts[1];
	int set = 0;
	int possible = 0;
	bool contains;
	int x_id;
	int i;

	for (i = 0; i < current_cs->n_c_vs; i++) {
		CHECK_TTL(ttl_ctr, 42)
		x_id = vs_per_c_idx[i];

		// if more than n variables are already set to k, return 0
		if (V_N_VALS(vs_prop_[x_id]) == 1 && V_MIN(vs_prop_[x_id]) == k) {
			if (++set > n) {
				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;
				// number of variables that may be set to k
			} else {
				cl_v_contains_val_m(&contains, &vs_prop_[x_id], k TTL_CTR_V);
				if (contains) {
					possible++;
				}
			}
		}
	}

	// constraint already fixed
	if (set + possible <= n) {
		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
	}
}

/*
 * Propagate the domain of the variable with the ID prop_v_id through all the other variables on the same c_numb ID at_most opposite constraint
 * #{i | X[i] = k} > n
 * vs_per_c_idx - vector with all constrained variables ID per constraint, per constraint ID order
 * c_consts - vector with all constrained constants 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 at_most_prop_opposite(CL_INTS_MEM int* vs_per_c_idx, CL_INTS_MEM int* c_consts, 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 n = c_consts[0];
	int k = c_consts[1];
	int set = 0;
	int possible = 0;
	bool contains;
	int x_id;
	bool changed = 0;
	int i;

	for (i = 0; i < current_cs->n_c_vs; i++) {
		CHECK_TTL(ttl_ctr, 206)
		x_id = vs_per_c_idx[i];

		// number of variables already set to k
		if (V_N_VALS(vs_prop_[x_id]) == 1 && V_MIN(vs_prop_[x_id]) == k) {
			set++;
			// number of variables that may be set to k
		} else {
			cl_v_contains_val_m(&contains, &vs_prop_[x_id], k TTL_CTR_V);
			if (contains) {
				possible++;
			}
		}
	}

	// if there are not enough variables to set to k
	if (set + possible <= n) {
		*prop_ok = 0;
		return;
	}

	// if the sum of the variables that contain k are n+1, assign all of them to k
	if (set + possible == n + 1) {

		for (i = 0; possible > 0; i++) {
			x_id = vs_per_c_idx[i];

			CHECK_TTL(ttl_ctr, 205)
			if (V_N_VALS(vs_prop_[x_id]) > 1) {
				cl_v_contains_val_m(&contains, &vs_prop_[x_id], k TTL_CTR_V);

				if (contains) {
					cl_v_del_all_except_val_m(&changed, &vs_prop_[x_id], k TTL_CTR_V);
					possible--;
					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 at_most_propagate(CL_INTS_MEM int* vs_per_c_idx, CL_INTS_MEM int* c_consts, 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_AT_MOST == 0
	at_most_prop(vs_per_c_idx, c_consts, 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_AT_MOST == 1
	if (current_cs->reified == 1) {
		if (V_N_VALS(vs_prop_[current_cs->reif_var_id]) > 1) {
			at_most_reif(vs_per_c_idx, c_consts, 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) {
				at_most_prop(vs_per_c_idx, c_consts, vs_prop_, current_cs, vs_id_to_prop_, prop_ok CS_IGNORE_CALL TTL_CTR_V);
			} else {
				at_most_prop_opposite(vs_per_c_idx, c_consts, vs_prop_, current_cs, vs_id_to_prop_, prop_ok CS_IGNORE_CALL TTL_CTR_V);
			}
#if CL_STATS == 1
			*propagated = true;
#endif
		}
	} else {
		at_most_prop(vs_per_c_idx, c_consts, 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