Second commitHEADmaster

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

1 files changed, 313 insertions, 0 deletions

diff --git a/libnormalform_fix_presentation__.c b/libnormalform_fix_presentation__.c
new file mode 100644
index 0000000..8c0f4e0
--- /dev/null
+++ b/libnormalform_fix_presentation__.c
@@ -0,0 +1,313 @@
+/* See LICENSE file for copyright and license details. */
+#include "common.h"
+#ifndef TEST
+
+
+/**
+ * Check whether inverting a sentence would require
+ * it to be relaxes before it can be represented
+ *
+ * @param   this  The sentence to check
+ * @param   flags  Flags from `libnormalform_express`
+ * @return         1 if the inversion can be exactly represented,
+ *                 0 if the inversion requires relaxation be
+ */
+PURE static int
+inversion_would_relax(struct expression *this, uint64_t flags)
+{
+	size_t i;
+
+beginning:
+	switch (this->type) {
+	case LIBNORMALFORM_CONJUNCTION:
+	case LIBNORMALFORM_DISJUNCTION:
+		for (i = 0; i < this->nterms; i++)
+			if (inversion_would_relax(this->terms[i], flags))
+				return 1;
+		return 0;
+
+	case LIBNORMALFORM_EXCLUSIVE_DISJUNCTION:
+		for (i = 0; i < this->nterms; i++)
+			if (!inversion_would_relax(this->terms[i], flags))
+				return 0;
+		return 1;
+
+	case LIBNORMALFORM_VARIABLE:
+		return flags & LIBNORMALFORM_ELIMINATE_NEGATED_VARIABLE;
+
+	case LIBNORMALFORM_NEGATED_VARIABLE:
+		return flags & LIBNORMALFORM_ELIMINATE_VARIABLE;
+
+	case LIBNORMALFORM_FUNCTION:
+		return flags & LIBNORMALFORM_ELIMINATE_NEGATED_FUNCTION;
+
+	case LIBNORMALFORM_NEGATED_FUNCTION:
+		return flags & LIBNORMALFORM_ELIMINATE_FUNCTION;
+
+	case LIBNORMALFORM_TRANSFORMATION:
+		this = this->terms[0];
+		goto beginning;
+
+	case LIBNORMALFORM_FOR_ALL:
+		if (!(flags & LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ALL))
+			return 0;
+		if (flags & LIBNORMALFORM_ELIMINATE_FOR_ANY)
+			return 1;
+		this = this->terms[this->nterms - 1];
+		goto beginning;
+
+	case LIBNORMALFORM_NEGATED_FOR_ALL:
+		if (!(flags & LIBNORMALFORM_ELIMINATE_FOR_ALL))
+			return 0;
+		if (flags & LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ANY)
+			return 1;
+		this = this->terms[this->nterms - 1];
+		goto beginning;
+
+	case LIBNORMALFORM_FOR_ANY:
+		if (!(flags & LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ANY))
+			return 0;
+		if (flags & LIBNORMALFORM_ELIMINATE_FOR_ALL)
+			return 1;
+		this = this->terms[this->nterms - 1];
+		goto beginning;
+
+	case LIBNORMALFORM_NEGATED_FOR_ANY:
+		if (!(flags & LIBNORMALFORM_ELIMINATE_FOR_ANY))
+			return 0;
+		if (flags & LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ALL)
+			return 1;
+		this = this->terms[this->nterms - 1];
+		goto beginning;
+
+	case LIBNORMALFORM_FOR_ONE:
+		return flags & LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ONE;
+
+	case LIBNORMALFORM_NEGATED_FOR_ONE:
+		return flags & LIBNORMALFORM_ELIMINATE_FOR_ONE;
+
+	default:
+		abort();
+	}
+}
+
+
+int
+(libnormalform_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;
+	int may_switch = 1;
+
+	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) { /* TODO always? */
+			this->invert ^= 1;
+			*require_inversion = 0;
+		}
+		for (i = 0; i < this->nterms; i++)
+			if (libnormalform_fix_presentation__(this->terms[i], flags, &this->invert, reduced))
+				return -1;
+		if (this->invert) {
+			/* TODO this is not necessarily the best element to invert,
+			 *      possibly the previous loop could be used to determine
+			 *      which is best (notably, clauses are not analysed) */
+			this->invert = 0;
+			this->terms[0]->invert ^= 1;
+			if (libnormalform_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 for_all: if (WILL_ELIMINATE(FOR_ALL, this->invert)) {
+			if (!may_switch)
+				goto eliminate;
+			may_switch = 0;
+			this->invert = 0;
+			this->terms[this->nterms - 1]->invert ^= 1;
+			this->type = LIBNORMALFORM_NEGATED_FOR_ANY - (this->type - LIBNORMALFORM_FOR_ALL);
+			goto for_any;
+		}
+		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))) {
+			if (!inversion_would_relax(this, flags)) {
+				this->terms[this->nterms - 1]->invert ^= 1;
+				this->type = LIBNORMALFORM_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 for_any: if (WILL_ELIMINATE(FOR_ANY, this->invert)) {
+			if (!may_switch)
+				goto eliminate;
+			may_switch = 0;
+			this->invert = 0;
+			this->terms[this->nterms - 1]->invert ^= 1;
+			this->type = LIBNORMALFORM_NEGATED_FOR_ALL - (this->type - LIBNORMALFORM_FOR_ANY);
+			goto for_all;
+		}
+		this->type ^= (LIBNORMALFORM_FOR_ANY ^ LIBNORMALFORM_NEGATED_FOR_ANY) * this->invert;
+		this->invert = 0;
+		if (flags & (LIBNORMALFORM_AVOID_FOR_ANY << (this->type - LIBNORMALFORM_FOR_ANY))) {
+			if (!inversion_would_relax(this, flags)) {
+				this->terms[this->nterms - 1]->invert ^= 1;
+				this->type = LIBNORMALFORM_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)) {
+			this->type ^= (LIBNORMALFORM_FOR_ONE ^ LIBNORMALFORM_NEGATED_FOR_ONE) * this->invert;
+			if (this->type == LIBNORMALFORM_FOR_ONE) {
+				this->invert = 0;
+				this->reduced = 1;
+				*reduced = 1;
+				goto for_any;
+			}
+			goto eliminate;
+		}
+		this->type ^= (LIBNORMALFORM_FOR_ONE ^ LIBNORMALFORM_NEGATED_FOR_ONE) * this->invert;
+		if (this->type == LIBNORMALFORM_FOR_ONE) {
+			if (flags & LIBNORMALFORM_ELIMINATE_FOR_ONE) {
+				this->type = LIBNORMALFORM_FOR_ANY;
+				this->invert = 0;
+				this->reduced = 1;
+				*reduced = 1;
+				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 (libnormalform_fix_presentation__(this->terms[i], flags, require_inversion, reduced))
+			return -1;
+
+	return 0;
+
+eliminate:
+	*require_inversion = 0;
+	this->refcount = 1;
+	this->reduced = 1;
+	this->invert = 0;
+	while (this->nterms)
+		libnormalform_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 = libnormalform_make_binary__(1, this->terms[0], 0, this->terms[1], LIBNORMALFORM_DISJUNCTION);
+	goto join_sides;
+
+for_any_join_sides:
+	new = libnormalform_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 (libnormalform_apply_transformation__(this->terms[0]->terms[0], LIBNORMALFORM_DOMAIN_VIEW))
+		return -1;
+	if (libnormalform_apply_transformation__(this->terms[0]->terms[1], LIBNORMALFORM_IMAGE_VIEW))
+		return -1;
+	*reduced = 1;
+	return 0;
+
+#undef WILL_ELIMINATE
+}
+
+
+#else
+
+TODO_TEST
+
+#endif