/* See LICENSE file for copyright and license details. */
#include "common.h"
#ifndef TEST


static int canonicalise_dnf(struct expression *this, uint64_t flags);


/**
 * Invert a sentence in place, but
 * require the result to be unrelaxed
 * 
 * The sentence may not contain XOR
 * 
 * @param   this   The sentence to invert (in place)
 * @param   flags  Flags from `libnormalform_express`
 * @return         1 on success, 0 if the inversion could not
 *                 be representated without being relaxed,
 *                 -1 on failure
 * 
 * In case the function returns 0 or -1, `this` may
 * have been partially inverted
 */
static int
perfectly_invert_expression(struct expression *this, uint64_t flags)
{
	struct expression **outer;
	size_t i, j, k, ci, cn, nouter;
	int r;

beginning:
	switch (this->type) {
	case LIBNORMALFORM_TRANSFORMATION:
		this = this->terms[0];
		goto beginning;

	case LIBNORMALFORM_DISJUNCTION:
		/* ¬⋁{⋀{x | x ∈ X} | X ∈ Y} =
		 * ⋀{¬⋀{x | x ∈ X} | X ∈ Y} =
		 * ⋀{⋁{¬x | x ∈ X} | X ∈ Y} =
		 * ⋁{¬x₁ ∧ … ∧ ¬xₙ | x₁ ∈ X₁, …, xₙ ∈ Xₙ, {X₁, …, Xₙ} = Y} */
		outer = NULL;
		nouter = 1U;
		for (i = 0; i < this->nterms; i++) {
			if (this->terms[i]->type != LIBNORMALFORM_CONJUNCTION)
				abort(); /* this function is only used for CDNF */
			if (!this->terms[i]->nterms) {
				nouter = 0;
				break;
			}
			if (this->terms[i]->nterms > SIZE_MAX / nouter) {
				errno = ENOMEM;
				return -1;
			}
			nouter *= this->terms[i]->nterms;
		}
		if (!nouter) {
			for (i = 0; i < this->nterms; i++)
				libnormalform_free_expression__(this->terms[i]);
			free(this->terms);
			this->terms = NULL;
			this->nterms = 0;
			return 0;
		}
		for (i = 0; i < this->nterms; i++) {
			this->reduced |= this->terms[i]->reduced;
			for (j = 0; j < this->terms[i]->nterms; j++)
				this->terms[i]->terms[j]->invert = 1;
		}
		for (i = 0; i < this->nterms; i++) {
			for (j = 0; j < this->terms[i]->nterms; j++) {
				if (!this->terms[i]->terms[j]->invert)
					continue;
				this->terms[i]->terms[j]->invert = 0;
				r = perfectly_invert_expression(this->terms[i]->terms[j], flags);
				if (r <= 0)
					return r;
				if (nouter / this->terms[i]->nterms > SIZE_MAX - this->terms[i]->terms[j]->refcount) {
					errno = ENOMEM;
					return -1;
				}
			}
		}
		for (i = 0; i < nouter; i++) {
			outer[i] = malloc(sizeof(*outer[i]));
			if (!outer[i])
				return -1;
			outer[i]->type = LIBNORMALFORM_CONJUNCTION;
			outer[i]->reduced = 0;
			outer[i]->invert = 0;
			outer[i]->refcount = 1;
			outer[i]->user_item = NULL;
			outer[i]->nterms = 0;
			outer[i]->terms = NULL;
			if (!this->nterms)
				continue;
			outer[i]->terms = malloc(this->nterms * sizeof(*outer[i]->terms));
			if (!outer[i]->terms) {
				free(outer[i]);
				while (i--) {
					free(outer[i]->terms);
					free(outer[i]);
				}
				return -1;
			}
		}
		cn = 1U;
		for (i = this->nterms; i--;) {
			for (k = 0; k < nouter;) {
				for (j = 0; j < this->terms[i]->nterms; j++) {
					this->terms[i]->terms[j]->refcount += cn;
					for (ci = 0; ci < cn; ci++)
						outer[k++]->terms[i] = this->terms[i]->terms[j];
				}
			}
			cn *= this->terms[i]->nterms;
			libnormalform_free_expression__(this->terms[i]);
			this->nterms--;
		}
		free(this->terms);
		this->terms = outer;
		this->nterms = nouter;
		return canonicalise_dnf(this, flags) ? -1 : 1;

	case LIBNORMALFORM_FOR_ALL:
	case LIBNORMALFORM_NEGATED_FOR_ALL:
		if (!(flags & (LIBNORMALFORM_ELIMINATE_FOR_ALL << (this->type - LIBNORMALFORM_FOR_ALL)))) {
			this->type ^= LIBNORMALFORM_FOR_ALL ^ LIBNORMALFORM_NEGATED_FOR_ALL;
			return 1;
		}
		/* ¬∀x.φ = ∃x.¬φ */
		if (flags & (LIBNORMALFORM_ELIMINATE_FOR_ANY << (this->type - LIBNORMALFORM_FOR_ALL)))
			return 0;
		this->type = LIBNORMALFORM_FOR_ANY + (this->type - LIBNORMALFORM_FOR_ALL);
		this = this->terms[this->nterms - 1];
		goto beginning;

	case LIBNORMALFORM_FOR_ANY:
	case LIBNORMALFORM_NEGATED_FOR_ANY:
		if (!(flags & (LIBNORMALFORM_ELIMINATE_FOR_ANY << (this->type - LIBNORMALFORM_FOR_ANY)))) {
			this->type ^= LIBNORMALFORM_FOR_ANY ^ LIBNORMALFORM_NEGATED_FOR_ANY;
			return 1;
		}
		/* ¬∃x.φ = ∀x.¬φ */
		if (flags & (LIBNORMALFORM_ELIMINATE_FOR_ALL << (this->type - LIBNORMALFORM_FOR_ANY)))
			return 0;
		this->type = LIBNORMALFORM_FOR_ALL + (this->type - LIBNORMALFORM_FOR_ANY);
		this = this->terms[this->nterms - 1];
		goto beginning;

	case LIBNORMALFORM_FUNCTION:
	case LIBNORMALFORM_NEGATED_FUNCTION:
		if (flags & (LIBNORMALFORM_ELIMINATE_FUNCTION << (this->type - LIBNORMALFORM_FUNCTION)))
			return 0;
		this->type ^= LIBNORMALFORM_FUNCTION ^ LIBNORMALFORM_NEGATED_FUNCTION;
		return 1;

	case LIBNORMALFORM_VARIABLE:
	case LIBNORMALFORM_NEGATED_VARIABLE:
		if (flags & (LIBNORMALFORM_ELIMINATE_VARIABLE << (this->type - LIBNORMALFORM_VARIABLE)))
			return 0;
		this->type ^= LIBNORMALFORM_VARIABLE ^ LIBNORMALFORM_NEGATED_VARIABLE;
		return 1;

	case LIBNORMALFORM_FOR_ONE:
	case LIBNORMALFORM_NEGATED_FOR_ONE:
		if (flags & (LIBNORMALFORM_ELIMINATE_FOR_ONE << (this->type - LIBNORMALFORM_FOR_ONE)))
			return 0;
		this->type ^= LIBNORMALFORM_FOR_ONE ^LIBNORMALFORM_NEGATED_FOR_ONE;
		return 1;

	case LIBNORMALFORM_EXCLUSIVE_DISJUNCTION: /* disallowed since we only is this for CDNF */
	case LIBNORMALFORM_CONJUNCTION: /* disallowed since we only is this for CDNF */
	default:
		abort();
	}
}


