diff options
Diffstat (limited to 'libnormalform_cdnf.c')
| -rw-r--r-- | libnormalform_cdnf.c | 560 |
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 |