From 77ade8d20906fe9ca2cf6788ff1e1437e0912868 Mon Sep 17 00:00:00 2001 From: Mattias Andrée Date: Mon, 1 Jun 2026 19:07:14 +0200 Subject: Second commit MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Signed-off-by: Mattias Andrée --- libnormalform_express.c | 834 +----------------------------------------------- 1 file changed, 1 insertion(+), 833 deletions(-) (limited to 'libnormalform_express.c') diff --git a/libnormalform_express.c b/libnormalform_express.c index 2532488..25c4d7c 100644 --- a/libnormalform_express.c +++ b/libnormalform_express.c @@ -3,842 +3,10 @@ #ifndef TEST -struct expression { - enum libnormalform_term_type type; - unsigned char reduced; - unsigned char invert; - size_t nterms; - struct expression **terms; - void *user_item; -}; - - -static enum libnormalform_sentences_relationship -get_relationship(struct expression *l, struct expression *r, const struct libnormalform_analysers *analysers) /* TODO */ -{ - (void) l; - (void) r; - (void) analysers; - return LIBNORMALFORM_MUTUALLY_INDEPENDENT; -} - - -static void -free_expression(struct expression *this) -{ - if (this->terms) { - while (this->nterms) - free_expression(this->terms[--this->nterms]); - free(this->terms); - } - free(this); -} - - -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->reduced = 0; - ret->invert = 0; - ret->nterms = 0; - ret->terms = NULL; - ret->user_item = NULL; - - 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_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: - 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) { - free_expression(sub); - goto contradiction; - } - free_expression(sub); - ret->reduced |= 1; - } else if (!sub->nterms && ret->type == LIBNORMALFORM_DISJUNCTION && sub->type == LIBNORMALFORM_CONJUNCTION) { - /* ⋁(X ∪ {⋀∅}) = ⋁(X ∪ {⊤}) = ⋁X ∨ ⊤ = ⊤ */ - free_expression(ret); - ret = sub; - goto tautology; - } else { - ret->terms = malloc(sizeof(*ret->terms)); - if (!ret->terms) { - 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) { - 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) { - free_expression(sub); - goto contradiction; - } - free_expression(sub); - ret->reduced |= 1; - } else if (!sub->nterms && ret->type == LIBNORMALFORM_DISJUNCTION && sub->type == LIBNORMALFORM_CONJUNCTION) { - /* ⋁(X ∪ {⋀∅}) = ⋁(X ∪ {⊤}) = ⋁X ∨ ⊤ = ⊤ */ - free_expression(ret); - ret = sub; - goto tautology; - } else { - void *new = realloc(ret->terms, (ret->nterms + 1U) * sizeof(*ret->terms)); - if (!new) { - 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 + 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 + 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); - free_expression(ret); - return NULL; -} - - -static struct expression * -make_binary(int invert_left, struct expression *left, int invert_right, struct expression *right, enum libnormalform_term_type type) -{ - struct expression *ret; - ret = malloc(sizeof(*ret)); - if (!ret) - return NULL; - ret->type = type; - ret->reduced = 0; - ret->invert = 0; - ret->user_item = NULL; - ret->nterms = 0; - ret->terms = malloc(2 * sizeof(*ret->terms)); - if (!ret->terms) { - free(ret); - return NULL; - } - (ret->terms[0] = left)->invert ^= (unsigned char)invert_left; - (ret->terms[1] = right)->invert ^= (unsigned char)invert_right; - return ret; -} - - -static int -reduce_expression(struct expression *this, const struct libnormalform_analysers *analysers) -{ - enum libnormalform_sentences_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++) { - relationship = get_relationship(this->terms[i], this->terms[j], analysers); - switch (relationship) { - case LIBNORMALFORM_MATERIAL_IMPLICATION: - case LIBNORMALFORM_IDENTICAL: - free_expression(this->terms[j]); - this->terms[j--] = this->terms[--this->nterms]; - break; - case LIBNORMALFORM_CONVERSE_IMPLICATION: - 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++) - 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++) { - relationship = get_relationship(this->terms[i], this->terms[j], analysers); - switch (relationship) { - case LIBNORMALFORM_IDENTICAL: - case LIBNORMALFORM_CONVERSE_IMPLICATION: - free_expression(this->terms[j]); - this->terms[j--] = this->terms[--this->nterms]; - break; - case LIBNORMALFORM_MATERIAL_IMPLICATION: - 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++) - 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++) { - relationship = get_relationship(this->terms[i], this->terms[j], analysers); - switch (relationship) { - case LIBNORMALFORM_MATERIAL_IMPLICATION: - new = make_binary(1, this->terms[i], 0, this->terms[j], LIBNORMALFORM_CONJUNCTION); - if (!new) - return -1; - goto xor_reduced; - case LIBNORMALFORM_CONVERSE_IMPLICATION: - new = 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: - free_expression(this->terms[i]); - 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 = make_binary(0, this->terms[i], 0, this->terms[j], LIBNORMALFORM_DISJUNCTION); - if (!new) - return -1; - goto xor_reduced; - case LIBNORMALFORM_JOINTLY_UNDENIABLE: - new = 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: - free_expression(this->terms[i]); - 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; -} - - -static void * -domain_view_transform(void *user_data, void *input) -{ - struct libnormalform_mapping *kvpair = input; - (void) user_data; - return kvpair->key; -} - - -static void * -image_view_transform(void *user_data, void *input) -{ - struct libnormalform_mapping *kvpair = input; - (void) user_data; - return kvpair->value; -} - - -static int -apply_transformation(struct expression *this, enum libnormalform_builtin_transformer transformer) -{ - /* Only .builtin is actually needed, but the others - * could be useful for debugging by the user */ - static struct libnormalform_transformer domain_view = { - .transform = &domain_view_transform, - .deallocate = NULL, - .user_data = NULL, - .identifier = "", - .builtin = LIBNORMALFORM_DOMAIN_VIEW - }; - static struct libnormalform_transformer image_view = { - .transform = &image_view_transform, - .deallocate = NULL, - .user_data = NULL, - .identifier = "", - .builtin = LIBNORMALFORM_IMAGE_VIEW - }; - - size_t i; - struct expression *new, **term_singleton; - - switch (this->type) { - case LIBNORMALFORM_CONJUNCTION: - case LIBNORMALFORM_DISJUNCTION: - case LIBNORMALFORM_EXCLUSIVE_DISJUNCTION: - /* transformations are morphism */ - for (i = 0; i < this->nterms; i++) - if (apply_transformation(this->terms[i], transformer)) - return -1; - break; - - case LIBNORMALFORM_TRANSFORMATION: - case LIBNORMALFORM_FUNCTION: - case LIBNORMALFORM_NEGATED_FUNCTION: - new = malloc(sizeof(*new)); - if (!new) - return -1; - term_singleton = malloc(sizeof(*term_singleton)); - if (!term_singleton) { - free(new); - return -1; - } - *new = *this; - this->type = LIBNORMALFORM_TRANSFORMATION; - this->reduced = 0; - this->invert = 0; - this->nterms = 1; - this->terms = term_singleton; - this->terms[0] = new; - switch (transformer) { - case LIBNORMALFORM_DOMAIN_VIEW: - this->user_item = &domain_view; - break; - case LIBNORMALFORM_IMAGE_VIEW: - this->user_item = &image_view; - break; - default: - case LIBNORMALFORM_NOT_BUILT_IN: - abort(); - } - break; - - case LIBNORMALFORM_VARIABLE: - case LIBNORMALFORM_NEGATED_VARIABLE: - /* variables are input-independent leafs */ - 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: - /* qualifiers reset input */ - default: - break; - } - - return 0; -} - - -static int -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; - - 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) { - this->invert ^= 1; - *require_inversion = 0; - } - if (flags & LIBNORMALFORM_ELIMINATE_XOR) - goto eliminate; - for (i = 0; i < this->nterms; i++) - if (fix_presentation(this->terms[i], flags, &this->invert, reduced)) - return -1; - if (this->invert) { - this->invert = 0; - this->terms[0]->invert ^= 1; - if (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 if (WILL_ELIMINATE(FOR_ALL, this->invert)) { - goto eliminate; - } - 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))) { - this->terms[this->nterms - 1]->invert ^= 1; - this->type = LIBNORMALFORM_AVOID_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 if (WILL_ELIMINATE(FOR_ANY, this->invert)) { - goto eliminate; - } - this->type ^= (LIBNORMALFORM_FOR_ANY ^ LIBNORMALFORM_NEGATED_FOR_ANY) * this->invert; - for_any: - this->invert = 0; - if (flags & (LIBNORMALFORM_AVOID_FOR_ANY << (this->type - LIBNORMALFORM_FOR_ANY))) { - this->terms[this->nterms - 1]->invert ^= 1; - this->type = LIBNORMALFORM_AVOID_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)) { - goto eliminate; - } - this->type ^= (LIBNORMALFORM_FOR_ONE ^ LIBNORMALFORM_NEGATED_FOR_ONE) * this->invert; - if (this->type == LIBNORMALFORM_FOR_ONE) { - if (flags & LIBNORMALFORM_RELAX_FOR_ONE) { - this->type = LIBNORMALFORM_FOR_ANY; - 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 (fix_presentation(this->terms[i], flags, require_inversion, reduced)) - return -1; - - return 0; - -eliminate: - *require_inversion = 0; - this->reduced = 0; - this->invert = 0; - while (this->nterms) - 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 = make_binary(1, this->terms[0], 0, this->terms[1], LIBNORMALFORM_DISJUNCTION); - goto join_sides; - -for_any_join_sides: - new = 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 (apply_transformation(this->terms[0]->terms[0], LIBNORMALFORM_DOMAIN_VIEW)) - return -1; - if (apply_transformation(this->terms[0]->terms[1], LIBNORMALFORM_IMAGE_VIEW)) - return -1; - *reduced = 1; - return 0; - -#undef WILL_ELIMINATE -} - - -static int -expression_to_term(struct libnormalform_term *out, struct expression *this) -{ - size_t i; - - out->type = this->type; - out->reduced = this->reduced; - - switch (this->type) { - case LIBNORMALFORM_CONJUNCTION: - case LIBNORMALFORM_DISJUNCTION: - case LIBNORMALFORM_EXCLUSIVE_DISJUNCTION: - out->term.clause.nterms = 0; - out->term.clause.terms = calloc(this->nterms, sizeof(*out->term.clause.terms)); - if (!out->term.clause.terms) - return -1; - for (i = 0; i < this->nterms; i++) - if (expression_to_term(&out->term.clause.terms[out->term.clause.nterms++], this->terms[i])) - return -1; - break; - - case LIBNORMALFORM_TRANSFORMATION: - out->term.transformation.transformer = this->user_item; - out->term.transformation.sentence = calloc(1, sizeof(*out->term.transformation.sentence)); - if (!out->term.transformation.sentence || - expression_to_term(out->term.transformation.sentence, this->terms[0])) - return -1; - break; - - case LIBNORMALFORM_VARIABLE: - case LIBNORMALFORM_NEGATED_VARIABLE: - out->term.variable = this->user_item; - break; - - case LIBNORMALFORM_FUNCTION: - case LIBNORMALFORM_NEGATED_FUNCTION: - out->term.function = this->user_item; - 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: - out->term.qualification.map = this->user_item; - if (this->nterms == 1) { - out->term.qualification.antecedent = NULL; - out->term.qualification.predicate = calloc(1, sizeof(*out->term.qualification.predicate)); - if (!out->term.qualification.predicate || - expression_to_term(out->term.qualification.predicate, this->terms[0])) - return -1; - } else { - out->term.qualification.antecedent = calloc(1, sizeof(*out->term.qualification.antecedent)); - if (!out->term.qualification.antecedent) - return -1; - out->term.qualification.predicate = calloc(1, sizeof(*out->term.qualification.predicate)); - if (!out->term.qualification.predicate || - expression_to_term(out->term.qualification.antecedent, this->terms[0]) || - expression_to_term(out->term.qualification.predicate, this->terms[1])) - return -1; - } - break; - - default: - abort(); - } - - return 0; -} - - struct libnormalform_term * (libnormalform_express)(LIBNORMALFORM_SENTENCE *this, uint64_t flags, const struct libnormalform_analysers *analysers) { - struct libnormalform_term *ret; - struct expression *expression; - int reduced; - - if (flags & ~LIBNORMALFORM_ALL_EXPRESS_FLAGS__) { - errno = EINVAL; - return NULL; - } - - if (flags & LIBNORMALFORM_REDUCE_XOR) - flags &= ~LIBNORMALFORM_ELIMINATE_XOR; - if ((flags & LIBNORMALFORM_ELIMINATE_FOR_ANY) && (flags & LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ALL)) - flags &= ~LIBNORMALFORM_RELAX_FOR_ONE; - if (flags & LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ALL) - flags &= ~LIBNORMALFORM_AVOID_FOR_ANY; - if (flags & LIBNORMALFORM_ELIMINATE_FOR_ALL) - flags &= ~LIBNORMALFORM_AVOID_NEGATED_FOR_ANY; - if (flags & LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ANY) - flags &= ~LIBNORMALFORM_AVOID_FOR_ALL; - if (flags & LIBNORMALFORM_ELIMINATE_FOR_ANY) - flags &= ~LIBNORMALFORM_AVOID_NEGATED_FOR_ALL; - 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; - - expression = sentence_to_expression(this, flags); - if (!expression) - return NULL; - do { - if (reduce_expression(expression, analysers)) { - free_expression(expression); - return NULL; - } - reduced = 0; - if (fix_presentation(expression, flags, &(unsigned char){0}, &reduced)) { - free_expression(expression); - return NULL; - } - } while (reduced); - - ret = malloc(sizeof(*ret)); - if (!ret) { - free_expression(expression); - return NULL; - } - if (expression_to_term(ret, expression)) { -#if defined(__GNUC__) -# pragma GCC diagnostic push -# pragma GCC diagnostic ignored "-Wmismatched-dealloc" -#endif - libnormalform_free(ret); - ret = NULL; -#if defined(__GNUC__) -# pragma GCC diagnostic pop -#endif - } - free_expression(expression); - - return ret; + return libnormalform_express__(this, flags, analysers, NNF, NULL); } -- cgit v1.3.1