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

/* TODO implement LIBNORMALFORM_DISTRIBUTE_QUALIFIERS */


/**
 * Convert a sentence of the type `LIBNORMALFORM_SENTENCE *`
 * to the temporary type `struct expression *`
 * 
 * This function will flatten the sentence so that no
 * clause contains terms, that are direct children and,
 * that are clauses using the same connective
 * 
 * Literals and qualifiers cannot be represented will
 * be removed, and any application-provided relaxation
 * will be applied
 *
 * The flags `LIBNORMALFORM_RELAX_XOR` and
 * `LIBNORMALFORM_REDUCE_XOR` will be applied
 * 
 * @param   this   The sentence to convert
 * @param   flags  Flags from `libnormalform_express`
 * @return         An sentence is at least as true as `this`,
 *                 using the reductions and rewrites mentions,
 *                 above expressed in the temporary type;
 *                 `NULL` on failure
 */
static struct expression *
sentence_to_expression(LIBNORMALFORM_SENTENCE *this, uint64_t flags)
{
	LIBNORMALFORM_SENTENCE *left, *right, *free1 = NULL, *free2 = NULL;
	struct expression *ret, *sub;

	ret = malloc(sizeof(*ret));
	if (!ret)
		return NULL;
	*ret = EXPRESSION_INIT(0);

	switch (this->type) {
	case TYPE_TRUE:
	tautology:
		ret->type = LIBNORMALFORM_CONJUNCTION;
		goto out;

	case TYPE_FALSE:
	contradiction:
		ret->type = LIBNORMALFORM_DISJUNCTION;
		goto out;

	case TYPE_XOR:
		if (flags & LIBNORMALFORM_RELAX_XOR)
			goto inclusive_disjunction;
		if (flags & LIBNORMALFORM_REDUCE_XOR) {
			/* x ⊕ y = (x ∨ y) ∧ ¬(x ∧ y) = (x ∨ y) ∧ (¬x ∨ ¬y) */
			free1 = left = libnormalform_or2(libnormalform_ref(LEFT(this)), libnormalform_ref(RIGHT(this)));
			free2 = right = libnormalform_or2(LEFT(this)->inverse(LEFT(this)), RIGHT(this)->inverse(RIGHT(this)));
			if (!left || !right)
				goto fail;
			ret->type = LIBNORMALFORM_CONJUNCTION;
			goto clause_prefetched_branches;
		}
		ret->type = LIBNORMALFORM_EXCLUSIVE_DISJUNCTION;
		goto clause;
	case TYPE_AND:
		ret->type = LIBNORMALFORM_CONJUNCTION;
		goto clause;
	case TYPE_OR:
	inclusive_disjunction:
		ret->type = LIBNORMALFORM_DISJUNCTION;
	clause:
		left = LEFT(this);
		right = RIGHT(this);
	clause_prefetched_branches:
		sub = sentence_to_expression(left, flags);
		if (sub)
			goto fail;
		if (sub->type == ret->type) {
			free(ret);
			ret = sub;
		} else if (!sub->nterms && ret->type == LIBNORMALFORM_CONJUNCTION && sub->type == LIBNORMALFORM_DISJUNCTION) {
			/* ⋀(X ∪ {⋁∅}) = ⋀(X ∪ {⊥}) = ⋀X ∧ ⊥ = ⊥ */
			if (!sub->reduced) {
				libnormalform_free_expression__(sub);
				goto contradiction;
			}
			libnormalform_free_expression__(sub);
			ret->reduced |= 1;
		} else if (!sub->nterms && ret->type == LIBNORMALFORM_DISJUNCTION && sub->type == LIBNORMALFORM_CONJUNCTION) {
			/* ⋁(X ∪ {⋀∅}) = ⋁(X ∪ {⊤}) = ⋁X ∨ ⊤ = ⊤ */
			libnormalform_free_expression__(ret);
			ret = sub;
			goto tautology;
		} else {
			ret->terms = malloc(sizeof(*ret->terms));
			if (!ret->terms) {
				libnormalform_free_expression__(sub);
				goto fail;
			}
			ret->nterms = 1;
			ret->terms[0] = sub;
		}
		sub = sentence_to_expression(right, flags);
		if (sub)
			goto fail;
		if (sub->type == ret->type) {
			void *new = realloc(ret->terms, (ret->nterms + sub->nterms) * sizeof(*ret->terms));
			if (!new) {
				libnormalform_free_expression__(sub);
				goto fail;
			}
			ret->terms = new;
			memcpy(&ret->terms[ret->nterms], sub->terms, sub->nterms * sizeof(sub->terms));
			ret->nterms += sub->nterms;
			free(sub->terms);
			free(sub);
		} else if (!sub->nterms && ret->type == LIBNORMALFORM_CONJUNCTION && sub->type == LIBNORMALFORM_DISJUNCTION) {
			/* ⋀(X ∪ {⋁∅}) = ⋀(X ∪ {⊥}) = ⋀X ∧ ⊥ = ⊥ */
			if (!sub->reduced) {
				libnormalform_free_expression__(sub);
				goto contradiction;
			}
			libnormalform_free_expression__(sub);
			ret->reduced |= 1;
		} else if (!sub->nterms && ret->type == LIBNORMALFORM_DISJUNCTION && sub->type == LIBNORMALFORM_CONJUNCTION) {
			/* ⋁(X ∪ {⋀∅}) = ⋁(X ∪ {⊤}) = ⋁X ∨ ⊤ = ⊤ */
			libnormalform_free_expression__(ret);
			ret = sub;
			goto tautology;
		} else {
			void *new = realloc(ret->terms, (ret->nterms + 1U) * sizeof(*ret->terms));
			if (!new) {
				libnormalform_free_expression__(sub);
				goto fail;
			}
			ret->terms = new;
			ret->terms[ret->nterms++] = sub;
		}
		break;

	case TYPE_ALL:
		ret->type = LIBNORMALFORM_FOR_ALL;
		goto qualifier;
	case TYPE_ANY:
		ret->type = LIBNORMALFORM_FOR_ANY;
		goto qualifier;
	case TYPE_ONE:
		ret->type = LIBNORMALFORM_FOR_ONE;
		goto qualifier;
	case TYPE_NOT_ONE:
		ret->type = LIBNORMALFORM_NEGATED_FOR_ONE;
	qualifier:
		ret->user_item = this->data.qualifier.domain;
		ret->nterms = 2;
		ret->terms = malloc(2 * sizeof(*ret->terms));
		if (!ret->terms)
			goto fail;
		ret->terms[0] = sentence_to_expression(this->data.qualifier.antecedent, flags);
		if (!ret->terms[0])
			goto fail;
		ret->terms[1] = sentence_to_expression(this->data.qualifier.predicate, flags);
		if (!ret->terms[1])
			goto fail;
		break;

	case TYPE_VARIABLE:
		if ((flags & LIBNORMALFORM_ELIMINATE_VARIABLE) && (flags & LIBNORMALFORM_ELIMINATE_NEGATED_VARIABLE))
			goto eliminated;
		ret->user_item = this->data.literal.atom.variable;
		ret->type = LIBNORMALFORM_VARIABLE + (enum libnormalform_term_type)this->data.literal.inverted;
		break;

	case TYPE_FUNCTION:
		if ((flags & LIBNORMALFORM_ELIMINATE_FUNCTION) && (flags & LIBNORMALFORM_ELIMINATE_NEGATED_FUNCTION))
			goto eliminated;
		ret->reduced = !!this->data.literal.atom.function->requires_relaxation;
		if (!ret->reduced)
			ret->user_item = this->data.literal.atom.function;
		else if (this->data.literal.atom.function->relaxation)
			ret->user_item = this->data.literal.atom.function->relaxation;
		else
			goto eliminated;
		ret->type = LIBNORMALFORM_FUNCTION + (enum libnormalform_term_type)this->data.literal.inverted;
		break;

	case TYPE_TRANS:
		if (this->data.trans.function->requires_elimination)
			goto eliminated;
		ret->type = LIBNORMALFORM_TRANSFORMATION;
		ret->user_item = this->data.trans.function;
		ret->terms = malloc(sizeof(*ret->terms));
		if (ret->terms)
			goto fail;
		ret->terms[0] = sentence_to_expression(this->data.trans.input, flags);
		if (!ret->terms[0])
			goto fail;
		break;

	default:
		abort();
	}

	goto out;

eliminated:
	ret->reduced = 1;
	ret->type = LIBNORMALFORM_CONJUNCTION;
out:
	libnormalform_free(free1);
	libnormalform_free(free2);
	return ret;

fail:
	libnormalform_free(free1);
	libnormalform_free(free2);
	libnormalform_free_expression__(ret);
	return NULL;
}



