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_xnor.c | 437 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 437 insertions(+) create mode 100644 libnormalform_xnor.c (limited to 'libnormalform_xnor.c') diff --git a/libnormalform_xnor.c b/libnormalform_xnor.c new file mode 100644 index 0000000..3b0bff6 --- /dev/null +++ b/libnormalform_xnor.c @@ -0,0 +1,437 @@ +/* See LICENSE file for copyright and license details. */ +#include "common.h" +#ifndef TEST + + +LIBNORMALFORM_SENTENCE * +(libnormalform_xnor)(LIBNORMALFORM_SENTENCE **xs) +{ + size_t n = 0; + + while (xs[n]) + n += 1; + + /* ⨀(X ∪ {x}) = ⨀X ⊙ x = ¬(⨀X ⊕ x) */ + /* ⨀∅ = ⨀∅ ⊙ 1 = ⨀∅ ⊙ 1 ⊙ 1 = ⨀(∅ ∪ {1, 1}) = ⨀{1, 1} = 1 ⊙ 1 = 1 = ¬0 = ¬⨁∅ */ + if (n & 1U) + return libnormalform_xor(xs); + else + return libnormalform_not(libnormalform_xor(xs)); +} + + +#else + + +#define XNOR(...) LIBNORMALFORM_XNOR(__VA_ARGS__) + + +int +main(void) +{ + TEST_BEGIN; + + struct libnormalform_variable var1, var2, var3; + LIBNORMALFORM_SENTENCE *a, *b, *v1, *v2, *v3; + LIBNORMALFORM_SENTENCE *ts, *fs; + + ASSUME(v1 = libnormalform_variable(&var1)); + ASSUME(v2 = libnormalform_variable(&var2)); + ASSUME(v3 = libnormalform_variable(&var3)); + ASSUME(ts = libnormalform_true()); + ASSUME(fs = libnormalform_false()); + +#ifdef USE_CHECKED_VERSION + errno = 0; + ASSERT(!XNOR(REF(v1), NULL) && errno == 0); + errno = 1; + ASSERT(!XNOR(REF(v1), NULL) && errno == 1); + errno = 0; + ASSERT(!XNOR(NULL, REF(v1)) && errno == 0); + errno = 1; + ASSERT(!XNOR(NULL, REF(v1)) && errno == 1); + errno = 0; + ASSERT(!XNOR(NULL, NULL) && errno == 0); + errno = 1; + ASSERT(!XNOR(NULL, NULL) && errno == 1); +#endif + +#define T REF(ts) +#define F REF(fs) +#define TV LIBNORMALFORM_TRUE +#define FV LIBNORMALFORM_FALSE + +#define ASSERT_CONST(VALUE, ...)\ + do {\ + ASSUME(a = XNOR(__VA_ARGS__));\ + ASSERT(a->type == TYPE_##VALUE);\ + libnormalform_free(a);\ + } while (0) + +#define ASSERT_EVAL2(VALUE, V1, V2)\ + do {\ + ASSUME(a = XNOR(REF(v1), REF(v2)));\ + ASSERT(a->type != TYPE_TRUE && a->type != TYPE_FALSE);\ + var1.value = V1##V;\ + var2.value = V2##V;\ + ASSERT(libnormalform_evaluate(a) == (int)LIBNORMALFORM_##VALUE);\ + libnormalform_free(a);\ + } while (0) + +#define ASSERT_EVAL3(VALUE, V1, V2, V3)\ + do {\ + ASSUME(a = XNOR(REF(v1), REF(v2), REF(v3)));\ + ASSERT(a->type != TYPE_TRUE && a->type != TYPE_FALSE);\ + var1.value = V1##V;\ + var2.value = V2##V;\ + var3.value = V3##V;\ + ASSERT(libnormalform_evaluate(a) == (int)LIBNORMALFORM_##VALUE);\ + libnormalform_free(a);\ + } while (0) + +#ifndef USE_TWO + +#if defined(__GNUC__) +# pragma GCC diagnostic push +# pragma GCC diagnostic ignored "-Wformat" +#endif + + ASSERT_CONST(TRUE); /* XNOR () -> TRUE */ + +#if defined(__GNUC__) +# pragma GCC diagnostic pop +#endif + + ASSERT_CONST(TRUE, T); /* XNOR (TRUE) -> TRUE */ + ASSERT_CONST(FALSE, F); /* XNOR (FALSE) -> FALSE */ + +#endif + + ASSERT_CONST(TRUE, F, F); /* XNOR (FALSE, FALSE) -> TRUE */ + ASSERT_CONST(FALSE, F, T); /* XNOR (FALSE, TRUE) -> FALSE */ + ASSERT_CONST(FALSE, T, F); /* XNOR (TRUE, FALSE) -> FALSE */ + ASSERT_CONST(TRUE, T, T); /* XNOR (TRUE, TRUE) -> TRUE */ + + ASSERT_EVAL2(TRUE, F, F); /* XNOR (var(FALSE), var(FALSE)) => TRUE */ + ASSERT_EVAL2(FALSE, F, T); /* XNOR (var(FALSE), var(TRUE)) => FALSE */ + ASSERT_EVAL2(FALSE, T, F); /* XNOR (var(TRUE), var(FALSE)) => FALSE */ + ASSERT_EVAL2(TRUE, T, T); /* XNOR (var(TRUE), var(TRUE)) => TRUE */ + +#ifndef USE_TWO + + ASSERT_CONST(FALSE, F, F, F); /* XNOR (FALSE, FALSE, FALSE) -> FALSE */ + ASSERT_CONST(TRUE, F, F, T); /* XNOR (FALSE, FALSE, TRUE) -> TRUE */ + ASSERT_CONST(TRUE, F, T, F); /* XNOR (FALSE, TRUE, FALSE) -> TRUE */ + ASSERT_CONST(FALSE, F, T, T); /* XNOR (FALSE, TRUE, TRUE) -> FALSE */ + ASSERT_CONST(TRUE, T, F, F); /* XNOR (TRUE, FALSE, FALSE) -> TRUE */ + ASSERT_CONST(FALSE, T, F, T); /* XNOR (TRUE, FALSE, TRUE) -> FALSE */ + ASSERT_CONST(FALSE, T, T, F); /* XNOR (TRUE, TRUE, FALSE) -> FALSE */ + ASSERT_CONST(TRUE, T, T, T); /* XNOR (TRUE, TRUE, TRUE) -> TRUE */ + + ASSERT_EVAL3(FALSE, F, F, F); /* XNOR (var(FALSE), var(FALSE), var(FALSE)) => FALSE */ + ASSERT_EVAL3(TRUE, F, F, T); /* XNOR (var(FALSE), var(FALSE), var(TRUE)) => TRUE */ + ASSERT_EVAL3(TRUE, F, T, F); /* XNOR (var(FALSE), var(TRUE), var(FALSE)) => TRUE */ + ASSERT_EVAL3(FALSE, F, T, T); /* XNOR (var(FALSE), var(TRUE), var(TRUE)) => FALSE */ + ASSERT_EVAL3(TRUE, T, F, F); /* XNOR (var(TRUE), var(FALSE), var(FALSE)) => TRUE */ + ASSERT_EVAL3(FALSE, T, F, T); /* XNOR (var(TRUE), var(FALSE), var(TRUE)) => FALSE */ + ASSERT_EVAL3(FALSE, T, T, F); /* XNOR (var(TRUE), var(TRUE), var(FALSE)) => FALSE */ + ASSERT_EVAL3(TRUE, T, T, T); /* XNOR (var(TRUE), var(TRUE), var(TRUE)) => TRUE */ + + /* XNOR (x) -> x */ + ASSUME(a = XNOR(REF(v1))); + ASSERT(a == v1); + ASSERT(a->refcount == 2); + libnormalform_free(a); + +#endif + + /* XNOR (x, FALSE) -> NOT x */ + ASSUME(a = XNOR(REF(v1), F)); + ASSERT_INVEQUAL(a, v1); + libnormalform_free(a); + + /* XNOR (FALSE, x) -> NOT x */ + ASSUME(a = XNOR(F, REF(v1))); + ASSERT_INVEQUAL(a, v1); + libnormalform_free(a); + + /* XNOR (x, TRUE) -> x */ + ASSUME(a = XNOR(REF(v1), T)); + ASSERT_EQUAL(a, v1); + libnormalform_free(a); + + /* XNOR (TRUE, x) -> x */ + ASSUME(a = XNOR(T, REF(v1))); + ASSERT_EQUAL(a, v1); + libnormalform_free(a); + +#ifndef USE_TWO + + /* XNOR (x, FALSE, FALSE) -> x */ + ASSUME(a = XNOR(REF(v1), F, F)); + ASSERT_EQUAL(a, v1); + ASSERT(a == v1); + libnormalform_free(a); + + /* XNOR (x, FALSE, TRUE) -> NOT x */ + ASSUME(a = XNOR(REF(v1), F, T)); + ASSERT_INVEQUAL(a, v1); + libnormalform_free(a); + + /* XNOR (x, TRUE, FALSE) -> NOT x */ + ASSUME(a = XNOR(REF(v1), T, F)); + ASSERT_INVEQUAL(a, v1); + libnormalform_free(a); + + /* XNOR (x, TRUE, TRUE) -> x */ + ASSUME(a = XNOR(REF(v1), T, T)); + ASSERT_EQUAL(a, v1); + ASSERT(a == v1); + libnormalform_free(a); + + /* XNOR (FALSE, x, FALSE) -> x */ + ASSUME(a = XNOR(F, REF(v1), F)); + ASSERT_EQUAL(a, v1); + ASSERT(a == v1); + libnormalform_free(a); + + /* XNOR (FALSE, x, TRUE) -> NOT x */ + ASSUME(a = XNOR(F, REF(v1), T)); + ASSERT_INVEQUAL(a, v1); + libnormalform_free(a); + + /* XNOR (TRUE, x, FALSE) -> NOT x */ + ASSUME(a = XNOR(T, REF(v1), F)); + ASSERT_INVEQUAL(a, v1); + libnormalform_free(a); + + /* XNOR (TRUE, x, TRUE) -> x */ + ASSUME(a = XNOR(T, REF(v1), T)); + ASSERT_EQUAL(a, v1); + ASSERT(a == v1); + libnormalform_free(a); + + /* XNOR (FALSE, FALSE, x) -> x */ + ASSUME(a = XNOR(F, F, REF(v1))); + ASSERT_EQUAL(a, v1); + ASSERT(a == v1); + libnormalform_free(a); + + /* XNOR (FALSE, TRUE, x) -> NOT x */ + ASSUME(a = XNOR(F, T, REF(v1))); + ASSERT_INVEQUAL(a, v1); + libnormalform_free(a); + + /* XNOR (TRUE, FALSE, x) -> NOT x */ + ASSUME(a = XNOR(T, F, REF(v1))); + ASSERT_INVEQUAL(a, v1); + libnormalform_free(a); + + /* XNOR (TRUE, TRUE, x) -> x */ + ASSUME(a = XNOR(T, T, REF(v1))); + ASSERT_EQUAL(a, v1); + ASSERT(a == v1); + libnormalform_free(a); + +#endif + + /* XNOR (x, x) -> TRUE */ + ASSUME(a = XNOR(REF(v1), REF(v1))); + ASSERT(a->type == TYPE_TRUE); + libnormalform_free(a); + +#ifndef USE_TWO + + /* XNOR (x, x, FALSE) -> FALSE */ + ASSUME(a = XNOR(REF(v1), REF(v1), F)); + ASSERT(a->type == TYPE_FALSE); + libnormalform_free(a); + + /* XNOR (x, x, FALSE, FALSE) -> TRUE */ + ASSUME(a = XNOR(REF(v1), REF(v1), F, F)); + ASSERT(a->type == TYPE_TRUE); + libnormalform_free(a); + + /* XNOR (x, x, TRUE) -> TRUE */ + ASSUME(a = XNOR(REF(v1), REF(v1), T)); + ASSERT(a->type == TYPE_TRUE); + libnormalform_free(a); + +#endif + + /* XNOR (x, NOT x) -> FALSE */ + ASSUME(a = libnormalform_not(REF(v1))); + ASSUME(a = XNOR(REF(v1), a)); + ASSERT(a->type == TYPE_FALSE); + libnormalform_free(a); + +#ifndef USE_TWO + + /* XNOR (x, NOT x, FALSE) -> TRUE */ + ASSUME(a = libnormalform_not(REF(v1))); + ASSUME(a = XNOR(REF(v1), a, F)); + ASSERT(a->type == TYPE_TRUE); + libnormalform_free(a); + + /* XNOR (x, NOT x, FALSE, FALSE) -> FALSE */ + ASSUME(a = libnormalform_not(REF(v1))); + ASSUME(a = XNOR(REF(v1), a, F, F)); + ASSERT(a->type == TYPE_FALSE); + libnormalform_free(a); + + /* XNOR (x, NOT x, TRUE) -> FALSE */ + ASSUME(a = libnormalform_not(REF(v1))); + ASSUME(a = XNOR(REF(v1), a, T)); + ASSERT(a->type == TYPE_FALSE); + libnormalform_free(a); + +#endif + + /* XNOR (x, y) -> NOT XOR (x, y) */ + ASSUME(a = XNOR(REF(v1), REF(v2))); + ASSUME(b = libnormalform_xor2(REF(v1), REF(v2))); + ASSERT_INVEQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + +#ifndef USE_TWO + + /* XNOR (x, y, z) -> NOT XOR (NOT XOR (x, y), z) */ + ASSUME(a = XNOR(REF(v1), REF(v2), REF(v3))); + ASSUME(b = libnormalform_xor2(REF(v1), REF(v2))); + ASSUME(b = libnormalform_not(b)); + ASSUME(b = libnormalform_xor2(b, REF(v3))); + ASSERT_INVEQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + +#endif + + /* XNOR (x, y) -> OR (AND (x, y), AND (NOT x, NOT y)) */ + ASSUME(a = libnormalform_not(REF(v1))); + ASSUME(b = libnormalform_not(REF(v2))); + ASSUME(b = libnormalform_and2(a, b)); + ASSUME(a = libnormalform_and2(REF(v1), REF(v2))); + ASSUME(b = libnormalform_or2__(a, b)); + ASSUME(a = XNOR(REF(v1), REF(v2))); + ASSERT(a->type == TYPE_XOR); + ASSERT(b->type == TYPE_OR); + ASSERT_EQUAL(a, b); + ASSERT_EQUAL(b, a); + libnormalform_free(a); + libnormalform_free(b); + + /* XNOR (x, y) -> AND (OR (x, NOT y), OR (NOT x, y)) */ + ASSUME(a = libnormalform_not(REF(v2))); + ASSUME(a = libnormalform_or2(REF(v1), a)); + ASSUME(b = libnormalform_not(REF(v1))); + ASSUME(b = libnormalform_or2(b, REF(v2))); + ASSUME(b = libnormalform_and2__(a, b)); + ASSUME(a = XNOR(REF(v1), REF(v2))); + ASSERT(a->type == TYPE_XOR); + ASSERT(b->type == TYPE_AND); + ASSERT_EQUAL(a, b); + ASSERT_EQUAL(b, a); + libnormalform_free(a); + libnormalform_free(b); + + /* XNOR (x, y) -> OR (AND (x, y), AND (NOT x, NOT y)) */ + ASSUME(a = libnormalform_not(REF(v1))); + ASSUME(b = libnormalform_not(REF(v2))); + ASSUME(b = libnormalform_and2(a, b)); + ASSUME(a = libnormalform_and2(REF(v1), REF(v2))); + ASSUME(b = libnormalform_or2(a, b)); + ASSUME(a = XNOR(REF(v1), REF(v2))); + ASSERT(a->type == TYPE_XOR); + ASSERT(b->type == TYPE_XOR); + ASSERT_EQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* XNOR (x, y) -> AND (OR (x, NOT y), OR (NOT x, y)) */ + ASSUME(a = libnormalform_not(REF(v2))); + ASSUME(a = libnormalform_or2(REF(v1), a)); + ASSUME(b = libnormalform_not(REF(v1))); + ASSUME(b = libnormalform_or2(b, REF(v2))); + ASSUME(b = libnormalform_and2(a, b)); + ASSUME(a = XNOR(REF(v1), REF(v2))); + ASSERT(a->type == TYPE_XOR); + ASSERT(b->type == TYPE_XOR); + ASSERT_EQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* XNOR (x, y) -> OR (AND (NOT x, NOT y), AND (x, y)) */ + ASSUME(a = libnormalform_not(REF(v1))); + ASSUME(b = libnormalform_not(REF(v2))); + ASSUME(b = libnormalform_and2(a, b)); + ASSUME(a = libnormalform_and2(REF(v1), REF(v2))); + ASSUME(b = libnormalform_or2__(b, a)); + ASSUME(a = XNOR(REF(v1), REF(v2))); + ASSERT(a->type == TYPE_XOR); + ASSERT(b->type == TYPE_OR); + ASSERT_EQUAL(a, b); + ASSERT_EQUAL(b, a); + libnormalform_free(a); + libnormalform_free(b); + + /* XNOR (x, y) -> AND (OR (NOT x, y), OR (x, NOT y)) */ + ASSUME(a = libnormalform_not(REF(v2))); + ASSUME(a = libnormalform_or2(REF(v1), a)); + ASSUME(b = libnormalform_not(REF(v1))); + ASSUME(b = libnormalform_or2(b, REF(v2))); + ASSUME(b = libnormalform_and2__(b, a)); + ASSUME(a = XNOR(REF(v1), REF(v2))); + ASSERT(a->type == TYPE_XOR); + ASSERT(b->type == TYPE_AND); + ASSERT_EQUAL(a, b); + ASSERT_EQUAL(b, a); + libnormalform_free(a); + libnormalform_free(b); + + /* XNOR (x, y) -> OR (AND (NOT x, NOT y), AND (x, y)) */ + ASSUME(a = libnormalform_not(REF(v1))); + ASSUME(b = libnormalform_not(REF(v2))); + ASSUME(b = libnormalform_and2(a, b)); + ASSUME(a = libnormalform_and2(REF(v1), REF(v2))); + ASSUME(b = libnormalform_or2(b, a)); + ASSUME(a = XNOR(REF(v1), REF(v2))); + ASSERT(a->type == TYPE_XOR); + ASSERT(b->type == TYPE_XOR); + ASSERT_EQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* XNOR (x, y) -> AND (OR (NOT x, y), OR (x, NOT y)) */ + ASSUME(a = libnormalform_not(REF(v2))); + ASSUME(a = libnormalform_or2(REF(v1), a)); + ASSUME(b = libnormalform_not(REF(v1))); + ASSUME(b = libnormalform_or2(b, REF(v2))); + ASSUME(b = libnormalform_and2(b, a)); + ASSUME(a = XNOR(REF(v1), REF(v2))); + ASSERT(a->type == TYPE_XOR); + ASSERT(b->type == TYPE_XOR); + ASSERT_EQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + +#undef T +#undef F +#undef TV +#undef FV + +#undef ASSERT_CONST +#undef ASSERT_EVAL2 +#undef ASSERT_EVAL3 + + libnormalform_free(v1); + libnormalform_free(v2); + libnormalform_free(v3); + libnormalform_free(ts); + libnormalform_free(fs); + + TEST_END; +} + + +#endif -- cgit v1.3.1