1 files changed, 287 insertions, 0 deletions
diff --git a/libnormalform_function.c b/libnormalform_function.c
new file mode 100644
index 0000000..3978a4a
--- /dev/null
+++ b/libnormalform_function.c
@@ -0,0 +1,287 @@
+/* See LICENSE file for copyright and license details. */
+#include "common.h"
+#ifndef TEST
+
+
+/** 
+ * See `.inverse` in `struct libnormalform_sentence` (Function literal implementation)
+ */
+static LIBNORMALFORM_SENTENCE *
+function_inverse(LIBNORMALFORM_SENTENCE *this)
+{
+	LIBNORMALFORM_SENTENCE *ret = libnormalform_function(this->data.literal.atom.function);
+	if (ret)
+		ret->data.literal.inverted = this->data.literal.inverted ^ 1;
+	return ret;
+}
+
+
+/** 
+ * See `.equals` in `struct libnormalform_sentence` (Function literal implementation)
+ */
+static int
+function_equals(LIBNORMALFORM_SENTENCE *this, LIBNORMALFORM_SENTENCE *other, int *inv_out)
+{
+	if (other->type != TYPE_FUNCTION || this->data.literal.atom.function != other->data.literal.atom.function)
+		return 0;
+	*inv_out = this->data.literal.inverted ^ other->data.literal.inverted;
+	return 1;
+}
+
+
+/** 
+ * See `.evaluate` in `struct libnormalform_sentence` (Function literal implementation)
+ */
+static int
+function_evaluate(LIBNORMALFORM_SENTENCE *this, void *input)
+{
+	int r = this->data.literal.atom.function->evaluate(this->data.literal.atom.function->user_data, input);
+	return r < 0 ? r : ((r > 0) ^ this->data.literal.inverted);
+}
+
+
+LIBNORMALFORM_SENTENCE *
+(libnormalform_function)(struct libnormalform_function *function)
+{
+	static const struct libnormalform_sentence prototype = {
+		PROTOTYPE_COMMON,
+		.type = TYPE_FUNCTION,
+		.inverse = &function_inverse,
+		.equals = &function_equals,
+		.evaluate = &function_evaluate
+	};
+
+	LIBNORMALFORM_SENTENCE *ret = malloc(sizeof(*ret));
+	if (ret) {
+		*ret = prototype;
+		ret->hash = LITERAL_HASH(function);
+		ret->data.literal.atom.function = function;
+		ret->data.literal.inverted = 0;
+	}
+	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;
+}
+
+
+static int
+einval(void *user_data, void *input)
+{
+	(void) user_data;
+	(void) input;
+	errno = EINVAL;
+	return -1;
+}
+
+
+int
+main(void)
+{
+	TEST_BEGIN;
+
+	struct libnormalform_function fun1, fun2;
+	struct libnormalform_variable var1;
+	struct libnormalform_mapping map[1];
+	struct libnormalform_map domain;
+	LIBNORMALFORM_SENTENCE *a, *b, *v1, *f1, *f2;
+
+	domain.nmappings = 0;
+
+	ASSUME(a = libnormalform_function(&fun1));
+	ASSERT(a->refcount == 1);
+	ASSERT(a->travel_index == 0);
+	ASSERT(a->travel_count == 0);
+	ASSERT(a->type == TYPE_FUNCTION);
+	ASSERT(a->data.literal.inverted == 0);
+	ASSERT(a->data.literal.atom.function == &fun1);
+	ASSERT_EQUAL(a, a);
+	fun1.evaluate = tautology;
+	ASSERT(libnormalform_evaluate(a) == 1);
+	fun1.evaluate = contradiction;
+	ASSERT(libnormalform_evaluate(a) == 0);
+	fun1.evaluate = einval;
+	errno = 0;
+	ASSERT(libnormalform_evaluate(a) == -1 && errno == EINVAL);
+
+	ASSUME(b = libnormalform_function(&fun1));
+	ASSERT_EQUAL(a, b);
+	ASSUME(b = libnormalform_not(b));
+	ASSERT_INVEQUAL(a, b);
+	ASSERT_INVEQUAL(b, a);
+	libnormalform_free(b);
+
+	ASSUME(b = libnormalform_function(&fun2));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	ASSUME(b = libnormalform_true());
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	ASSUME(b = libnormalform_false());
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	ASSUME(v1 = libnormalform_variable(&var1));
+	ASSUME(f1 = libnormalform_function(&fun1));
+	ASSUME(f2 = libnormalform_function(&fun2));
+
+	ASSERT_NOTEQUAL(a, v1);
+
+	ASSUME(b = libnormalform_and2(REF(f1), REF(f2)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	ASSUME(b = libnormalform_or2(REF(f1), REF(f2)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	ASSUME(b = libnormalform_xor2(REF(f1), REF(f2)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	ASSUME(b = libnormalform_all(&domain, REF(f1), REF(f2)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	ASSUME(b = libnormalform_any(&domain, REF(f1), REF(f2)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	ASSUME(b = libnormalform_one(&domain, REF(f1), REF(f2)));
+	ASSERT_NOTEQUAL(a, b);
+	ASSUME(b = libnormalform_not(b));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	libnormalform_free(a);
+
+	ASSUME(a = libnormalform_function(&fun1));
+	ASSUME(b = libnormalform_function(&fun2));
+	ASSUME(a = libnormalform_and2(a, b));
+	fun1.evaluate = tautology;
+	fun2.evaluate = einval;
+	errno = 0;
+	ASSERT(libnormalform_evaluate(a) == -1 && errno == EINVAL);
+	fun1.evaluate = einval;
+	fun2.evaluate = tautology;
+	errno = 0;
+	ASSERT(libnormalform_evaluate(a) == -1 && errno == EINVAL);
+	fun1.evaluate = tautology;
+	fun2.evaluate = tautology;
+	ASSERT(libnormalform_evaluate(a) == 1);
+	libnormalform_free(a);
+
+	ASSUME(a = libnormalform_function(&fun1));
+	ASSUME(b = libnormalform_function(&fun2));
+	ASSUME(a = libnormalform_or2(a, b));
+	fun1.evaluate = contradiction;
+	fun2.evaluate = einval;
+	errno = 0;
+	ASSERT(libnormalform_evaluate(a) == -1 && errno == EINVAL);
+	fun1.evaluate = einval;
+	fun2.evaluate = contradiction;
+	errno = 0;
+	ASSERT(libnormalform_evaluate(a) == -1 && errno == EINVAL);
+	fun1.evaluate = contradiction;
+	fun2.evaluate = contradiction;
+	ASSERT(libnormalform_evaluate(a) == 0);
+	libnormalform_free(a);
+
+	ASSUME(a = libnormalform_function(&fun1));
+	ASSUME(b = libnormalform_function(&fun2));
+	ASSUME(a = libnormalform_xor2(a, b));
+	fun1.evaluate = contradiction;
+	fun2.evaluate = einval;
+	errno = 0;
+	ASSERT(libnormalform_evaluate(a) == -1 && errno == EINVAL);
+	fun1.evaluate = einval;
+	fun2.evaluate = contradiction;
+	errno = 0;
+	ASSERT(libnormalform_evaluate(a) == -1 && errno == EINVAL);
+	fun1.evaluate = contradiction;
+	fun2.evaluate = contradiction;
+	ASSERT(libnormalform_evaluate(a) == 0);
+	libnormalform_free(a);
+
+	domain.nmappings = 1;
+	domain.mappings = map;
+	map[0].key = NULL;
+	map[0].value = NULL;
+
+	ASSUME(a = libnormalform_function(&fun1));
+	ASSUME(b = libnormalform_function(&fun2));
+	ASSUME(a = libnormalform_all(&domain, a, b));
+	fun1.evaluate = tautology;
+	fun2.evaluate = einval;
+	errno = 0;
+	ASSERT(libnormalform_evaluate(a) == -1 && errno == EINVAL);
+	fun1.evaluate = einval;
+	fun2.evaluate = tautology;
+	errno = 0;
+	ASSERT(libnormalform_evaluate(a) == -1 && errno == EINVAL);
+	fun1.evaluate = tautology;
+	fun2.evaluate = tautology;
+	ASSERT(libnormalform_evaluate(a) == 1);
+	libnormalform_free(a);
+
+	ASSUME(a = libnormalform_function(&fun1));
+	ASSUME(b = libnormalform_function(&fun2));
+	ASSUME(a = libnormalform_any(&domain, a, b));
+	fun1.evaluate = tautology;
+	fun2.evaluate = einval;
+	errno = 0;
+	ASSERT(libnormalform_evaluate(a) == -1 && errno == EINVAL);
+	fun1.evaluate = einval;
+	fun2.evaluate = tautology;
+	errno = 0;
+	ASSERT(libnormalform_evaluate(a) == -1 && errno == EINVAL);
+	fun1.evaluate = tautology;
+	fun2.evaluate = tautology;
+	ASSERT(libnormalform_evaluate(a) == 1);
+	libnormalform_free(a);
+
+	ASSUME(a = libnormalform_function(&fun1));
+	ASSUME(b = libnormalform_function(&fun2));
+	ASSUME(a = libnormalform_one(&domain, a, b));
+	fun1.evaluate = tautology;
+	fun2.evaluate = einval;
+	errno = 0;
+	ASSERT(libnormalform_evaluate(a) == -1 && errno == EINVAL);
+	fun1.evaluate = einval;
+	fun2.evaluate = tautology;
+	errno = 0;
+	ASSERT(libnormalform_evaluate(a) == -1 && errno == EINVAL);
+	fun1.evaluate = tautology;
+	fun2.evaluate = tautology;
+	ASSERT(libnormalform_evaluate(a) == 1);
+	libnormalform_free(a);
+
+	libnormalform_free(v1);
+	libnormalform_free(f1);
+	libnormalform_free(f2);
+
+	TEST_END;
+}
+
+
+#endif