/**
 * Reduce a sentence as much as possible keeping it logically equivalent
 *
 * All objects must have a reference count of 1
 * 
 * @param   this       The sentence to reduce (in place)
 * @param   analysers  Application-provided analysis functions, or `NULL`
 * @return             0 on success, -1 on failure
 */
static int
reduce_expression(struct expression *this, const struct libnormalform_analysers *analysers)
{
	enum libnormalform_sentence_relationship relationship;
	struct expression *new;
	size_t i, j;

	for (i = 0; i < this->nterms; i++)
		if (reduce_expression(this->terms[i], analysers))
			return -1;

	switch (this->type) {
	case LIBNORMALFORM_CONJUNCTION:
		for (i = 0; i < this->nterms; i++) {
		left_eliminated_conjunction:
			for (j = i + 1; j < this->nterms; j++) {
				if (libnormalform_get_relationship__(this->terms[i], this->terms[j], analysers, &relationship))
					return -1;
				switch (relationship) {
				case LIBNORMALFORM_MATERIAL_IMPLICATION:
				case LIBNORMALFORM_IDENTICAL:
					libnormalform_free_expression__(this->terms[j]);
					this->terms[j--] = this->terms[--this->nterms];
					break;
				case LIBNORMALFORM_CONVERSE_IMPLICATION:
					libnormalform_free_expression__(this->terms[i]);
					this->terms[i--] = this->terms[--this->nterms];
					goto left_eliminated_conjunction;
				case LIBNORMALFORM_MUTUALLY_INVERSE:
				case LIBNORMALFORM_MUTUALLY_EXCLUSIVE:
					goto contradiction;
				case LIBNORMALFORM_JOINTLY_UNDENIABLE:
				case LIBNORMALFORM_MUTUALLY_INDEPENDENT:
				default:
					break;
				}
			}
		}
		break;
	contradiction:
		for (i = 0; i < this->nterms; i++)
			libnormalform_free_expression__(this->terms[i]);
		free(this->terms);
		this->terms = NULL;
		this->nterms = 0;
		this->type = LIBNORMALFORM_DISJUNCTION;
		break;

	case LIBNORMALFORM_DISJUNCTION:
		for (i = 0; i < this->nterms; i++) {
		left_eliminated_disjunction:
			for (j = i + 1; j < this->nterms; j++) {
				if (libnormalform_get_relationship__(this->terms[i], this->terms[j], analysers, &relationship))
					return -1;
				switch (relationship) {
				case LIBNORMALFORM_IDENTICAL:
				case LIBNORMALFORM_CONVERSE_IMPLICATION:
					libnormalform_free_expression__(this->terms[j]);
					this->terms[j--] = this->terms[--this->nterms];
					break;
				case LIBNORMALFORM_MATERIAL_IMPLICATION:
					libnormalform_free_expression__(this->terms[i]);
					this->terms[i--] = this->terms[--this->nterms];
					goto left_eliminated_disjunction;
				case LIBNORMALFORM_MUTUALLY_INVERSE:
				case LIBNORMALFORM_JOINTLY_UNDENIABLE:
					goto tautology;
				case LIBNORMALFORM_MUTUALLY_EXCLUSIVE:
				case LIBNORMALFORM_MUTUALLY_INDEPENDENT:
				default:
					break;
				}
			}
		}
		break;
	tautology:
		for (i = 0; i < this->nterms; i++)
			libnormalform_free_expression__(this->terms[i]);
		free(this->terms);
		this->terms = NULL;
		this->nterms = 0;
		this->type = LIBNORMALFORM_CONJUNCTION;
		break;

	case LIBNORMALFORM_EXCLUSIVE_DISJUNCTION:
		i = 0;
	both_eliminated_exclusive_disjunction:
		for (; i < this->nterms; i++) {
			for (j = i + 1; j < this->nterms; j++) {
				if (libnormalform_get_relationship__(this->terms[i], this->terms[j], analysers, &relationship))
					return -1;
				switch (relationship) {
				case LIBNORMALFORM_MATERIAL_IMPLICATION:
					new = libnormalform_make_binary__(1, this->terms[i], 0, this->terms[j],
					                                  LIBNORMALFORM_CONJUNCTION);
					if (!new)
						return -1;
					goto xor_reduced;
				case LIBNORMALFORM_CONVERSE_IMPLICATION:
					new = libnormalform_make_binary__(0, this->terms[i], 1, this->terms[j],
					                                  LIBNORMALFORM_CONJUNCTION);
					if (!new)
						return -1;
					goto xor_reduced;
				case LIBNORMALFORM_MUTUALLY_INVERSE:
					this->invert ^= 1;
					/* fall through */
				case LIBNORMALFORM_IDENTICAL:
					libnormalform_free_expression__(this->terms[i]);
					libnormalform_free_expression__(this->terms[j]);
					this->terms[i--] = this->terms[--this->nterms];
					this->terms[j--] = this->terms[--this->nterms];
					goto both_eliminated_exclusive_disjunction;
				case LIBNORMALFORM_MUTUALLY_EXCLUSIVE:
					new = libnormalform_make_binary__(0, this->terms[i], 0, this->terms[j],
					                                  LIBNORMALFORM_DISJUNCTION);
					if (!new)
						return -1;
					goto xor_reduced;
				case LIBNORMALFORM_JOINTLY_UNDENIABLE:
					new = libnormalform_make_binary__(1, this->terms[i], 1, this->terms[j],
					                                  LIBNORMALFORM_DISJUNCTION);
					if (!new)
						return -1;
					goto xor_reduced;
				case LIBNORMALFORM_MUTUALLY_INDEPENDENT:
				default:
					break;
				xor_reduced:
					libnormalform_free_expression__(this->terms[i]);
					libnormalform_free_expression__(this->terms[j]);
					this->terms[j--] = this->terms[--this->nterms];
					this->terms[i] = new;
					goto both_eliminated_exclusive_disjunction;
				}
			}
		}
		if (!this->nterms) {
			if (this->invert) {
				this->invert = 0;
				this->type = LIBNORMALFORM_CONJUNCTION;
			} else {
				this->type = LIBNORMALFORM_DISJUNCTION;
			}
		}
		break;

	case LIBNORMALFORM_TRANSFORMATION:
	case LIBNORMALFORM_VARIABLE:
	case LIBNORMALFORM_NEGATED_VARIABLE:
	case LIBNORMALFORM_FUNCTION:
	case LIBNORMALFORM_NEGATED_FUNCTION:
	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:
	default:
		return 0;
	}

	if (this->nterms == 1) {
		new = this->terms[0];
		free(this->terms);
		new->invert ^= this->invert;
		*this = *new;
		free(new);
	}

	return 0;
}


