From 4294ec0ed06ee34920c9edaeebaeb8b65c720791 Mon Sep 17 00:00:00 2001 From: Mattias Andrée Date: Fri, 19 Jul 2024 01:29:42 +0200 Subject: First commit MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Signed-off-by: Mattias Andrée --- libnormalform_transformation.c | 419 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 419 insertions(+) create mode 100644 libnormalform_transformation.c (limited to 'libnormalform_transformation.c') diff --git a/libnormalform_transformation.c b/libnormalform_transformation.c new file mode 100644 index 0000000..3a1218b --- /dev/null +++ b/libnormalform_transformation.c @@ -0,0 +1,419 @@ +/* See LICENSE file for copyright and license details. */ +#include "common.h" +#ifndef TEST + + +/** + * See `.inverse` in `struct libnormalform_sentence` (Transformation function implementation) + */ +static LIBNORMALFORM_SENTENCE * +trans_inverse(LIBNORMALFORM_SENTENCE *this) +{ + return libnormalform_transformation(this->data.trans.function, this->data.trans.input->inverse(this->data.trans.input)); +} + + +/** + * See `.equals` in `struct libnormalform_sentence` (Transformation function implementation) + */ +static int +trans_equals(LIBNORMALFORM_SENTENCE *this, LIBNORMALFORM_SENTENCE *other, int *inv_out) +{ + if (other->type != TYPE_TRANS || this->data.trans.function != other->data.trans.function) + return 0; + return this->data.trans.input->equals(this->data.trans.input, other->data.trans.input, inv_out); +} + + +/** + * See `.evaluate` in `struct libnormalform_sentence` (Transformation function implementation) + */ +static int +trans_evaluate(LIBNORMALFORM_SENTENCE *this, void *input) +{ + int r; + input = this->data.trans.function->transform(this->data.trans.function->user_data, input); + if (!input) + return -1; + r = this->data.trans.input->evaluate(this->data.trans.input, input); + if (this->data.trans.function->deallocate) + this->data.trans.function->deallocate(this->data.trans.function->user_data, input); + return r; +} + + +LIBNORMALFORM_SENTENCE * +(libnormalform_transformation)(struct libnormalform_transformer *function, LIBNORMALFORM_SENTENCE *sentence) +{ + static const struct libnormalform_sentence prototype = { + PROTOTYPE_COMMON, + .type = TYPE_TRANS, + .inverse = &trans_inverse, + .equals = &trans_equals, + .evaluate = &trans_evaluate + }; + + LIBNORMALFORM_SENTENCE *ret, *left, *right; + LIBNORMALFORM_SENTENCE *(*connective)(LIBNORMALFORM_SENTENCE *, LIBNORMALFORM_SENTENCE *); + + if (!sentence) + return NULL; + + function->builtin = LIBNORMALFORM_NOT_BUILT_IN; + + switch (sentence->type) { + case TYPE_ALL: + case TYPE_ANY: + case TYPE_ONE: + case TYPE_NOT_ONE: + libnormalform_free(sentence); + errno = EDOM; + return NULL; + + case TYPE_TRUE: + case TYPE_FALSE: + case TYPE_VARIABLE: + return sentence; + + case TYPE_FUNCTION: + case TYPE_TRANS: + ret = malloc(sizeof(*ret)); + if (!ret) { + libnormalform_free(sentence); + return NULL; + } + *ret = prototype; + ret->hash = TRANS_HASH(function, sentence); + ret->data.trans.function = function; + ret->data.trans.input = sentence; + return ret; + + case TYPE_AND: + connective = &libnormalform_and2__; + break; + case TYPE_OR: + connective = &libnormalform_or2__; + break; + case TYPE_XOR: + connective = &libnormalform_xor2__; + break; + + default: + abort(); + } + + left = LEFT(sentence), LEFT(sentence) = NULL; + right = RIGHT(sentence), RIGHT(sentence) = NULL; + libnormalform_free(sentence); + left = libnormalform_transformation(function, left); + if (!left) { + libnormalform_free(right); + return NULL; + } + right = libnormalform_transformation(function, right); + if (!right) { + libnormalform_free(left); + return NULL; + } + + return (*connective)(left, right); +} + + +#else + + +static void * +uppercase(void *user_data, void *input) +{ + char *s = strdup(input), *p; + (void) user_data; + if (s) + for (p = s; *p; p++) + *p = (char)toupper(*p); + return s; +} + + +static void * +constuppercase(void *user_data, void *input) +{ + static char ret[] = "HELLO WORLD"; + (void) user_data; + (void) input; + return ret; +} + + +static void * +einval(void *user_data, void *input) +{ + (void) user_data; + (void) input; + errno = EINVAL; + return NULL; +} + + +static void +deallocate(void *user_data, void *input) +{ + (void) user_data; + free(input); +} + + +static int +validate(void *expected, void *input) +{ + return input ? !strcmp(input, expected) : (errno = EDOM, -1); +} + + +int +main(void) +{ + TEST_BEGIN; + + struct libnormalform_transformer trans1, trans2; + struct libnormalform_function fun1, fun2; + struct libnormalform_variable var1; + struct libnormalform_map dom1; + LIBNORMALFORM_SENTENCE *a, *b, *f1, *f2; + + errno = 0; + ASSERT(!libnormalform_transformation(&trans1, NULL) && errno == 0); + errno = 1; + ASSERT(!libnormalform_transformation(&trans1, NULL) && errno == 1); + + /* F(⊤) = ⊤ */ + ASSUME(a = libnormalform_true()); + ASSUME(b = libnormalform_transformation(&trans1, REF(a))); + ASSERT(b->refcount == 2); + ASSERT(b->type == TYPE_TRUE); + ASSERT(b == a); + libnormalform_free(a); + libnormalform_free(b); + + /* F(⊥) = ⊥ */ + ASSUME(a = libnormalform_false()); + ASSUME(b = libnormalform_transformation(&trans1, REF(a))); + ASSERT(b->refcount == 2); + ASSERT(b->type == TYPE_FALSE); + ASSERT(b == a); + libnormalform_free(a); + libnormalform_free(b); + + /* F(a) = a */ + ASSUME(a = libnormalform_variable(&var1)); + ASSUME(b = libnormalform_transformation(&trans1, REF(a))); + ASSERT(b->refcount == 2); + ASSERT(b->type == TYPE_VARIABLE); + ASSERT(b == a); + libnormalform_free(a); + libnormalform_free(b); + + /* F(f(x)) irreducible */ + ASSUME(a = libnormalform_function(&fun1)); + ASSUME(b = libnormalform_transformation(&trans1, REF(a))); + ASSERT(b->refcount == 1); + ASSERT(a->refcount == 2); + ASSERT(b->type == TYPE_TRANS); + ASSERT(b->data.trans.function == &trans1); + ASSERT(b->data.trans.input == a); + libnormalform_free(a); + libnormalform_free(b); + + /* F(f(x) ∧ g(x)) = F(f(x)) ∧ F(g(x)) */ + ASSUME(a = libnormalform_function(&fun1)); + ASSUME(b = libnormalform_function(&fun2)); + ASSUME(a = libnormalform_and2(a, b)); + ASSUME(b = libnormalform_transformation(&trans1, a)); + ASSERT(b->refcount == 1); + ASSERT(b->type == TYPE_AND); + ASSERT(LEFT(b)->type == TYPE_TRANS); + ASSERT(RIGHT(b)->type == TYPE_TRANS); + ASSERT(LEFT(b)->refcount == 1); + ASSERT(RIGHT(b)->refcount == 1); + ASSERT(LEFT(b)->data.trans.function == &trans1); + ASSERT(RIGHT(b)->data.trans.function == &trans1); + ASSERT(LEFT(b)->data.trans.input); + ASSERT(RIGHT(b)->data.trans.input); + ASSERT(LEFT(b)->data.trans.input->type == TYPE_FUNCTION); + ASSERT(RIGHT(b)->data.trans.input->type == TYPE_FUNCTION); + ASSERT(LEFT(b)->data.trans.input != RIGHT(b)->data.trans.input); + libnormalform_free(b); + + /* F(f(x) ∨ g(x)) = F(f(x)) ∨ F(g(x)) */ + ASSUME(a = libnormalform_function(&fun1)); + ASSUME(b = libnormalform_function(&fun2)); + ASSUME(a = libnormalform_or2(a, b)); + ASSUME(b = libnormalform_transformation(&trans1, a)); + ASSERT(b->refcount == 1); + ASSERT(b->type == TYPE_OR); + ASSERT(LEFT(b)->type == TYPE_TRANS); + ASSERT(RIGHT(b)->type == TYPE_TRANS); + ASSERT(LEFT(b)->refcount == 1); + ASSERT(RIGHT(b)->refcount == 1); + ASSERT(LEFT(b)->data.trans.function == &trans1); + ASSERT(RIGHT(b)->data.trans.function == &trans1); + ASSERT(LEFT(b)->data.trans.input); + ASSERT(RIGHT(b)->data.trans.input); + ASSERT(LEFT(b)->data.trans.input->type == TYPE_FUNCTION); + ASSERT(RIGHT(b)->data.trans.input->type == TYPE_FUNCTION); + ASSERT(LEFT(b)->data.trans.input != RIGHT(b)->data.trans.input); + libnormalform_free(b); + + /* F(f(x) ⊕ g(x)) = F(f(x)) ⊕ F(g(x)) */ + ASSUME(a = libnormalform_function(&fun1)); + ASSUME(b = libnormalform_function(&fun2)); + ASSUME(a = libnormalform_xor2(a, b)); + ASSUME(b = libnormalform_transformation(&trans1, a)); + ASSERT(b->refcount == 1); + ASSERT(b->type == TYPE_XOR); + ASSERT(LEFT(b)->type == TYPE_TRANS); + ASSERT(RIGHT(b)->type == TYPE_TRANS); + ASSERT(LEFT(b)->refcount == 1); + ASSERT(RIGHT(b)->refcount == 1); + ASSERT(LEFT(b)->data.trans.function == &trans1); + ASSERT(RIGHT(b)->data.trans.function == &trans1); + ASSERT(LEFT(b)->data.trans.input); + ASSERT(RIGHT(b)->data.trans.input); + ASSERT(LEFT(b)->data.trans.input->type == TYPE_FUNCTION); + ASSERT(RIGHT(b)->data.trans.input->type == TYPE_FUNCTION); + ASSERT(LEFT(b)->data.trans.input != RIGHT(b)->data.trans.input); + libnormalform_free(b); + + /* F(Q(q)∀{p,q}:P(p)) illegal construct */ + ASSUME(a = libnormalform_function(&fun1)); + ASSUME(b = libnormalform_function(&fun2)); + ASSUME(a = libnormalform_all(&dom1, a, b)); + errno = 0; + ASSERT(!libnormalform_transformation(&trans1, a) && errno == EDOM); + + /* F(Q(q)∃{p,q}:P(p)) illegal construct */ + ASSUME(a = libnormalform_function(&fun1)); + ASSUME(b = libnormalform_function(&fun2)); + ASSUME(a = libnormalform_any(&dom1, a, b)); + errno = 0; + ASSERT(!libnormalform_transformation(&trans1, a) && errno == EDOM); + + /* F(Q(q)∃!{p,q}:P(p)) illegal construct */ + ASSUME(a = libnormalform_function(&fun1)); + ASSUME(b = libnormalform_function(&fun2)); + ASSUME(a = libnormalform_one(&dom1, a, b)); + errno = 0; + ASSERT(!libnormalform_transformation(&trans1, a) && errno == EDOM); + + /* F(¬(Q(q)∃!{p,q}:P(p))) illegal construct */ + ASSUME(a = libnormalform_function(&fun1)); + ASSUME(b = libnormalform_function(&fun2)); + ASSUME(a = libnormalform_one(&dom1, a, b)); + ASSUME(a = libnormalform_not(a)); + errno = 0; + ASSERT(!libnormalform_transformation(&trans1, a) && errno == EDOM); + + ASSUME(a = libnormalform_function(&fun1)); + trans1.transform = &uppercase; + trans1.deallocate = &deallocate; + + fun1.evaluate = validate; + ASSUME(fun1.user_data = strdup("hello world")); + ASSERT(a->evaluate(a, (char []){"hello world"}) == 1); + ASSERT(a->evaluate(a, (char []){"HELLO WORLD"}) == 0); + ASSERT(a->evaluate(a, (char []){"x"}) == 0); + errno = 0; + ASSERT(a->evaluate(a, NULL) == -1 && errno == EDOM); + free(fun1.user_data); + + fun1.evaluate = validate; + ASSUME(fun1.user_data = strdup("HELLO WORLD")); + ASSUME(a = libnormalform_transformation(&trans1, a)); + ASSERT(a->evaluate(a, (char []){"hello world"}) == 1); + ASSERT(a->evaluate(a, (char []){"HELLO WORLD"}) == 1); + ASSERT(a->evaluate(a, (char []){"x"}) == 0); + trans1.transform = constuppercase; + trans1.deallocate = NULL; + ASSERT(a->evaluate(a, (char []){"hello world"}) == 1); + free(fun1.user_data); + + libnormalform_free(a); + + ASSUME(f1 = libnormalform_function(&fun1)); + ASSUME(f2 = libnormalform_function(&fun2)); + + ASSUME(a = libnormalform_transformation(&trans1, REF(f1))); + trans1.transform = einval; + trans1.deallocate = NULL; + errno = 0; + ASSERT(a->evaluate(a, (char []){"hello world"}) == -1 && errno == EINVAL); + + ASSERT_NOTEQUAL(a, f1); + + ASSUME(b = libnormalform_true()); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(b); + + ASSUME(b = libnormalform_true()); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(b); + + ASSUME(b = libnormalform_variable(&var1)); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(b); + + ASSUME(b = libnormalform_transformation(&trans1, REF(f1))); + ASSERT_EQUAL(a, b); + libnormalform_free(b); + + ASSUME(b = libnormalform_transformation(&trans1, libnormalform_not(REF(f1)))); + ASSERT_INVEQUAL(a, b); + libnormalform_free(b); + + ASSUME(b = libnormalform_transformation(&trans1, REF(f2))); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(b); + + ASSUME(b = libnormalform_transformation(&trans2, REF(f1))); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(b); + + ASSUME(b = libnormalform_and2(REF(f1), REF(f2))); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(b); + + ASSUME(b = libnormalform_or2(REF(f1), REF(f2))); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(b); + + ASSUME(b = libnormalform_xor2(REF(f1), REF(f2))); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(b); + + ASSUME(b = libnormalform_all(&dom1, REF(f1), REF(f2))); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(b); + + ASSUME(b = libnormalform_any(&dom1, REF(f1), REF(f2))); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(b); + + ASSUME(b = libnormalform_one(&dom1, REF(f1), REF(f2))); + ASSERT_NOTEQUAL(a, b); + ASSUME(b = libnormalform_not(b)); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(b); + + ASSUME(b = libnormalform_not(libnormalform_transformation(&trans1, REF(f1)))); + ASSERT_INVEQUAL(a, b); + libnormalform_free(b); + + libnormalform_free(a); + libnormalform_free(f1); + libnormalform_free(f2); + + TEST_END; +} + + +#endif -- cgit v1.3.1