1 files changed, 156 insertions, 0 deletions
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