1 files changed, 1 insertions, 833 deletions

diff --git a/libnormalform_express.c b/libnormalform_express.c
index 2532488..25c4d7c 100644
--- a/libnormalform_express.c
+++ b/libnormalform_express.c
@@ -3,842 +3,10 @@
 #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;
+	return libnormalform_express__(this, flags, analysers, NNF, NULL);
 }