Second commitHEADmaster

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

1 files changed, 483 insertions, 0 deletions

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