First commit

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

1 files changed, 115 insertions, 0 deletions

diff --git a/libnormalform_not.c b/libnormalform_not.c
new file mode 100644
index 0000000..fcc9604
--- /dev/null
+++ b/libnormalform_not.c
@@ -0,0 +1,115 @@
+/* See LICENSE file for copyright and license details. */
+#include "common.h"
+#ifndef TEST
+
+
+LIBNORMALFORM_SENTENCE *
+(libnormalform_not)(LIBNORMALFORM_SENTENCE *x)
+{
+	LIBNORMALFORM_SENTENCE *ret;
+	if (!x)
+		return NULL;
+	ret = x->inverse(x);
+	libnormalform_free(x);
+	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;
+	int r1, r2;
+
+	var1.value = LIBNORMALFORM_FALSE;
+	var2.value = LIBNORMALFORM_TRUE;
+	fun1.evaluate = &tautology;
+	fun2.evaluate = &contradiction;
+	domain.nmappings = 0;
+
+	errno = 0;
+	ASSERT(!libnormalform_not(NULL) && errno == 0);
+	errno = 1;
+	ASSERT(!libnormalform_not(NULL) && errno == 1);
+
+	ASSUME(v1 = libnormalform_variable(&var1));
+	ASSUME(v2 = libnormalform_variable(&var2));
+	ASSUME(f1 = libnormalform_function(&fun1));
+	ASSUME(f2 = libnormalform_function(&fun2));
+
+#define CHECK(X)\
+	do {\
+		ASSUME(a = libnormalform_not(REF(X)));\
+		ASSERT((X)->refcount == 1);\
+		ASSERT(a->refcount == 1);\
+		ASSERT_INVEQUAL(a, (X));\
+		ASSERT((r1 = a->evaluate(a, NULL)) >= 0);\
+		ASSERT((r2 = (X)->evaluate((X), NULL)) >= 0);\
+		ASSERT(r1 == 1 - r2);\
+		libnormalform_free(a);\
+	} while (0)
+
+	CHECK(v1);
+	CHECK(f1);
+
+#undef CHECK
+
+#define CHECK(X)\
+	do {\
+		ASSUME(b = (X));\
+		ASSUME(a = libnormalform_not(REF(b)));\
+		ASSERT(b->refcount == 1);\
+		ASSERT(a->refcount == 1);\
+		ASSERT_INVEQUAL(a, b);\
+		ASSERT((r1 = a->evaluate(a, NULL)) >= 0);\
+		ASSERT((r2 = b->evaluate(b, NULL)) >= 0);\
+		ASSERT(r1 == 1 - r2);\
+		libnormalform_free(a);\
+		libnormalform_free(b);\
+	} while (0)
+
+	CHECK(libnormalform_and2(REF(v1), REF(v2)));
+	CHECK(libnormalform_or2(REF(v1), REF(v2)));
+	CHECK(libnormalform_xor2(REF(v1), REF(v2)));
+	CHECK(libnormalform_all(&domain, REF(f1), REF(f2)));
+	CHECK(libnormalform_any(&domain, REF(f1), REF(f2)));
+	CHECK(libnormalform_one(&domain, REF(f1), REF(f2)));
+
+#undef CHECK
+
+	libnormalform_free(v1);
+	libnormalform_free(v2);
+	libnormalform_free(f1);
+	libnormalform_free(f2);
+
+	TEST_END;
+}
+
+
+#endif