/**
 * Convert from DNF to CDNF
 * 
 * @param   this   The DNF to convert to CDNF (in place)
 * @param   flags  Flags from `libnormalform_express`
 * @return         0 on success, -1 on failure
 */
static int
canonicalise_dnf(struct expression *this, uint64_t flags)
{
	struct expression *clause, *new_clause, *term, *nested_term;
	struct expression *positive = NULL, **req_positives = NULL;
	struct expression *negative = NULL, **req_negatives = NULL;
	struct expression *have, **want, **req_unsigneds = NULL;
	size_t clause_i, term_i, req_i, req_n = 0, req_size, i, max;
	int cmp, ret = -1, r;
	void *new, *tmp;

	if (this->type != LIBNORMALFORM_DISJUNCTION)
		abort();

	max = 0;
	for (clause_i = 0; clause_i < this->nterms; clause_i++) {
		clause = this->terms[clause_i];
		if (clause->type != LIBNORMALFORM_CONJUNCTION)
			abort();
		if (clause->nterms > max)
			max = clause->nterms;

		for (i = 0; i < clause->nterms; i++) {
			switch (clause->terms[i]->type) {
			case LIBNORMALFORM_TRANSFORMATION:
			case LIBNORMALFORM_VARIABLE:
			case LIBNORMALFORM_NEGATED_VARIABLE:
			case LIBNORMALFORM_FUNCTION:
			case LIBNORMALFORM_NEGATED_FUNCTION:
				break;

			case LIBNORMALFORM_FOR_ALL:
			case LIBNORMALFORM_NEGATED_FOR_ALL:
			case LIBNORMALFORM_FOR_ANY:
			case LIBNORMALFORM_NEGATED_FOR_ANY:
			case LIBNORMALFORM_FOR_ONE:
			case LIBNORMALFORM_NEGATED_FOR_ONE:
				if (canonicalise_dnf(clause->terms[i], flags))
					return -1;
				break;

			default:
			case LIBNORMALFORM_CONJUNCTION:
			case LIBNORMALFORM_DISJUNCTION:
			case LIBNORMALFORM_EXCLUSIVE_DISJUNCTION:
				abort();
			}
		}

		qsort(clause->terms, clause->nterms, sizeof(*clause->terms), &libnormalform_literal_sort_cmp__);
	}
	req_size = max;
	req_positives = malloc(req_size * sizeof(*req_positives));
	if (!req_positives)
		goto fail;
	req_negatives = malloc(req_size * sizeof(*req_negatives));
	if (!req_negatives)
		goto fail;
	req_unsigneds = malloc(req_size * sizeof(*req_unsigneds));
	if (!req_unsigneds)
		goto fail;
	for (clause_i = 0; clause_i < this->nterms; clause_i++) {
		clause = this->terms[clause_i];
		req_i = 0;
		for (term_i = 0; term_i < clause->nterms; term_i++) {
			term = clause->terms[term_i];
		req_again:
			if (req_i == req_n) {
			req_new:
				if (req_n == req_size) {
					req_size += 64;
					new = realloc(req_positives, req_size * sizeof(*req_positives));
					if (!new)
						goto fail;
					req_positives = new;
					req_negatives = realloc(req_negatives, req_size * sizeof(*req_negatives));
					if (!new)
						goto fail;
					req_negatives = new;
					req_unsigneds = realloc(req_unsigneds, req_size * sizeof(*req_unsigneds));
					if (!new)
						goto fail;
					req_unsigneds = new;
				}
				memmove(&req_positives[req_i + 1U], &req_positives[req_i], (req_n - req_i) * sizeof(*req_positives));
				memmove(&req_negatives[req_i + 1U], &req_negatives[req_i], (req_n - req_i) * sizeof(*req_negatives));
				memmove(&req_unsigneds[req_i + 1U], &req_unsigneds[req_i], (req_n - req_i) * sizeof(*req_unsigneds));
				req_positives[req_i] = NULL;
				req_negatives[req_i] = NULL;
				req_unsigneds[req_i] = NULL;
				req_n += 1;
				nested_term = term;
			positivity_again:
				switch (nested_term->type) {
				case LIBNORMALFORM_TRANSFORMATION:
					nested_term = nested_term->terms[0];
					goto positivity_again;
				case LIBNORMALFORM_FUNCTION:
				case LIBNORMALFORM_VARIABLE:
				case LIBNORMALFORM_FOR_ONE:
					req_positives[req_i] = term;
					req_positives[req_i]->refcount += 1;
					break;
				case LIBNORMALFORM_NEGATED_FUNCTION:
				case LIBNORMALFORM_NEGATED_VARIABLE:
				case LIBNORMALFORM_NEGATED_FOR_ONE:
					req_negatives[req_i] = term;
					req_negatives[req_i]->refcount += 1;
					break;
				case LIBNORMALFORM_FOR_ALL:
				case LIBNORMALFORM_NEGATED_FOR_ALL:
				case LIBNORMALFORM_FOR_ANY:
				case LIBNORMALFORM_NEGATED_FOR_ANY:
					req_unsigneds[req_i] = term;
					req_unsigneds[req_i]->refcount += 1;
					break;
				default:
				case LIBNORMALFORM_CONJUNCTION:
				case LIBNORMALFORM_DISJUNCTION:
				case LIBNORMALFORM_EXCLUSIVE_DISJUNCTION:
					abort();
				}
			} else if (req_positives[req_i]) {
				cmp = libnormalform_literal_cmp__(term, req_positives[req_i]);
				if (cmp < -1) {
					goto req_new;
				} else if (cmp == -1) {
					abort();
				} else if (cmp == +1) {
					if (!req_negatives[req_i]) {
						req_negatives[req_i] = term;
						term->refcount += 1;
					}
				} else if (cmp > +1) {
					req_i++;
					goto req_again;
				} else {
					libnormalform_free_expression__(term);
					clause->terms[term_i] = req_positives[req_i];
				}
			} else if (req_negatives[req_i]) {
				cmp = libnormalform_literal_cmp__(term, req_negatives[req_i]);
				if (cmp < -1) {
					goto req_new;
				} else if (cmp == -1) {
					req_positives[req_i] = term;
					term->refcount += 1;
				} else if (cmp == +1) {
					abort();
				} else if (cmp > +1) {
					req_i++;
					goto req_again;
				} else {
					libnormalform_free_expression__(term);
					clause->terms[term_i] = req_negatives[req_i];
				}
			} else if (req_unsigneds[req_i]) {
				cmp = libnormalform_literal_cmp__(term, req_unsigneds[req_i]);
				if (cmp < -1) {
					goto req_new;
				} else if (cmp == -1) {
					req_positives[req_i] = term;
					term->refcount += 1;
					req_negatives[req_i] = req_unsigneds[req_i];
					req_unsigneds[req_i] = NULL;
				} else if (cmp == +1) {
					req_negatives[req_i] = term;
					term->refcount += 1;
					req_positives[req_i] = req_unsigneds[req_i];
					req_unsigneds[req_i] = NULL;
				} else if (cmp > +1) {
					req_i++;
					goto req_again;
				} else {
					libnormalform_free_expression__(term);
					clause->terms[term_i] = req_unsigneds[req_i];
				}
			} else {
				abort();
			}
		}
	}
	qsort(this->terms, this->nterms, sizeof(*this->terms), &libnormalform_clause_sort_cmp__);

	clause_i = 0;
again:
	for (; clause_i < this->nterms; clause_i++) {
		clause = this->terms[clause_i];

		if (clause->nterms < req_n) {
			new = realloc(clause->terms, req_n * sizeof(*clause->terms));
			if (!new)
				goto fail;
			clause->terms = new;
		}

		for (term_i = req_i = 0; req_i < req_n; term_i++, req_i++) {
			positive = req_positives[req_i];
			negative = req_negatives[req_i];
			have = positive ? positive : negative;
			have = have ? have : req_unsigneds[req_i];
			if (!have) {
				/* TODO (elimination) */
			}

			if (term_i < clause->nterms) {
				cmp = libnormalform_literal_cmp__(have, clause->terms[term_i]);
				if (cmp >= -1) {
					if (cmp > +1)
						abort();
					continue;
				}
			}

			if (!positive && !negative) {
				positive = have;
				negative = malloc(sizeof(*negative));
				*negative = *positive;
				negative->refcount = 1;
				negative->terms = malloc(negative->nterms * sizeof(*negative->terms));
				if (!negative->terms) {
					free(negative);
					goto fail;
				}
				for (i = 0; i < negative->nterms; i++) {
					negative->terms[i] = positive->terms[i];
					negative->terms[i]->refcount += 1;
				}
				req_positives[req_i] = positive;
				req_negatives[req_i] = negative;
				req_unsigneds[req_i] = NULL;
				r = perfectly_invert_expression(negative, flags);
				if (r < 0)
					goto fail;
				if (!r) {
				eliminate_term:
					libnormalform_free_expression__(req_positives[req_i]);
					libnormalform_free_expression__(req_negatives[req_i]);
					req_positives[req_i] = NULL;
					req_negatives[req_i] = NULL;
					/* TODO (elimination)
					 * the term as to be eliminated, and the clause may have
					 * to be moved down (and potentially eliminated)
					 */
				}
				cmp = libnormalform_literal_cmp__(positive, negative);
				if (cmp == +1) {
					tmp = positive, positive = negative, negative = tmp;
					req_positives[req_i] = positive;
					req_negatives[req_i] = negative;
				} else if (cmp != -1) {
					abort();
				}
			} else if (!positive || !negative) {
				want = positive ? &positive : &negative;
				*want = malloc(sizeof(**want));
				**want = *have;
				(*want)->refcount = 1;
				(*want)->terms = malloc(have->nterms * sizeof(*have->terms));
				if (!(*want)->terms) {
					free(*want);
					goto fail;
				}
				for (i = 0; i < have->nterms; i++) {
					(*want)->terms[i] = have->terms[i];
					(*want)->terms[i]->refcount += 1;
				}
				r = perfectly_invert_expression(*want, flags);
				if (r < 0)
					goto fail;
				if (!r)
					goto eliminate_term;
			}

			memmove(&clause->terms[term_i + 1U], &clause->terms[term_i],
			        (clause->nterms++ - term_i) * sizeof(*clause->terms));

			clause->terms[term_i] = negative;
			if (libnormalform_contains_clause__(this, clause, clause_i)) {
				libnormalform_free_expression__(negative);
				negative = NULL;
			}

			clause->terms[term_i] = positive;
			if (libnormalform_contains_clause__(this, clause, clause_i)) {
				libnormalform_free_expression__(positive);
				positive = NULL;
			}

			if (positive) {
				clause->terms[term_i] = positive;
				if (!negative)
					continue;
			} else if (negative) {
				clause->terms[term_i] = negative;
				continue;
			} else {
				libnormalform_free_expression__(clause);
				memmove(&this->terms[clause_i], &this->terms[clause_i + 1U],
					(--clause->nterms - clause_i) * sizeof(*clause->terms));
				goto again;
			}

			new_clause = malloc(sizeof(*new_clause));
			if (!new_clause) {
				libnormalform_free_expression__(negative);
				goto fail;
			}
			*new_clause = *clause;
			new_clause->refcount = 1;
			new_clause->terms = malloc(new_clause->nterms * sizeof(*new_clause->terms));
			if (!new_clause->terms) {
				libnormalform_free_expression__(negative);
				free(new_clause);
				goto fail;
			}
			for (i = 0; i < new_clause->nterms; i++) {
				new_clause->terms[i] = clause->terms[i];
				new_clause->terms[i]->refcount += 1;
			}

			new_clause->terms[term_i]->refcount -= 1;
			new_clause->terms[term_i] = negative;

			new = realloc(this->terms, (this->nterms + 1U) * sizeof(*this->terms));
			if (!new) {
				libnormalform_free_expression__(new_clause);
				goto fail;
			}
			this->terms = new;
			memmove(&this->terms[clause_i + 1U], &this->terms[clause_i],
			        (this->nterms++ - clause_i) * sizeof(*this->terms));
			this->terms[clause_i] = new_clause;
		}
		if (term_i != clause->nterms)
			abort();
	}

	ret = 0;
fail:
	if (req_positives) {
		for (i = 0; i < req_n; i++)
			if (req_positives[i])
				libnormalform_free_expression__(req_positives[i]);
		free(req_positives);
	}
	if (req_negatives) {
		for (i = 0; i < req_n; i++)
			if (req_positives[i])
				libnormalform_free_expression__(req_positives[i]);
		free(req_positives);
	}
	if (req_unsigneds) {
		for (i = 0; i < req_n; i++)
			if (req_unsigneds[i])
				libnormalform_free_expression__(req_unsigneds[i]);
		free(req_unsigneds);
	}
	return ret;
}


struct libnormalform_term *
(libnormalform_cdnf)(LIBNORMALFORM_SENTENCE *this, uint64_t flags, const struct libnormalform_analysers *analysers)
{
	return libnormalform_express__(this, flags | LIBNORMALFORM_RELAX_XOR, analysers, DNF, &canonicalise_dnf);
}


#else

TODO_TEST

#endif