Second commitHEADmaster

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

1 files changed, 560 insertions, 0 deletions

diff --git a/libnormalform_cdnf.c b/libnormalform_cdnf.c
new file mode 100644
index 0000000..d846a45
--- /dev/null
+++ b/libnormalform_cdnf.c
@@ -0,0 +1,560 @@
+/* See LICENSE file for copyright and license details. */
+#include "common.h"
+#ifndef TEST
+
+
+static int canonicalise_dnf(struct expression *this, uint64_t flags);
+
+
+/**
+ * Invert a sentence in place, but
+ * require the result to be unrelaxed
+ * 
+ * The sentence may not contain XOR
+ * 
+ * @param   this   The sentence to invert (in place)
+ * @param   flags  Flags from `libnormalform_express`
+ * @return         1 on success, 0 if the inversion could not
+ *                 be representated without being relaxed,
+ *                 -1 on failure
+ * 
+ * In case the function returns 0 or -1, `this` may
+ * have been partially inverted
+ */
+static int
+perfectly_invert_expression(struct expression *this, uint64_t flags)
+{
+	struct expression **outer;
+	size_t i, j, k, ci, cn, nouter;
+	int r;
+
+beginning:
+	switch (this->type) {
+	case LIBNORMALFORM_TRANSFORMATION:
+		this = this->terms[0];
+		goto beginning;
+
+	case LIBNORMALFORM_DISJUNCTION:
+		/* ¬⋁{⋀{x | x ∈ X} | X ∈ Y} =
+		 * ⋀{¬⋀{x | x ∈ X} | X ∈ Y} =
+		 * ⋀{⋁{¬x | x ∈ X} | X ∈ Y} =
+		 * ⋁{¬x₁ ∧ … ∧ ¬xₙ | x₁ ∈ X₁, …, xₙ ∈ Xₙ, {X₁, …, Xₙ} = Y} */
+		outer = NULL;
+		nouter = 1U;
+		for (i = 0; i < this->nterms; i++) {
+			if (this->terms[i]->type != LIBNORMALFORM_CONJUNCTION)
+				abort(); /* this function is only used for CDNF */
+			if (!this->terms[i]->nterms) {
+				nouter = 0;
+				break;
+			}
+			if (this->terms[i]->nterms > SIZE_MAX / nouter) {
+				errno = ENOMEM;
+				return -1;
+			}
+			nouter *= this->terms[i]->nterms;
+		}
+		if (!nouter) {
+			for (i = 0; i < this->nterms; i++)
+				libnormalform_free_expression__(this->terms[i]);
+			free(this->terms);
+			this->terms = NULL;
+			this->nterms = 0;
+			return 0;
+		}
+		for (i = 0; i < this->nterms; i++) {
+			this->reduced |= this->terms[i]->reduced;
+			for (j = 0; j < this->terms[i]->nterms; j++)
+				this->terms[i]->terms[j]->invert = 1;
+		}
+		for (i = 0; i < this->nterms; i++) {
+			for (j = 0; j < this->terms[i]->nterms; j++) {
+				if (!this->terms[i]->terms[j]->invert)
+					continue;
+				this->terms[i]->terms[j]->invert = 0;
+				r = perfectly_invert_expression(this->terms[i]->terms[j], flags);
+				if (r <= 0)
+					return r;
+				if (nouter / this->terms[i]->nterms > SIZE_MAX - this->terms[i]->terms[j]->refcount) {
+					errno = ENOMEM;
+					return -1;
+				}
+			}
+		}
+		for (i = 0; i < nouter; i++) {
+			outer[i] = malloc(sizeof(*outer[i]));
+			if (!outer[i])
+				return -1;
+			outer[i]->type = LIBNORMALFORM_CONJUNCTION;
+			outer[i]->reduced = 0;
+			outer[i]->invert = 0;
+			outer[i]->refcount = 1;
+			outer[i]->user_item = NULL;
+			outer[i]->nterms = 0;
+			outer[i]->terms = NULL;
+			if (!this->nterms)
+				continue;
+			outer[i]->terms = malloc(this->nterms * sizeof(*outer[i]->terms));
+			if (!outer[i]->terms) {
+				free(outer[i]);
+				while (i--) {
+					free(outer[i]->terms);
+					free(outer[i]);
+				}
+				return -1;
+			}
+		}
+		cn = 1U;
+		for (i = this->nterms; i--;) {
+			for (k = 0; k < nouter;) {
+				for (j = 0; j < this->terms[i]->nterms; j++) {
+					this->terms[i]->terms[j]->refcount += cn;
+					for (ci = 0; ci < cn; ci++)
+						outer[k++]->terms[i] = this->terms[i]->terms[j];
+				}
+			}
+			cn *= this->terms[i]->nterms;
+			libnormalform_free_expression__(this->terms[i]);
+			this->nterms--;
+		}
+		free(this->terms);
+		this->terms = outer;
+		this->nterms = nouter;
+		return canonicalise_dnf(this, flags) ? -1 : 1;
+
+	case LIBNORMALFORM_FOR_ALL:
+	case LIBNORMALFORM_NEGATED_FOR_ALL:
+		if (!(flags & (LIBNORMALFORM_ELIMINATE_FOR_ALL << (this->type - LIBNORMALFORM_FOR_ALL)))) {
+			this->type ^= LIBNORMALFORM_FOR_ALL ^ LIBNORMALFORM_NEGATED_FOR_ALL;
+			return 1;
+		}
+		/* ¬∀x.φ = ∃x.¬φ */
+		if (flags & (LIBNORMALFORM_ELIMINATE_FOR_ANY << (this->type - LIBNORMALFORM_FOR_ALL)))
+			return 0;
+		this->type = LIBNORMALFORM_FOR_ANY + (this->type - LIBNORMALFORM_FOR_ALL);
+		this = this->terms[this->nterms - 1];
+		goto beginning;
+
+	case LIBNORMALFORM_FOR_ANY:
+	case LIBNORMALFORM_NEGATED_FOR_ANY:
+		if (!(flags & (LIBNORMALFORM_ELIMINATE_FOR_ANY << (this->type - LIBNORMALFORM_FOR_ANY)))) {
+			this->type ^= LIBNORMALFORM_FOR_ANY ^ LIBNORMALFORM_NEGATED_FOR_ANY;
+			return 1;
+		}
+		/* ¬∃x.φ = ∀x.¬φ */
+		if (flags & (LIBNORMALFORM_ELIMINATE_FOR_ALL << (this->type - LIBNORMALFORM_FOR_ANY)))
+			return 0;
+		this->type = LIBNORMALFORM_FOR_ALL + (this->type - LIBNORMALFORM_FOR_ANY);
+		this = this->terms[this->nterms - 1];
+		goto beginning;
+
+	case LIBNORMALFORM_FUNCTION:
+	case LIBNORMALFORM_NEGATED_FUNCTION:
+		if (flags & (LIBNORMALFORM_ELIMINATE_FUNCTION << (this->type - LIBNORMALFORM_FUNCTION)))
+			return 0;
+		this->type ^= LIBNORMALFORM_FUNCTION ^ LIBNORMALFORM_NEGATED_FUNCTION;
+		return 1;
+
+	case LIBNORMALFORM_VARIABLE:
+	case LIBNORMALFORM_NEGATED_VARIABLE:
+		if (flags & (LIBNORMALFORM_ELIMINATE_VARIABLE << (this->type - LIBNORMALFORM_VARIABLE)))
+			return 0;
+		this->type ^= LIBNORMALFORM_VARIABLE ^ LIBNORMALFORM_NEGATED_VARIABLE;
+		return 1;
+
+	case LIBNORMALFORM_FOR_ONE:
+	case LIBNORMALFORM_NEGATED_FOR_ONE:
+		if (flags & (LIBNORMALFORM_ELIMINATE_FOR_ONE << (this->type - LIBNORMALFORM_FOR_ONE)))
+			return 0;
+		this->type ^= LIBNORMALFORM_FOR_ONE ^LIBNORMALFORM_NEGATED_FOR_ONE;
+		return 1;
+
+	case LIBNORMALFORM_EXCLUSIVE_DISJUNCTION: /* disallowed since we only is this for CDNF */
+	case LIBNORMALFORM_CONJUNCTION: /* disallowed since we only is this for CDNF */
+	default:
+		abort();
+	}
+}
+
+
+/**
+ * Convert from DNF to CDNF
+ * 
+ * @param   this   The DNF to convert to CDNF (in place)
+ * @param   flags  Flags from `libnormalform_express`
+ * @return         0 on success, -1 on failure
+ */
+static int
+canonicalise_dnf(struct expression *this, uint64_t flags)
+{
+	struct expression *clause, *new_clause, *term, *nested_term;
+	struct expression *positive = NULL, **req_positives = NULL;
+	struct expression *negative = NULL, **req_negatives = NULL;
+	struct expression *have, **want, **req_unsigneds = NULL;
+	size_t clause_i, term_i, req_i, req_n = 0, req_size, i, max;
+	int cmp, ret = -1, r;
+	void *new, *tmp;
+
+	if (this->type != LIBNORMALFORM_DISJUNCTION)
+		abort();
+
+	max = 0;
+	for (clause_i = 0; clause_i < this->nterms; clause_i++) {
+		clause = this->terms[clause_i];
+		if (clause->type != LIBNORMALFORM_CONJUNCTION)
+			abort();
+		if (clause->nterms > max)
+			max = clause->nterms;
+
+		for (i = 0; i < clause->nterms; i++) {
+			switch (clause->terms[i]->type) {
+			case LIBNORMALFORM_TRANSFORMATION:
+			case LIBNORMALFORM_VARIABLE:
+			case LIBNORMALFORM_NEGATED_VARIABLE:
+			case LIBNORMALFORM_FUNCTION:
+			case LIBNORMALFORM_NEGATED_FUNCTION:
+				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:
+				if (canonicalise_dnf(clause->terms[i], flags))
+					return -1;
+				break;
+
+			default:
+			case LIBNORMALFORM_CONJUNCTION:
+			case LIBNORMALFORM_DISJUNCTION:
+			case LIBNORMALFORM_EXCLUSIVE_DISJUNCTION:
+				abort();
+			}
+		}
+
+		qsort(clause->terms, clause->nterms, sizeof(*clause->terms), &libnormalform_literal_sort_cmp__);
+	}
+	req_size = max;
+	req_positives = malloc(req_size * sizeof(*req_positives));
+	if (!req_positives)
+		goto fail;
+	req_negatives = malloc(req_size * sizeof(*req_negatives));
+	if (!req_negatives)
+		goto fail;
+	req_unsigneds = malloc(req_size * sizeof(*req_unsigneds));
+	if (!req_unsigneds)
+		goto fail;
+	for (clause_i = 0; clause_i < this->nterms; clause_i++) {
+		clause = this->terms[clause_i];
+		req_i = 0;
+		for (term_i = 0; term_i < clause->nterms; term_i++) {
+			term = clause->terms[term_i];
+		req_again:
+			if (req_i == req_n) {
+			req_new:
+				if (req_n == req_size) {
+					req_size += 64;
+					new = realloc(req_positives, req_size * sizeof(*req_positives));
+					if (!new)
+						goto fail;
+					req_positives = new;
+					req_negatives = realloc(req_negatives, req_size * sizeof(*req_negatives));
+					if (!new)
+						goto fail;
+					req_negatives = new;
+					req_unsigneds = realloc(req_unsigneds, req_size * sizeof(*req_unsigneds));
+					if (!new)
+						goto fail;
+					req_unsigneds = new;
+				}
+				memmove(&req_positives[req_i + 1U], &req_positives[req_i], (req_n - req_i) * sizeof(*req_positives));
+				memmove(&req_negatives[req_i + 1U], &req_negatives[req_i], (req_n - req_i) * sizeof(*req_negatives));
+				memmove(&req_unsigneds[req_i + 1U], &req_unsigneds[req_i], (req_n - req_i) * sizeof(*req_unsigneds));
+				req_positives[req_i] = NULL;
+				req_negatives[req_i] = NULL;
+				req_unsigneds[req_i] = NULL;
+				req_n += 1;
+				nested_term = term;
+			positivity_again:
+				switch (nested_term->type) {
+				case LIBNORMALFORM_TRANSFORMATION:
+					nested_term = nested_term->terms[0];
+					goto positivity_again;
+				case LIBNORMALFORM_FUNCTION:
+				case LIBNORMALFORM_VARIABLE:
+				case LIBNORMALFORM_FOR_ONE:
+					req_positives[req_i] = term;
+					req_positives[req_i]->refcount += 1;
+					break;
+				case LIBNORMALFORM_NEGATED_FUNCTION:
+				case LIBNORMALFORM_NEGATED_VARIABLE:
+				case LIBNORMALFORM_NEGATED_FOR_ONE:
+					req_negatives[req_i] = term;
+					req_negatives[req_i]->refcount += 1;
+					break;
+				case LIBNORMALFORM_FOR_ALL:
+				case LIBNORMALFORM_NEGATED_FOR_ALL:
+				case LIBNORMALFORM_FOR_ANY:
+				case LIBNORMALFORM_NEGATED_FOR_ANY:
+					req_unsigneds[req_i] = term;
+					req_unsigneds[req_i]->refcount += 1;
+					break;
+				default:
+				case LIBNORMALFORM_CONJUNCTION:
+				case LIBNORMALFORM_DISJUNCTION:
+				case LIBNORMALFORM_EXCLUSIVE_DISJUNCTION:
+					abort();
+				}
+			} else if (req_positives[req_i]) {
+				cmp = libnormalform_literal_cmp__(term, req_positives[req_i]);
+				if (cmp < -1) {
+					goto req_new;
+				} else if (cmp == -1) {
+					abort();
+				} else if (cmp == +1) {
+					if (!req_negatives[req_i]) {
+						req_negatives[req_i] = term;
+						term->refcount += 1;
+					}
+				} else if (cmp > +1) {
+					req_i++;
+					goto req_again;
+				} else {
+					libnormalform_free_expression__(term);
+					clause->terms[term_i] = req_positives[req_i];
+				}
+			} else if (req_negatives[req_i]) {
+				cmp = libnormalform_literal_cmp__(term, req_negatives[req_i]);
+				if (cmp < -1) {
+					goto req_new;
+				} else if (cmp == -1) {
+					req_positives[req_i] = term;
+					term->refcount += 1;
+				} else if (cmp == +1) {
+					abort();
+				} else if (cmp > +1) {
+					req_i++;
+					goto req_again;
+				} else {
+					libnormalform_free_expression__(term);
+					clause->terms[term_i] = req_negatives[req_i];
+				}
+			} else if (req_unsigneds[req_i]) {
+				cmp = libnormalform_literal_cmp__(term, req_unsigneds[req_i]);
+				if (cmp < -1) {
+					goto req_new;
+				} else if (cmp == -1) {
+					req_positives[req_i] = term;
+					term->refcount += 1;
+					req_negatives[req_i] = req_unsigneds[req_i];
+					req_unsigneds[req_i] = NULL;
+				} else if (cmp == +1) {
+					req_negatives[req_i] = term;
+					term->refcount += 1;
+					req_positives[req_i] = req_unsigneds[req_i];
+					req_unsigneds[req_i] = NULL;
+				} else if (cmp > +1) {
+					req_i++;
+					goto req_again;
+				} else {
+					libnormalform_free_expression__(term);
+					clause->terms[term_i] = req_unsigneds[req_i];
+				}
+			} else {
+				abort();
+			}
+		}
+	}
+	qsort(this->terms, this->nterms, sizeof(*this->terms), &libnormalform_clause_sort_cmp__);
+
+	clause_i = 0;
+again:
+	for (; clause_i < this->nterms; clause_i++) {
+		clause = this->terms[clause_i];
+
+		if (clause->nterms < req_n) {
+			new = realloc(clause->terms, req_n * sizeof(*clause->terms));
+			if (!new)
+				goto fail;
+			clause->terms = new;
+		}
+
+		for (term_i = req_i = 0; req_i < req_n; term_i++, req_i++) {
+			positive = req_positives[req_i];
+			negative = req_negatives[req_i];
+			have = positive ? positive : negative;
+			have = have ? have : req_unsigneds[req_i];
+			if (!have) {
+				/* TODO (elimination) */
+			}
+
+			if (term_i < clause->nterms) {
+				cmp = libnormalform_literal_cmp__(have, clause->terms[term_i]);
+				if (cmp >= -1) {
+					if (cmp > +1)
+						abort();
+					continue;
+				}
+			}
+
+			if (!positive && !negative) {
+				positive = have;
+				negative = malloc(sizeof(*negative));
+				*negative = *positive;
+				negative->refcount = 1;
+				negative->terms = malloc(negative->nterms * sizeof(*negative->terms));
+				if (!negative->terms) {
+					free(negative);
+					goto fail;
+				}
+				for (i = 0; i < negative->nterms; i++) {
+					negative->terms[i] = positive->terms[i];
+					negative->terms[i]->refcount += 1;
+				}
+				req_positives[req_i] = positive;
+				req_negatives[req_i] = negative;
+				req_unsigneds[req_i] = NULL;
+				r = perfectly_invert_expression(negative, flags);
+				if (r < 0)
+					goto fail;
+				if (!r) {
+				eliminate_term:
+					libnormalform_free_expression__(req_positives[req_i]);
+					libnormalform_free_expression__(req_negatives[req_i]);
+					req_positives[req_i] = NULL;
+					req_negatives[req_i] = NULL;
+					/* TODO (elimination)
+					 * the term as to be eliminated, and the clause may have
+					 * to be moved down (and potentially eliminated)
+					 */
+				}
+				cmp = libnormalform_literal_cmp__(positive, negative);
+				if (cmp == +1) {
+					tmp = positive, positive = negative, negative = tmp;
+					req_positives[req_i] = positive;
+					req_negatives[req_i] = negative;
+				} else if (cmp != -1) {
+					abort();
+				}
+			} else if (!positive || !negative) {
+				want = positive ? &positive : &negative;
+				*want = malloc(sizeof(**want));
+				**want = *have;
+				(*want)->refcount = 1;
+				(*want)->terms = malloc(have->nterms * sizeof(*have->terms));
+				if (!(*want)->terms) {
+					free(*want);
+					goto fail;
+				}
+				for (i = 0; i < have->nterms; i++) {
+					(*want)->terms[i] = have->terms[i];
+					(*want)->terms[i]->refcount += 1;
+				}
+				r = perfectly_invert_expression(*want, flags);
+				if (r < 0)
+					goto fail;
+				if (!r)
+					goto eliminate_term;
+			}
+
+			memmove(&clause->terms[term_i + 1U], &clause->terms[term_i],
+			        (clause->nterms++ - term_i) * sizeof(*clause->terms));
+
+			clause->terms[term_i] = negative;
+			if (libnormalform_contains_clause__(this, clause, clause_i)) {
+				libnormalform_free_expression__(negative);
+				negative = NULL;
+			}
+
+			clause->terms[term_i] = positive;
+			if (libnormalform_contains_clause__(this, clause, clause_i)) {
+				libnormalform_free_expression__(positive);
+				positive = NULL;
+			}
+
+			if (positive) {
+				clause->terms[term_i] = positive;
+				if (!negative)
+					continue;
+			} else if (negative) {
+				clause->terms[term_i] = negative;
+				continue;
+			} else {
+				libnormalform_free_expression__(clause);
+				memmove(&this->terms[clause_i], &this->terms[clause_i + 1U],
+					(--clause->nterms - clause_i) * sizeof(*clause->terms));
+				goto again;
+			}
+
+			new_clause = malloc(sizeof(*new_clause));
+			if (!new_clause) {
+				libnormalform_free_expression__(negative);
+				goto fail;
+			}
+			*new_clause = *clause;
+			new_clause->refcount = 1;
+			new_clause->terms = malloc(new_clause->nterms * sizeof(*new_clause->terms));
+			if (!new_clause->terms) {
+				libnormalform_free_expression__(negative);
+				free(new_clause);
+				goto fail;
+			}
+			for (i = 0; i < new_clause->nterms; i++) {
+				new_clause->terms[i] = clause->terms[i];
+				new_clause->terms[i]->refcount += 1;
+			}
+
+			new_clause->terms[term_i]->refcount -= 1;
+			new_clause->terms[term_i] = negative;
+
+			new = realloc(this->terms, (this->nterms + 1U) * sizeof(*this->terms));
+			if (!new) {
+				libnormalform_free_expression__(new_clause);
+				goto fail;
+			}
+			this->terms = new;
+			memmove(&this->terms[clause_i + 1U], &this->terms[clause_i],
+			        (this->nterms++ - clause_i) * sizeof(*this->terms));
+			this->terms[clause_i] = new_clause;
+		}
+		if (term_i != clause->nterms)
+			abort();
+	}
+
+	ret = 0;
+fail:
+	if (req_positives) {
+		for (i = 0; i < req_n; i++)
+			if (req_positives[i])
+				libnormalform_free_expression__(req_positives[i]);
+		free(req_positives);
+	}
+	if (req_negatives) {
+		for (i = 0; i < req_n; i++)
+			if (req_positives[i])
+				libnormalform_free_expression__(req_positives[i]);
+		free(req_positives);
+	}
+	if (req_unsigneds) {
+		for (i = 0; i < req_n; i++)
+			if (req_unsigneds[i])
+				libnormalform_free_expression__(req_unsigneds[i]);
+		free(req_unsigneds);
+	}
+	return ret;
+}
+
+
+struct libnormalform_term *
+(libnormalform_cdnf)(LIBNORMALFORM_SENTENCE *this, uint64_t flags, const struct libnormalform_analysers *analysers)
+{
+	return libnormalform_express__(this, flags | LIBNORMALFORM_RELAX_XOR, analysers, DNF, &canonicalise_dnf);
+}
+
+
+#else
+
+TODO_TEST
+
+#endif