First commit

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

1 files changed, 235 insertions, 0 deletions

diff --git a/libnormalform_nor.c b/libnormalform_nor.c
new file mode 100644
index 0000000..dbee41b
--- /dev/null
+++ b/libnormalform_nor.c
@@ -0,0 +1,235 @@
+/* See LICENSE file for copyright and license details. */
+#include "common.h"
+#ifndef TEST
+
+
+LIBNORMALFORM_SENTENCE *
+(libnormalform_nor)(LIBNORMALFORM_SENTENCE **xs)
+{
+	LIBNORMALFORM_SENTENCE *x, *ret;
+	int inv;
+
+	/* 0 ⊽ x = ¬x, but 1 ⊽ x = 0, so at least one argument is required */
+	ret = *xs++;
+	if (!ret) {
+		errno = EDOM;
+		return NULL;
+	}
+
+	for (; (x = *xs); xs++) {
+		if (!ret) {
+			/* error handling */
+			libnormalform_free(x);
+
+		} else if (x->type == TYPE_TRUE || ret->type == TYPE_TRUE) {
+		set_to_false:
+			/* x ⊽ 1 = 1 ⊽ x = 0 */
+			libnormalform_free(ret);
+			libnormalform_free(x);
+			ret = libnormalform_false();
+
+		} else if (x->type == TYPE_FALSE) {
+			/* x ⊽ 0 = ¬x */
+			libnormalform_free(x);
+			ret = libnormalform_not(ret);
+
+		} else if (ret->type == TYPE_FALSE) {
+		set_to_not_x:
+			/* 0 ⊽ x = ¬x */
+			libnormalform_free(ret);
+			ret = libnormalform_not(x);
+
+		} else if (ret->equals(ret, x, &inv)) {
+			if (!inv) {
+				/* x ⊽ x = ¬x */
+				goto set_to_not_x;
+			} else {
+				/* x ⊽ ¬x = 0 */
+				goto set_to_false;
+			}
+
+		} else {
+			/* a ⊽ b = ¬(a ∨ b) = ¬a ∧ ¬b */
+			ret = libnormalform_and2(libnormalform_not(ret), libnormalform_not(x));
+		}
+	}
+
+	return ret;
+}
+
+
+#else
+
+
+#define NOR(...) LIBNORMALFORM_NOR(__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(!NOR(REF(v1), NULL) && errno == 0);
+	errno = 1;
+	ASSERT(!NOR(REF(v1), NULL) && errno == 1);
+	errno = 0;
+	ASSERT(!NOR(NULL, REF(v1)) && errno == 0);
+	errno = 1;
+	ASSERT(!NOR(NULL, REF(v1)) && errno == 1);
+	errno = 0;
+	ASSERT(!NOR(NULL, NULL) && errno == 0);
+	errno = 1;
+	ASSERT(!NOR(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 = NOR(__VA_ARGS__));\
+		ASSERT(a->type == TYPE_##VALUE);\
+		libnormalform_free(a);\
+	} while (0)
+
+#define ASSERT_EVAL2(VALUE, V1, V2)\
+	do {\
+		ASSUME(a = NOR(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)
+
+#ifndef USE_TWO
+
+#if defined(__GNUC__)
+# pragma GCC diagnostic push
+# pragma GCC diagnostic ignored "-Wformat"
+#endif
+
+	/* NOR () -> EDOM */
+	errno = 0;
+	ASSERT(!NOR() && errno == EDOM);
+
+#if defined(__GNUC__)
+# pragma GCC diagnostic pop
+#endif
+
+	ASSERT_CONST(TRUE, T);  /* NOR (TRUE) -> TRUE */
+	ASSERT_CONST(FALSE, F); /* NOR (FALSE) -> FALSE */
+
+#endif
+
+	ASSERT_CONST(TRUE,  F, F); /* NOR (FALSE, FALSE) -> TRUE */
+	ASSERT_CONST(FALSE, F, T); /* NOR (FALSE, TRUE) -> FALSE */
+	ASSERT_CONST(FALSE, T, F); /* NOR (TRUE, FALSE) -> FALSE */
+	ASSERT_CONST(FALSE, T, T); /* NOR (TRUE, TRUE) -> FALSE */
+
+	ASSERT_EVAL2(TRUE,  F, F); /* NOR (var(FALSE), var(FALSE)) => TRUE */
+	ASSERT_EVAL2(FALSE, F, T); /* NOR (var(FALSE), var(TRUE)) => FALSE */
+	ASSERT_EVAL2(FALSE, T, F); /* NOR (var(TRUE), var(FALSE)) => FALSE */
+	ASSERT_EVAL2(FALSE, T, T); /* NOR (var(TRUE), var(TRUE)) => FALSE */
+
+#ifndef USE_TWO
+
+	/* NOR (x) -> x */
+	ASSUME(a = NOR(REF(v1)));
+	ASSERT(a == v1);
+	ASSERT(a->refcount == 2);
+	libnormalform_free(a);
+
+#endif
+
+	/* NOR (x, TRUE) -> FALSE */
+	ASSUME(a = NOR(REF(v1), T));
+	ASSERT(a->type == TYPE_FALSE);
+	libnormalform_free(a);
+
+	/* NOR (TRUE, x) -> FALSE */
+	ASSUME(a = NOR(T, REF(v1)));
+	ASSERT(a->type == TYPE_FALSE);
+	libnormalform_free(a);
+
+	/* NOR (x, FALSE) -> NOT x */
+	ASSUME(a = NOR(REF(v1), F));
+	ASSERT_INVEQUAL(a, v1);
+	libnormalform_free(a);
+
+	/* NOR (FALSE, x) -> NOT x */
+	ASSUME(a = NOR(F, REF(v1)));
+	ASSERT_INVEQUAL(a, v1);
+	libnormalform_free(a);
+
+	/* NOR (x, x) -> NOT x */
+	ASSUME(a = NOR(REF(v1), REF(v1)));
+	ASSERT_INVEQUAL(a, v1);
+	libnormalform_free(a);
+
+	/* NOR (x, NOT x) -> FALSE x */
+	ASSUME(a = libnormalform_not(REF(v1)));
+	ASSUME(a = NOR(REF(v1), a));
+	ASSERT(a->type == TYPE_FALSE);
+	libnormalform_free(a);
+
+	/* NOR (x, y) -> NOT OR (x, y) */
+	ASSUME(b = libnormalform_or2(REF(v1), REF(v2)));
+	ASSUME(a = NOR(REF(v1), REF(v2)));
+	ASSERT_INVEQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* NOR (y, x) -> NOR (x, y) */
+	ASSUME(a = NOR(REF(v2), REF(v1)));
+	ASSUME(b = NOR(REF(v1), REF(v2)));
+	ASSERT_EQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+#ifndef USE_TWO
+
+	/* NOR (x, y, z) -> NOT OR (NOT OR (x, y), z) */
+	ASSUME(b = libnormalform_or2(REF(v1), REF(v2)));
+	ASSUME(b = libnormalform_not(b));
+	ASSUME(b = libnormalform_or2(b, REF(v3)));
+	ASSUME(a = NOR(REF(v1), REF(v2), REF(v3)));
+	ASSERT_INVEQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+#endif
+
+#undef T
+#undef F
+#undef TV
+#undef FV
+
+#undef ASSERT_CONST
+#undef ASSERT_EVAL2
+
+	libnormalform_free(v1);
+	libnormalform_free(v2);
+	libnormalform_free(v3);
+	libnormalform_free(ts);
+	libnormalform_free(fs);
+
+	TEST_END;
+}
+
+
+#endif