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


struct expression {
	enum libnormalform_term_type type;
	unsigned char reduced;
	unsigned char invert;
	size_t nterms;
	struct expression **terms;
	void *user_item;
};


static enum libnormalform_sentences_relationship
get_relationship(struct expression *l, struct expression *r, const struct libnormalform_analysers *analysers) /* TODO */
{
	(void) l;
	(void) r;
	(void) analysers;
	return LIBNORMALFORM_MUTUALLY_INDEPENDENT;
}


static void
free_expression(struct expression *this)
{
	if (this->terms) {
		while (this->nterms)
			free_expression(this->terms[--this->nterms]);
		free(this->terms);
	}
	free(this);
}


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->reduced = 0;
	ret->invert = 0;
	ret->nterms = 0;
	ret->terms = NULL;
	ret->user_item = NULL;

	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_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:
		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) {
				free_expression(sub);
				goto contradiction;
			}
			free_expression(sub);
			ret->reduced |= 1;
		} else if (!sub->nterms && ret->type == LIBNORMALFORM_DISJUNCTION && sub->type == LIBNORMALFORM_CONJUNCTION) {
			/* ⋁(X ∪ {⋀∅}) = ⋁(X ∪ {⊤}) = ⋁X ∨ ⊤ = ⊤ */
			free_expression(ret);
			ret = sub;
			goto tautology;
		} else {
			ret->terms = malloc(sizeof(*ret->terms));
			if (!ret->terms) {
				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) {
				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) {
				free_expression(sub);
				goto contradiction;
			}
			free_expression(sub);
			ret->reduced |= 1;
		} else if (!sub->nterms && ret->type == LIBNORMALFORM_DISJUNCTION && sub->type == LIBNORMALFORM_CONJUNCTION) {
			/* ⋁(X ∪ {⋀∅}) = ⋁(X ∪ {⊤}) = ⋁X ∨ ⊤ = ⊤ */
			free_expression(ret);
			ret = sub;
			goto tautology;
		} else {
			void *new = realloc(ret->terms, (ret->nterms + 1U) * sizeof(*ret->terms));
			if (!new) {
				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 + 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 + 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);
	free_expression(ret);
	return NULL;
}


static struct expression *
make_binary(int invert_left, struct expression *left, int invert_right, struct expression *right, enum libnormalform_term_type type)
{
	struct expression *ret;
	ret = malloc(sizeof(*ret));
	if (!ret)
		return NULL;
	ret->type = type;
	ret->reduced = 0;
	ret->invert = 0;
	ret->user_item = NULL;
	ret->nterms = 0;
	ret->terms = malloc(2 * sizeof(*ret->terms));
	if (!ret->terms) {
		free(ret);
		return NULL;
	}
	(ret->terms[0] = left)->invert ^= (unsigned char)invert_left;
	(ret->terms[1] = right)->invert ^= (unsigned char)invert_right;
	return ret;
}


