First commit

Signed-off-by: Mattias Andrée <maandree@kth.se>

1 files changed, 437 insertions, 0 deletions

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