First commit

Signed-off-by: Mattias Andrée <maandree@kth.se>

1 files changed, 849 insertions, 0 deletions

diff --git a/libnormalform_express.c b/libnormalform_express.c
new file mode 100644
index 0000000..2532488
--- /dev/null
+++ b/libnormalform_express.c
@@ -0,0 +1,849 @@
+/* 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