static int
reduce_expression(struct expression *this, const struct libnormalform_analysers *analysers)
{
	enum libnormalform_sentences_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++) {
				relationship = get_relationship(this->terms[i], this->terms[j], analysers);
				switch (relationship) {
				case LIBNORMALFORM_MATERIAL_IMPLICATION:
				case LIBNORMALFORM_IDENTICAL:
					free_expression(this->terms[j]);
					this->terms[j--] = this->terms[--this->nterms];
					break;
				case LIBNORMALFORM_CONVERSE_IMPLICATION:
					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++)
			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++) {
				relationship = get_relationship(this->terms[i], this->terms[j], analysers);
				switch (relationship) {
				case LIBNORMALFORM_IDENTICAL:
				case LIBNORMALFORM_CONVERSE_IMPLICATION:
					free_expression(this->terms[j]);
					this->terms[j--] = this->terms[--this->nterms];
					break;
				case LIBNORMALFORM_MATERIAL_IMPLICATION:
					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++)
			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++) {
				relationship = get_relationship(this->terms[i], this->terms[j], analysers);
				switch (relationship) {
				case LIBNORMALFORM_MATERIAL_IMPLICATION:
					new = make_binary(1, this->terms[i], 0, this->terms[j], LIBNORMALFORM_CONJUNCTION);
					if (!new)
						return -1;
					goto xor_reduced;
				case LIBNORMALFORM_CONVERSE_IMPLICATION:
					new = 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:
					free_expression(this->terms[i]);
					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 = make_binary(0, this->terms[i], 0, this->terms[j], LIBNORMALFORM_DISJUNCTION);
					if (!new)
						return -1;
					goto xor_reduced;
				case LIBNORMALFORM_JOINTLY_UNDENIABLE:
					new = 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:
					free_expression(this->terms[i]);
					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;
}


static void *
domain_view_transform(void *user_data, void *input)
{
	struct libnormalform_mapping *kvpair = input;
	(void) user_data;
	return kvpair->key;
}


static void *
image_view_transform(void *user_data, void *input)
{
	struct libnormalform_mapping *kvpair = input;
	(void) user_data;
	return kvpair->value;
}


static int
apply_transformation(struct expression *this, enum libnormalform_builtin_transformer transformer)
{
	/* Only .builtin is actually needed, but the others
	 * could be useful for debugging by the user */
	static struct libnormalform_transformer domain_view = {
		.transform = &domain_view_transform,
		.deallocate = NULL,
		.user_data = NULL,
		.identifier = "<builtin:domain-view>",
		.builtin = LIBNORMALFORM_DOMAIN_VIEW
	};
	static struct libnormalform_transformer image_view = {
		.transform = &image_view_transform,
		.deallocate = NULL,
		.user_data = NULL,
		.identifier = "<builtin:image-view>",
		.builtin = LIBNORMALFORM_IMAGE_VIEW
	};

	size_t i;
	struct expression *new, **term_singleton;

	switch (this->type) {
	case LIBNORMALFORM_CONJUNCTION:
	case LIBNORMALFORM_DISJUNCTION:
	case LIBNORMALFORM_EXCLUSIVE_DISJUNCTION:
		/* transformations are morphism */
		for (i = 0; i < this->nterms; i++)
			if (apply_transformation(this->terms[i], transformer))
				return -1;
		break;

	case LIBNORMALFORM_TRANSFORMATION:
	case LIBNORMALFORM_FUNCTION:
	case LIBNORMALFORM_NEGATED_FUNCTION:
		new = malloc(sizeof(*new));
		if (!new)
			return -1;
		term_singleton = malloc(sizeof(*term_singleton));
		if (!term_singleton) {
			free(new);
			return -1;
		}
		*new = *this;
		this->type = LIBNORMALFORM_TRANSFORMATION;
		this->reduced = 0;
		this->invert = 0;
		this->nterms = 1;
		this->terms = term_singleton;
		this->terms[0] = new;
		switch (transformer) {
		case LIBNORMALFORM_DOMAIN_VIEW:
			this->user_item = &domain_view;
			break;
		case LIBNORMALFORM_IMAGE_VIEW:
			this->user_item = &image_view;
			break;
		default:
		case LIBNORMALFORM_NOT_BUILT_IN:
			abort();
		}
		break;

	case LIBNORMALFORM_VARIABLE:
	case LIBNORMALFORM_NEGATED_VARIABLE:
		/* variables are input-independent leafs */
	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:
		/* qualifiers reset input */
	default:
		break;
	}

	return 0;
}


static int
fix_presentation(struct expression *this, uint64_t flags, unsigned char *require_inversion, int *reduced)
{
#define WILL_ELIMINATE(BASETYPE, INVERT)\
	(flags & (LIBNORMALFORM_ELIMINATE_##BASETYPE <<\
	          ((this->type ^ ((LIBNORMALFORM_##BASETYPE ^ LIBNORMALFORM_NEGATED_##BASETYPE) *\
	                          (INVERT))) -\
	           LIBNORMALFORM_##BASETYPE)))

	size_t i;
	unsigned char zero = 0;
	struct expression *new;

	switch (this->type) {
	case LIBNORMALFORM_CONJUNCTION:
	case LIBNORMALFORM_DISJUNCTION:
		this->type ^= LIBNORMALFORM_CONJUNCTION ^ LIBNORMALFORM_DISJUNCTION;
		if (this->invert) {
			if (*require_inversion) {
				this->invert ^= 1;
				*require_inversion = 0;
			}
			for (i = 0; i < this->nterms; i++)
				this->terms[i]->invert ^= 1;
		}
		require_inversion = &zero;
		break;

	case LIBNORMALFORM_EXCLUSIVE_DISJUNCTION:
		if (!this->nterms)
			abort();
		if (*require_inversion) {
			this->invert ^= 1;
			*require_inversion = 0;
		}
		if (flags & LIBNORMALFORM_ELIMINATE_XOR)
			goto eliminate;
		for (i = 0; i < this->nterms; i++)
			if (fix_presentation(this->terms[i], flags, &this->invert, reduced))
				return -1;
		if (this->invert) {
			this->invert = 0;
			this->terms[0]->invert ^= 1;
			if (fix_presentation(this->terms[0], flags, &zero, reduced))
				return -1;
		}
		return 0;

	case LIBNORMALFORM_VARIABLE:
	case LIBNORMALFORM_NEGATED_VARIABLE:
		if (!WILL_ELIMINATE(VARIABLE, this->invert ^ *require_inversion)) {
			this->invert ^= *require_inversion;
			*require_inversion = 0;
		} else if (WILL_ELIMINATE(VARIABLE, this->invert)) {
			goto eliminate;
		}
		this->type ^= (LIBNORMALFORM_VARIABLE ^ LIBNORMALFORM_NEGATED_VARIABLE) * this->invert;
		break;

	case LIBNORMALFORM_FUNCTION:
	case LIBNORMALFORM_NEGATED_FUNCTION:
		if (!WILL_ELIMINATE(FUNCTION, this->invert ^ *require_inversion)) {
			this->invert ^= *require_inversion;
			*require_inversion = 0;
		} else if (WILL_ELIMINATE(FUNCTION, this->invert)) {
			goto eliminate;
		}
		this->type ^= (LIBNORMALFORM_FUNCTION ^ LIBNORMALFORM_NEGATED_FUNCTION) * this->invert;
		break;

	case LIBNORMALFORM_TRANSFORMATION:
		this->terms[0]->invert ^= this->invert;
		break;

	case LIBNORMALFORM_FOR_ALL:
	case LIBNORMALFORM_NEGATED_FOR_ALL:
		if (!WILL_ELIMINATE(FOR_ALL, this->invert ^ *require_inversion)) {
			this->invert ^= *require_inversion;
			*require_inversion = 0;
		} else if (WILL_ELIMINATE(FOR_ALL, this->invert)) {
			goto eliminate;
		}
		this->type ^= (LIBNORMALFORM_FOR_ALL ^ LIBNORMALFORM_NEGATED_FOR_ALL) * this->invert;
		this->invert = 0;
		if (flags & (LIBNORMALFORM_AVOID_FOR_ALL << (this->type - LIBNORMALFORM_FOR_ALL))) {
			this->terms[this->nterms - 1]->invert ^= 1;
			this->type = LIBNORMALFORM_AVOID_NEGATED_FOR_ANY - (this->type - LIBNORMALFORM_FOR_ALL);
			goto for_any_maybe_join_sides;
		}
	for_all_maybe_join_sides:
		if (this->nterms > 1)
			break;
		if (flags & (LIBNORMALFORM_JOIN_SIDES_IN_FOR_ALL << (this->type - LIBNORMALFORM_FOR_ALL)))
			goto for_all_join_sides;
		break;

	case LIBNORMALFORM_FOR_ANY:
	case LIBNORMALFORM_NEGATED_FOR_ANY:
		if (!WILL_ELIMINATE(FOR_ANY, this->invert ^ *require_inversion)) {
			this->invert ^= *require_inversion;
			*require_inversion = 0;
		} else if (WILL_ELIMINATE(FOR_ANY, this->invert)) {
			goto eliminate;
		}
		this->type ^= (LIBNORMALFORM_FOR_ANY ^ LIBNORMALFORM_NEGATED_FOR_ANY) * this->invert;
	for_any:
		this->invert = 0;
		if (flags & (LIBNORMALFORM_AVOID_FOR_ANY << (this->type - LIBNORMALFORM_FOR_ANY))) {
			this->terms[this->nterms - 1]->invert ^= 1;
			this->type = LIBNORMALFORM_AVOID_NEGATED_FOR_ALL - (this->type - LIBNORMALFORM_FOR_ANY);
			goto for_all_maybe_join_sides;
		}
	for_any_maybe_join_sides:
		if (this->nterms > 1)
			break;
		if (flags & (LIBNORMALFORM_JOIN_SIDES_IN_FOR_ANY << (this->type - LIBNORMALFORM_FOR_ANY)))
			goto for_any_join_sides;
		break;

	case LIBNORMALFORM_FOR_ONE:
	case LIBNORMALFORM_NEGATED_FOR_ONE:
		if (!WILL_ELIMINATE(FOR_ONE, this->invert ^ *require_inversion)) {
			this->invert ^= *require_inversion;
			*require_inversion = 0;
		} else if (WILL_ELIMINATE(FOR_ONE, this->invert)) {
			goto eliminate;
		}
		this->type ^= (LIBNORMALFORM_FOR_ONE ^ LIBNORMALFORM_NEGATED_FOR_ONE) * this->invert;
		if (this->type == LIBNORMALFORM_FOR_ONE) {
			if (flags & LIBNORMALFORM_RELAX_FOR_ONE) {
				this->type = LIBNORMALFORM_FOR_ANY;
				goto for_any;
			}
		}
		if (this->nterms > 1)
			break;
		if (flags & (LIBNORMALFORM_JOIN_SIDES_IN_FOR_ONE << (this->type - LIBNORMALFORM_FOR_ONE)))
			goto for_any_join_sides;
		break;

	default:
		abort();
	}

	this->invert = 0;

	for (i = 0; i < this->nterms; i++)
		if (fix_presentation(this->terms[i], flags, require_inversion, reduced))
			return -1;

	return 0;

eliminate:
	*require_inversion = 0;
	this->reduced = 0;
	this->invert = 0;
	while (this->nterms)
		free_expression(this->terms[--this->nterms]);
	free(this->terms);
	this->terms = NULL;
	this->type = LIBNORMALFORM_CONJUNCTION;
	*reduced = 1;
	return 0;

for_all_join_sides:
	new = make_binary(1, this->terms[0], 0, this->terms[1], LIBNORMALFORM_DISJUNCTION);
	goto join_sides;

for_any_join_sides:
	new = make_binary(0, this->terms[0], 0, this->terms[1], LIBNORMALFORM_CONJUNCTION);
join_sides:
	if (!new)
		return -1;
	this->terms[0] = new;
	this->nterms--;
	if (apply_transformation(this->terms[0]->terms[0], LIBNORMALFORM_DOMAIN_VIEW))
		return -1;
	if (apply_transformation(this->terms[0]->terms[1], LIBNORMALFORM_IMAGE_VIEW))
		return -1;
	*reduced = 1;
	return 0;

#undef WILL_ELIMINATE
}


static int
expression_to_term(struct libnormalform_term *out, struct expression *this)
{
	size_t i;

	out->type = this->type;
	out->reduced = this->reduced;

	switch (this->type) {
	case LIBNORMALFORM_CONJUNCTION:
	case LIBNORMALFORM_DISJUNCTION:
	case LIBNORMALFORM_EXCLUSIVE_DISJUNCTION:
		out->term.clause.nterms = 0;
		out->term.clause.terms = calloc(this->nterms, sizeof(*out->term.clause.terms));
		if (!out->term.clause.terms)
			return -1;
		for (i = 0; i < this->nterms; i++)
			if (expression_to_term(&out->term.clause.terms[out->term.clause.nterms++], this->terms[i]))
				return -1;
		break;

	case LIBNORMALFORM_TRANSFORMATION:
		out->term.transformation.transformer = this->user_item;
		out->term.transformation.sentence = calloc(1, sizeof(*out->term.transformation.sentence));
		if (!out->term.transformation.sentence ||
		    expression_to_term(out->term.transformation.sentence, this->terms[0]))
			return -1;
		break;

	case LIBNORMALFORM_VARIABLE:
	case LIBNORMALFORM_NEGATED_VARIABLE:
		out->term.variable = this->user_item;
		break;

	case LIBNORMALFORM_FUNCTION:
	case LIBNORMALFORM_NEGATED_FUNCTION:
		out->term.function = this->user_item;
		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:
		out->term.qualification.map = this->user_item;
		if (this->nterms == 1) {
			out->term.qualification.antecedent = NULL;
			out->term.qualification.predicate = calloc(1, sizeof(*out->term.qualification.predicate));
			if (!out->term.qualification.predicate ||
			    expression_to_term(out->term.qualification.predicate, this->terms[0]))
				return -1;
		} else {
			out->term.qualification.antecedent = calloc(1, sizeof(*out->term.qualification.antecedent));
			if (!out->term.qualification.antecedent)
				return -1;
			out->term.qualification.predicate = calloc(1, sizeof(*out->term.qualification.predicate));
			if (!out->term.qualification.predicate ||
			    expression_to_term(out->term.qualification.antecedent, this->terms[0]) ||
			    expression_to_term(out->term.qualification.predicate, this->terms[1]))
				return -1;
		}
		break;

	default:
		abort();
	}

	return 0;
}


struct libnormalform_term *
(libnormalform_express)(LIBNORMALFORM_SENTENCE *this, uint64_t flags, const struct libnormalform_analysers *analysers)
{
	struct libnormalform_term *ret;
	struct expression *expression;
	int reduced;

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

	if (flags & LIBNORMALFORM_REDUCE_XOR)
		flags &= ~LIBNORMALFORM_ELIMINATE_XOR;
	if ((flags & LIBNORMALFORM_ELIMINATE_FOR_ANY) && (flags & LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ALL))
		flags &= ~LIBNORMALFORM_RELAX_FOR_ONE;
	if (flags & LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ALL)
		flags &= ~LIBNORMALFORM_AVOID_FOR_ANY;
	if (flags & LIBNORMALFORM_ELIMINATE_FOR_ALL)
		flags &= ~LIBNORMALFORM_AVOID_NEGATED_FOR_ANY;
	if (flags & LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ANY)
		flags &= ~LIBNORMALFORM_AVOID_FOR_ALL;
	if (flags & LIBNORMALFORM_ELIMINATE_FOR_ANY)
		flags &= ~LIBNORMALFORM_AVOID_NEGATED_FOR_ALL;
	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;

	expression = sentence_to_expression(this, flags);
	if (!expression)
		return NULL;
	do {
		if (reduce_expression(expression, analysers)) {
			free_expression(expression);
			return NULL;
		}
		reduced = 0;
		if (fix_presentation(expression, flags, &(unsigned char){0}, &reduced)) {
			free_expression(expression);
			return NULL;
		}
	} while (reduced);

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

	return ret;
}


#else

TODO_TEST

#endif