First commit

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

1 files changed, 419 insertions, 0 deletions

diff --git a/libnormalform_transformation.c b/libnormalform_transformation.c
new file mode 100644
index 0000000..3a1218b
--- /dev/null
+++ b/libnormalform_transformation.c
@@ -0,0 +1,419 @@
+/* See LICENSE file for copyright and license details. */
+#include "common.h"
+#ifndef TEST
+
+
+/** 
+ * See `.inverse` in `struct libnormalform_sentence` (Transformation function implementation)
+ */
+static LIBNORMALFORM_SENTENCE *
+trans_inverse(LIBNORMALFORM_SENTENCE *this)
+{
+	return libnormalform_transformation(this->data.trans.function, this->data.trans.input->inverse(this->data.trans.input));
+}
+
+
+/** 
+ * See `.equals` in `struct libnormalform_sentence` (Transformation function implementation)
+ */
+static int
+trans_equals(LIBNORMALFORM_SENTENCE *this, LIBNORMALFORM_SENTENCE *other, int *inv_out)
+{
+	if (other->type != TYPE_TRANS || this->data.trans.function != other->data.trans.function)
+		return 0;
+	return this->data.trans.input->equals(this->data.trans.input, other->data.trans.input, inv_out);
+}
+
+
+/** 
+ * See `.evaluate` in `struct libnormalform_sentence` (Transformation function implementation)
+ */
+static int
+trans_evaluate(LIBNORMALFORM_SENTENCE *this, void *input)
+{
+	int r;
+	input = this->data.trans.function->transform(this->data.trans.function->user_data, input);
+	if (!input)
+		return -1;
+	r = this->data.trans.input->evaluate(this->data.trans.input, input);
+	if (this->data.trans.function->deallocate)
+		this->data.trans.function->deallocate(this->data.trans.function->user_data, input);
+	return r;
+}
+
+
+LIBNORMALFORM_SENTENCE *
+(libnormalform_transformation)(struct libnormalform_transformer *function, LIBNORMALFORM_SENTENCE *sentence)
+{
+	static const struct libnormalform_sentence prototype = {
+		PROTOTYPE_COMMON,
+		.type = TYPE_TRANS,
+		.inverse = &trans_inverse,
+		.equals = &trans_equals,
+		.evaluate = &trans_evaluate
+	};
+
+	LIBNORMALFORM_SENTENCE *ret, *left, *right;
+	LIBNORMALFORM_SENTENCE *(*connective)(LIBNORMALFORM_SENTENCE *, LIBNORMALFORM_SENTENCE *);
+
+	if (!sentence)
+		return NULL;
+
+	function->builtin = LIBNORMALFORM_NOT_BUILT_IN;
+
+	switch (sentence->type) {
+	case TYPE_ALL:
+	case TYPE_ANY:
+	case TYPE_ONE:
+	case TYPE_NOT_ONE:
+		libnormalform_free(sentence);
+		errno = EDOM;
+		return NULL;
+
+	case TYPE_TRUE:
+	case TYPE_FALSE:
+	case TYPE_VARIABLE:
+		return sentence;
+
+	case TYPE_FUNCTION:
+	case TYPE_TRANS:
+		ret = malloc(sizeof(*ret));
+		if (!ret) {
+			libnormalform_free(sentence);
+			return NULL;
+		}
+		*ret = prototype;
+		ret->hash = TRANS_HASH(function, sentence);
+		ret->data.trans.function = function;
+		ret->data.trans.input = sentence;
+		return ret;
+
+	case TYPE_AND:
+		connective = &libnormalform_and2__;
+		break;
+	case TYPE_OR:
+		connective = &libnormalform_or2__;
+		break;
+	case TYPE_XOR:
+		connective = &libnormalform_xor2__;
+		break;
+
+	default:
+		abort();
+	}
+
+	left = LEFT(sentence), LEFT(sentence) = NULL;
+	right = RIGHT(sentence), RIGHT(sentence) = NULL;
+	libnormalform_free(sentence);
+	left = libnormalform_transformation(function, left);
+	if (!left) {
+		libnormalform_free(right);
+		return NULL;
+	}
+	right = libnormalform_transformation(function, right);
+	if (!right) {
+		libnormalform_free(left);
+		return NULL;
+	}
+
+	return (*connective)(left, right);
+}
+
+
+#else
+
+
+static void *
+uppercase(void *user_data, void *input)
+{
+	char *s = strdup(input), *p;
+	(void) user_data;
+	if (s)
+		for (p = s; *p; p++)
+			*p = (char)toupper(*p);
+	return s;
+}
+
+
+static void *
+constuppercase(void *user_data, void *input)
+{
+	static char ret[] = "HELLO WORLD";
+	(void) user_data;
+	(void) input;
+	return ret;
+}
+
+
+static void *
+einval(void *user_data, void *input)
+{
+	(void) user_data;
+	(void) input;
+	errno = EINVAL;
+	return NULL;
+}
+
+
+static void
+deallocate(void *user_data, void *input)
+{
+	(void) user_data;
+	free(input);
+}
+
+
+static int
+validate(void *expected, void *input)
+{
+	return input ? !strcmp(input, expected) : (errno = EDOM, -1);
+}
+
+
+int
+main(void)
+{
+	TEST_BEGIN;
+
+	struct libnormalform_transformer trans1, trans2;
+	struct libnormalform_function fun1, fun2;
+	struct libnormalform_variable var1;
+	struct libnormalform_map dom1;
+	LIBNORMALFORM_SENTENCE *a, *b, *f1, *f2;
+
+	errno = 0;
+	ASSERT(!libnormalform_transformation(&trans1, NULL) && errno == 0);
+	errno = 1;
+	ASSERT(!libnormalform_transformation(&trans1, NULL) && errno == 1);
+
+	/* F(⊤) = ⊤ */
+	ASSUME(a = libnormalform_true());
+	ASSUME(b = libnormalform_transformation(&trans1, REF(a)));
+	ASSERT(b->refcount == 2);
+	ASSERT(b->type == TYPE_TRUE);
+	ASSERT(b == a);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* F(⊥) = ⊥ */
+	ASSUME(a = libnormalform_false());
+	ASSUME(b = libnormalform_transformation(&trans1, REF(a)));
+	ASSERT(b->refcount == 2);
+	ASSERT(b->type == TYPE_FALSE);
+	ASSERT(b == a);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* F(a) = a */
+	ASSUME(a = libnormalform_variable(&var1));
+	ASSUME(b = libnormalform_transformation(&trans1, REF(a)));
+	ASSERT(b->refcount == 2);
+	ASSERT(b->type == TYPE_VARIABLE);
+	ASSERT(b == a);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* F(f(x)) irreducible */
+	ASSUME(a = libnormalform_function(&fun1));
+	ASSUME(b = libnormalform_transformation(&trans1, REF(a)));
+	ASSERT(b->refcount == 1);
+	ASSERT(a->refcount == 2);
+	ASSERT(b->type == TYPE_TRANS);
+	ASSERT(b->data.trans.function == &trans1);
+	ASSERT(b->data.trans.input == a);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* F(f(x) ∧ g(x)) = F(f(x)) ∧ F(g(x)) */
+	ASSUME(a = libnormalform_function(&fun1));
+	ASSUME(b = libnormalform_function(&fun2));
+	ASSUME(a = libnormalform_and2(a, b));
+	ASSUME(b = libnormalform_transformation(&trans1, a));
+	ASSERT(b->refcount == 1);
+	ASSERT(b->type == TYPE_AND);
+	ASSERT(LEFT(b)->type == TYPE_TRANS);
+	ASSERT(RIGHT(b)->type == TYPE_TRANS);
+	ASSERT(LEFT(b)->refcount == 1);
+	ASSERT(RIGHT(b)->refcount == 1);
+	ASSERT(LEFT(b)->data.trans.function == &trans1);
+	ASSERT(RIGHT(b)->data.trans.function == &trans1);
+	ASSERT(LEFT(b)->data.trans.input);
+	ASSERT(RIGHT(b)->data.trans.input);
+	ASSERT(LEFT(b)->data.trans.input->type == TYPE_FUNCTION);
+	ASSERT(RIGHT(b)->data.trans.input->type == TYPE_FUNCTION);
+	ASSERT(LEFT(b)->data.trans.input != RIGHT(b)->data.trans.input);
+	libnormalform_free(b);
+
+	/* F(f(x) ∨ g(x)) = F(f(x)) ∨ F(g(x)) */
+	ASSUME(a = libnormalform_function(&fun1));
+	ASSUME(b = libnormalform_function(&fun2));
+	ASSUME(a = libnormalform_or2(a, b));
+	ASSUME(b = libnormalform_transformation(&trans1, a));
+	ASSERT(b->refcount == 1);
+	ASSERT(b->type == TYPE_OR);
+	ASSERT(LEFT(b)->type == TYPE_TRANS);
+	ASSERT(RIGHT(b)->type == TYPE_TRANS);
+	ASSERT(LEFT(b)->refcount == 1);
+	ASSERT(RIGHT(b)->refcount == 1);
+	ASSERT(LEFT(b)->data.trans.function == &trans1);
+	ASSERT(RIGHT(b)->data.trans.function == &trans1);
+	ASSERT(LEFT(b)->data.trans.input);
+	ASSERT(RIGHT(b)->data.trans.input);
+	ASSERT(LEFT(b)->data.trans.input->type == TYPE_FUNCTION);
+	ASSERT(RIGHT(b)->data.trans.input->type == TYPE_FUNCTION);
+	ASSERT(LEFT(b)->data.trans.input != RIGHT(b)->data.trans.input);
+	libnormalform_free(b);
+
+	/* F(f(x) ⊕ g(x)) = F(f(x)) ⊕ F(g(x)) */
+	ASSUME(a = libnormalform_function(&fun1));
+	ASSUME(b = libnormalform_function(&fun2));
+	ASSUME(a = libnormalform_xor2(a, b));
+	ASSUME(b = libnormalform_transformation(&trans1, a));
+	ASSERT(b->refcount == 1);
+	ASSERT(b->type == TYPE_XOR);
+	ASSERT(LEFT(b)->type == TYPE_TRANS);
+	ASSERT(RIGHT(b)->type == TYPE_TRANS);
+	ASSERT(LEFT(b)->refcount == 1);
+	ASSERT(RIGHT(b)->refcount == 1);
+	ASSERT(LEFT(b)->data.trans.function == &trans1);
+	ASSERT(RIGHT(b)->data.trans.function == &trans1);
+	ASSERT(LEFT(b)->data.trans.input);
+	ASSERT(RIGHT(b)->data.trans.input);
+	ASSERT(LEFT(b)->data.trans.input->type == TYPE_FUNCTION);
+	ASSERT(RIGHT(b)->data.trans.input->type == TYPE_FUNCTION);
+	ASSERT(LEFT(b)->data.trans.input != RIGHT(b)->data.trans.input);
+	libnormalform_free(b);
+
+	/* F(Q(q)∀{p,q}:P(p)) illegal construct */
+	ASSUME(a = libnormalform_function(&fun1));
+	ASSUME(b = libnormalform_function(&fun2));
+	ASSUME(a = libnormalform_all(&dom1, a, b));
+	errno = 0;
+	ASSERT(!libnormalform_transformation(&trans1, a) && errno == EDOM);
+
+	/* F(Q(q)∃{p,q}:P(p)) illegal construct */
+	ASSUME(a = libnormalform_function(&fun1));
+	ASSUME(b = libnormalform_function(&fun2));
+	ASSUME(a = libnormalform_any(&dom1, a, b));
+	errno = 0;
+	ASSERT(!libnormalform_transformation(&trans1, a) && errno == EDOM);
+
+	/* F(Q(q)∃!{p,q}:P(p)) illegal construct */
+	ASSUME(a = libnormalform_function(&fun1));
+	ASSUME(b = libnormalform_function(&fun2));
+	ASSUME(a = libnormalform_one(&dom1, a, b));
+	errno = 0;
+	ASSERT(!libnormalform_transformation(&trans1, a) && errno == EDOM);
+
+	/* F(¬(Q(q)∃!{p,q}:P(p))) illegal construct */
+	ASSUME(a = libnormalform_function(&fun1));
+	ASSUME(b = libnormalform_function(&fun2));
+	ASSUME(a = libnormalform_one(&dom1, a, b));
+	ASSUME(a = libnormalform_not(a));
+	errno = 0;
+	ASSERT(!libnormalform_transformation(&trans1, a) && errno == EDOM);
+
+	ASSUME(a = libnormalform_function(&fun1));
+	trans1.transform = &uppercase;
+	trans1.deallocate = &deallocate;
+
+	fun1.evaluate = validate;
+	ASSUME(fun1.user_data = strdup("hello world"));
+	ASSERT(a->evaluate(a, (char []){"hello world"}) == 1);
+	ASSERT(a->evaluate(a, (char []){"HELLO WORLD"}) == 0);
+	ASSERT(a->evaluate(a, (char []){"x"}) == 0);
+	errno = 0;
+	ASSERT(a->evaluate(a, NULL) == -1 && errno == EDOM);
+	free(fun1.user_data);
+
+	fun1.evaluate = validate;
+	ASSUME(fun1.user_data = strdup("HELLO WORLD"));
+	ASSUME(a = libnormalform_transformation(&trans1, a));
+	ASSERT(a->evaluate(a, (char []){"hello world"}) == 1);
+	ASSERT(a->evaluate(a, (char []){"HELLO WORLD"}) == 1);
+	ASSERT(a->evaluate(a, (char []){"x"}) == 0);
+	trans1.transform = constuppercase;
+	trans1.deallocate = NULL;
+	ASSERT(a->evaluate(a, (char []){"hello world"}) == 1);
+	free(fun1.user_data);
+
+	libnormalform_free(a);
+
+	ASSUME(f1 = libnormalform_function(&fun1));
+	ASSUME(f2 = libnormalform_function(&fun2));
+
+	ASSUME(a = libnormalform_transformation(&trans1, REF(f1)));
+	trans1.transform = einval;
+	trans1.deallocate = NULL;
+	errno = 0;
+	ASSERT(a->evaluate(a, (char []){"hello world"}) == -1 && errno == EINVAL);
+
+	ASSERT_NOTEQUAL(a, f1);
+
+	ASSUME(b = libnormalform_true());
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	ASSUME(b = libnormalform_true());
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	ASSUME(b = libnormalform_variable(&var1));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	ASSUME(b = libnormalform_transformation(&trans1, REF(f1)));
+	ASSERT_EQUAL(a, b);
+	libnormalform_free(b);
+
+	ASSUME(b = libnormalform_transformation(&trans1, libnormalform_not(REF(f1))));
+	ASSERT_INVEQUAL(a, b);
+	libnormalform_free(b);
+
+	ASSUME(b = libnormalform_transformation(&trans1, REF(f2)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	ASSUME(b = libnormalform_transformation(&trans2, REF(f1)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	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(&dom1, REF(f1), REF(f2)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	ASSUME(b = libnormalform_any(&dom1, REF(f1), REF(f2)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	ASSUME(b = libnormalform_one(&dom1, REF(f1), REF(f2)));
+	ASSERT_NOTEQUAL(a, b);
+	ASSUME(b = libnormalform_not(b));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	ASSUME(b = libnormalform_not(libnormalform_transformation(&trans1, REF(f1))));
+	ASSERT_INVEQUAL(a, b);
+	libnormalform_free(b);
+
+	libnormalform_free(a);
+	libnormalform_free(f1);
+	libnormalform_free(f2);
+
+	TEST_END;
+}
+
+
+#endif