/*
 * schurs.c
 *
 *  Created on: 18/11/2017
 *      Author: pedro
 *
 *      https://github.com/MiniZinc/minizinc-benchmarks/blob/master/schur_numbers/schur.mzn
 *
 *		Schurs numbers:
 *		Determine if N balls labelled 0..n-1 can be placed in K boxes with
 *		no box containing a triple {x,y,z} where x+y=z
 */

#include "schurs.h"

#include <stdbool.h>
#include <stdio.h>
#include <stdlib.h>
#include <sys/types.h>

#include "../config.h"
#include "../constraints/ne.h"
#include "../constraints/bool_or.h"
#include "../split.h"
#include "../variables.h"

/*
 * Solve the Schurs numbers problem with N values
 */
void run_schurs(int* csp_dims) {
	int k = csp_dims[0];
	int n = csp_dims[1];
	unsigned long result;
	unsigned int *box;
	unsigned int reif[3];
	unsigned int or_v_id;
	int i, j;

	// N - number of balls
	// K - number of boxes
	box = malloc((unsigned long)n * sizeof(unsigned int));

	for (i = 0; i < n; i++) {
		box[i] = v_new_range(0, (unsigned int)k - 1, true);
	}

	or_v_id = v_new_val(1);
	for (i = 1; i < n; i++) {
		for (j = i + 1; j < n - i + 1; j++) {
			reif[0] = v_new_range(0, 1, false);
			reif[1] = v_new_range(0, 1, false);
			reif[2] = v_new_range(0, 1, false);

			c_ne_reif(box[i - 1], box[j - 1], (int)reif[0]);
			c_ne_reif(box[i - 1], box[i + j - 1], (int)reif[1]);
			c_ne_reif(box[j - 1], box[i + j - 1], (int)reif[2]);

			c_bool_or(reif, 3, or_v_id);
		}
	}

	if (FINDING_ONE_SOLUTION) {
		printf("\nFinding one solution for Schurs numbers with %u balls and %u boxes.\n", n, k);
	} else {
		printf("\nCounting all the solutions for Schurs numbers with %u balls and %u boxes.\n", n, k);
	}

	// Solve the CSP
	result = solve_CSP();

	if (FINDING_ONE_SOLUTION && result == 1) {
		printf("Solution:\n");
		vs_print_single_val(box, (unsigned int)n, 1);
		printf("\n");
	} else {
		printf("%lu solution(s) found\n", result);
	}

	free(box);
}