struct libnormalform_term *
(libnormalform_express__)(LIBNORMALFORM_SENTENCE *this, uint64_t flags,
                          const struct libnormalform_analysers *analysers, enum normal_form form,
                          int (*canonicalise)(struct expression *this, uint64_t flags))
{
	struct libnormalform_term *ret;
	struct expression *expression;
	int reduced;

	if (flags & ~LIBNORMALFORM_ALL_EXPRESS_FLAGS__) {
		errno = EINVAL;
		return NULL;
	}

	/* just to be safe */
	if (flags & LIBNORMALFORM_REDUCE_XOR)
		flags |= LIBNORMALFORM_RELAX_XOR;
	if ((flags & LIBNORMALFORM_AVOID_FOR_ANY) && (flags & LIBNORMALFORM_AVOID_NEGATED_FOR_ALL))
		flags ^= LIBNORMALFORM_AVOID_FOR_ANY | LIBNORMALFORM_AVOID_NEGATED_FOR_ALL;
	if ((flags & LIBNORMALFORM_AVOID_FOR_ALL) && (flags & LIBNORMALFORM_AVOID_NEGATED_FOR_ANY))
		flags ^= LIBNORMALFORM_AVOID_FOR_ALL | LIBNORMALFORM_AVOID_NEGATED_FOR_ANY;

	(void) form; /* TODO respect form=={CNF,DNF} */
	expression = sentence_to_expression(this, flags);
	if (!expression)
		return NULL;
	do {
		if (reduce_expression(expression, analysers)) {
			libnormalform_free_expression__(expression);
			return NULL;
		}
		reduced = 0;
		if (libnormalform_fix_presentation__(expression, flags, &(unsigned char){0}, &reduced)) {
			libnormalform_free_expression__(expression);
			return NULL;
		}
	} while (reduced);

	if (canonicalise) {
		if ((*canonicalise)(expression, flags)) {
			libnormalform_free_expression__(expression);
			return NULL;
		}
	}

	ret = malloc(sizeof(*ret));
	if (!ret) {
		libnormalform_free_expression__(expression);
		return NULL;
	}
	if (libnormalform_expression_to_term__(ret, expression)) {
#if defined(__GNUC__) && !defined(__clang__)
# pragma GCC diagnostic push
# pragma GCC diagnostic ignored "-Wmismatched-dealloc"
#endif
		libnormalform_free(ret);
		ret = NULL;
#if defined(__GNUC__) && !defined(__clang__)
# pragma GCC diagnostic pop
#endif
	}
	libnormalform_free_expression__(expression);

	return ret;
}


#else


CONST int
main(void)
{
	return 0; /* indirectly tested via libnormalform_{express,dnf,cnf,cdnf} */
}


#endif