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