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_true.c | 156 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 156 insertions(+) create mode 100644 libnormalform_true.c (limited to 'libnormalform_true.c') diff --git a/libnormalform_true.c b/libnormalform_true.c new file mode 100644 index 0000000..e716cc5 --- /dev/null +++ b/libnormalform_true.c @@ -0,0 +1,156 @@ +/* See LICENSE file for copyright and license details. */ +#include "common.h" +#ifndef TEST + + +/** + * See `.inverse` in `struct libnormalform_sentence` (TRUE implementation) + */ +static LIBNORMALFORM_SENTENCE * +true_inverse(LIBNORMALFORM_SENTENCE *this) +{ + (void) this; + return libnormalform_false(); +} + + +/** + * See `.equals` in `struct libnormalform_sentence` (TRUE implementation) + */ +static int +true_equals(LIBNORMALFORM_SENTENCE *this, LIBNORMALFORM_SENTENCE *other, int *inv_out) +{ + (void) this; + if (other->type == TYPE_TRUE) { + *inv_out = 0; + return 1; + } else if (other->type == TYPE_FALSE) { + *inv_out = 1; + return 1; + } else { + return 0; + } +} + + +/** + * See `.evaluate` in `struct libnormalform_sentence` (TRUE implementation) + */ +CONST static int +true_evaluate(LIBNORMALFORM_SENTENCE *this, void *input) +{ + (void) this; + (void) input; + return 1; +} + + +LIBNORMALFORM_SENTENCE * +(libnormalform_true)(void) +{ + static const struct libnormalform_sentence prototype = { + PROTOTYPE_COMMON, + .type = TYPE_TRUE, + .hash = TRUE_FALSE_HASH, + .inverse = &true_inverse, + .equals = &true_equals, + .evaluate = &true_evaluate + }; + + /* + * During normalisation, some fields may be set, + * therefore a new allocation is returned instead + * of a reference to a static allocation, so that + * converation can be done from the threads at + * the same time on different sentences, both + * including this constant. + */ + + LIBNORMALFORM_SENTENCE *ret = malloc(sizeof(*ret)); + if (ret) + *ret = prototype; + return ret; +} + + +#else + + +static int +tautology(void *user_data, void *input) +{ + (void) user_data; + (void) input; + return 1; +} + + +static int +contradiction(void *user_data, void *input) +{ + (void) user_data; + (void) input; + return 0; +} + + +int +main(void) +{ + TEST_BEGIN; + + struct libnormalform_variable var1, var2; + struct libnormalform_function fun1, fun2; + struct libnormalform_map domain; + LIBNORMALFORM_SENTENCE *a, *b, *v1, *v2, *f1, *f2; + + var1.value = LIBNORMALFORM_FALSE; + var2.value = LIBNORMALFORM_TRUE; + fun1.evaluate = &tautology; + fun2.evaluate = &contradiction; + + ASSUME(v1 = libnormalform_variable(&var1)); + ASSUME(v2 = libnormalform_variable(&var2)); + ASSUME(f1 = libnormalform_function(&fun1)); + ASSUME(f2 = libnormalform_function(&fun2)); + + ASSUME(a = libnormalform_true()); + ASSERT(a->type == TYPE_TRUE); + ASSERT(a->refcount == 1); + ASSERT_EQUAL(a, a); + + ASSERT(a->evaluate(a, NULL) == 1); + +#define CHECK(CMP, X)\ + do {\ + ASSUME(b = (X));\ + ASSERT_##CMP(a, b);\ + libnormalform_free(b);\ + } while (0) + + CHECK(EQUAL, libnormalform_true()); + CHECK(INVEQUAL, libnormalform_false()); + CHECK(NOTEQUAL, libnormalform_and2(REF(v1), REF(v2))); + CHECK(NOTEQUAL, libnormalform_or2(REF(v1), REF(v2))); + CHECK(NOTEQUAL, libnormalform_xor2(REF(v1), REF(v2))); + CHECK(NOTEQUAL, libnormalform_all(&domain, REF(f1), REF(f2))); + CHECK(NOTEQUAL, libnormalform_any(&domain, REF(f1), REF(f2))); + CHECK(NOTEQUAL, libnormalform_one(&domain, REF(f1), REF(f2))); + CHECK(NOTEQUAL, libnormalform_not(libnormalform_one(&domain, REF(f1), REF(f2)))); + CHECK(NOTEQUAL, REF(v1)); + CHECK(NOTEQUAL, REF(f1)); + +#undef CHECK + + libnormalform_free(a); + + libnormalform_free(v1); + libnormalform_free(v2); + libnormalform_free(f1); + libnormalform_free(f2); + + TEST_END; +} + + +#endif -- cgit v1.3.1