First commit

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

1 files changed, 710 insertions, 0 deletions

diff --git a/libnormalform_xor.c b/libnormalform_xor.c
new file mode 100644
index 0000000..451fbf9
--- /dev/null
+++ b/libnormalform_xor.c
@@ -0,0 +1,710 @@
+/* See LICENSE file for copyright and license details. */
+#include "common.h"
+#ifndef TEST
+
+
+/**
+ * Check if a sentence equivalent to a specific sentence
+ * or its inverse is in an array of sentences
+ * 
+ * @param   x          The sentence to look for
+ * @param   among      The array of sentences to look in
+ * @param   n          The number of sentences in `among`
+ * @param   index_out  Output parameter for the offset, in `among`,
+ *                     of the found sentence
+ * @param   inv_out    Output parameter for equivalency of `x` and the
+ *                     sentence found in `among`; set to 0 if the two
+ *                     are equivalent or 1 if `x` is equivalent to the
+ *                     inverse of the sentence found in `among`
+ * @return             1 if a sentence equivalent to `x` or its inverse
+ *                     was found, 0 otherwise
+ */
+static int
+find(LIBNORMALFORM_SENTENCE *x, LIBNORMALFORM_SENTENCE **among, size_t n, size_t *index_out, int *inv_out)
+{
+	for (*index_out = 0; *index_out < n; ++*index_out)
+		if (x->equals(x, among[*index_out], inv_out))
+			return 1;
+	return 0;
+}
+
+
+LIBNORMALFORM_SENTENCE *
+(libnormalform_xor)(LIBNORMALFORM_SENTENCE **xs)
+{
+	LIBNORMALFORM_SENTENCE *x, *ret, **saved = xs;
+	size_t n = 0, i;
+	int inv;
+
+	/* ⨁∅ = {⨁X ⊕ (x ⊕ x) = ⨁X ⊕ 0 = ⨁X ⇒ ⨁X = ⨁(X ∪ {x, x})} = x ⊕ x = 0 */
+	ret = libnormalform_false();
+
+	for (; (x = *xs); xs++) {
+		if (x->type == TYPE_FALSE) {
+			/* ⨁X ⊕ 0 = ⨁X */
+			libnormalform_free(x);
+
+		} else if (x->type == TYPE_TRUE) {
+			/* ⨁X ⊕ 1 = ¬⨁X */
+			libnormalform_free(x);
+		invert:
+			ret = libnormalform_not(ret);
+
+		} else if (find(x, saved, n, &i, &inv)) {
+			/* ⨁X ⊕ x ⊕  x = ⨁X ⊕ (x ⊕  x) = ⨁X ⊕ 0 =  ⨁X */
+			/* ⨁X ⊕ x ⊕ ¬x = ⨁X ⊕ (x ⊕ ¬x) = ⨁X ⊕ 1 = ¬⨁X */
+			libnormalform_free(saved[i]);
+			libnormalform_free(x);
+			saved[i] = saved[--n];
+			if (inv)
+				goto invert;
+
+		} else {
+			saved[n++] = x;
+		}
+	}
+
+	saved[n] = NULL;
+	/* ⨁(X ∪ x) = ⨁X ⊕ x */
+	for (; *saved; saved++)
+		ret = libnormalform_xor2(ret, *saved);
+
+	return ret;
+}
+
+
+#else
+
+
+#define XOR(...) LIBNORMALFORM_XOR(__VA_ARGS__)
+
+
+int
+main(void)
+{
+	TEST_BEGIN;
+
+	struct libnormalform_variable var1, var2, var3, var4;
+	struct libnormalform_function fun1, fun2;
+	struct libnormalform_map domain;
+	struct libnormalform_transformer trans;
+	LIBNORMALFORM_SENTENCE *a, *b, *v1, *v2, *v3, *v4, *f1, *f2;
+	LIBNORMALFORM_SENTENCE *ts, *fs;
+
+	ASSUME(v1 = libnormalform_variable(&var1));
+	ASSUME(v2 = libnormalform_variable(&var2));
+	ASSUME(v3 = libnormalform_variable(&var3));
+	ASSUME(v4 = libnormalform_variable(&var4));
+	ASSUME(f1 = libnormalform_function(&fun1));
+	ASSUME(f2 = libnormalform_function(&fun2));
+	ASSUME(ts = libnormalform_true());
+	ASSUME(fs = libnormalform_false());
+
+#ifdef USE_CHECKED_VERSION
+	errno = 0;
+	ASSERT(!XOR(REF(v1), NULL) && errno == 0);
+	errno = 1;
+	ASSERT(!XOR(REF(v1), NULL) && errno == 1);
+	errno = 0;
+	ASSERT(!XOR(NULL, REF(v1)) && errno == 0);
+	errno = 1;
+	ASSERT(!XOR(NULL, REF(v1)) && errno == 1);
+	errno = 0;
+	ASSERT(!XOR(NULL, NULL) && errno == 0);
+	errno = 1;
+	ASSERT(!XOR(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 = XOR(__VA_ARGS__));\
+		ASSERT(a->type == TYPE_##VALUE);\
+		libnormalform_free(a);\
+	} while (0)
+
+#define ASSERT_EVAL2(VALUE, V1, V2)\
+	do {\
+		ASSUME(a = XOR(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)
+
+#define ASSERT_EVAL3(VALUE, V1, V2, V3)\
+	do {\
+		ASSUME(a = XOR(REF(v1), REF(v2), REF(v3)));\
+		ASSERT(a->type != TYPE_TRUE && a->type != TYPE_FALSE);\
+		var1.value = V1##V;\
+		var2.value = V2##V;\
+		var3.value = V3##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
+
+	ASSERT_CONST(FALSE); /* XOR () -> FALSE */
+
+#if defined(__GNUC__)
+# pragma GCC diagnostic pop
+#endif
+
+	ASSERT_CONST(TRUE, T);  /* XOR (TRUE) -> TRUE */
+	ASSERT_CONST(FALSE, F); /* XOR (FALSE) -> FALSE */
+
+#endif
+
+	ASSERT_CONST(FALSE, F, F); /* XOR (FALSE, FALSE) -> FALSE */
+	ASSERT_CONST(TRUE,  F, T); /* XOR (FALSE, TRUE) -> TRUE */
+	ASSERT_CONST(TRUE,  T, F); /* XOR (TRUE, FALSE) -> TRUE */
+	ASSERT_CONST(FALSE, T, T); /* XOR (TRUE, TRUE) -> FALSE */
+
+	ASSERT_EVAL2(FALSE, F, F); /* XOR (var(FALSE), var(FALSE)) => FALSE */
+	ASSERT_EVAL2(TRUE,  F, T); /* XOR (var(FALSE), var(TRUE)) => TRUE */
+	ASSERT_EVAL2(TRUE,  T, F); /* XOR (var(TRUE), var(FALSE)) => TRUE */
+	ASSERT_EVAL2(FALSE, T, T); /* XOR (var(TRUE), var(TRUE)) => FALSE */
+
+#ifndef USE_TWO
+
+	ASSERT_CONST(FALSE, F, F, F); /* XOR (FALSE, FALSE, FALSE) -> FALSE */
+	ASSERT_CONST(TRUE,  F, F, T); /* XOR (FALSE, FALSE, TRUE) -> TRUE */
+	ASSERT_CONST(TRUE,  F, T, F); /* XOR (FALSE, TRUE, FALSE) -> TRUE */
+	ASSERT_CONST(FALSE, F, T, T); /* XOR (FALSE, TRUE, TRUE) -> FALSE */
+	ASSERT_CONST(TRUE,  T, F, F); /* XOR (TRUE, FALSE, FALSE) -> TRUE */
+	ASSERT_CONST(FALSE, T, F, T); /* XOR (TRUE, FALSE, TRUE) -> FALSE */
+	ASSERT_CONST(FALSE, T, T, F); /* XOR (TRUE, TRUE, FALSE) -> FALSE */
+	ASSERT_CONST(TRUE,  T, T, T); /* XOR (TRUE, TRUE, TRUE) -> TRUE */
+
+	ASSERT_EVAL3(FALSE, F, F, F); /* XOR (var(FALSE), var(FALSE), var(FALSE)) => FALSE */
+	ASSERT_EVAL3(TRUE,  F, F, T); /* XOR (var(FALSE), var(FALSE), var(TRUE)) => TRUE */
+	ASSERT_EVAL3(TRUE,  F, T, F); /* XOR (var(FALSE), var(TRUE), var(FALSE)) => TRUE */
+	ASSERT_EVAL3(FALSE, F, T, T); /* XOR (var(FALSE), var(TRUE), var(TRUE)) => FALSE */
+	ASSERT_EVAL3(TRUE,  T, F, F); /* XOR (var(TRUE), var(FALSE), var(FALSE)) => TRUE */
+	ASSERT_EVAL3(FALSE, T, F, T); /* XOR (var(TRUE), var(FALSE), var(TRUE)) => FALSE */
+	ASSERT_EVAL3(FALSE, T, T, F); /* XOR (var(TRUE), var(TRUE), var(FALSE)) => FALSE */
+	ASSERT_EVAL3(TRUE,  T, T, T); /* XOR (var(TRUE), var(TRUE), var(TRUE)) => TRUE */
+
+	/* XOR (x) -> x */
+	ASSUME(a = XOR(REF(v1)));
+	ASSERT(a == v1);
+	ASSERT(a->refcount == 2);
+	libnormalform_free(a);
+
+#endif
+
+	/* XOR (x, TRUE) -> NOT x */
+	ASSUME(a = XOR(REF(v1), T));
+	ASSERT_INVEQUAL(a, v1);
+	libnormalform_free(a);
+
+	/* XOR (TRUE, x) -> NOT x */
+	ASSUME(a = XOR(T, REF(v1)));
+	ASSERT_INVEQUAL(a, v1);
+	libnormalform_free(a);
+
+	/* XOR (x, FALSE) -> x */
+	ASSUME(a = XOR(REF(v1), F));
+	ASSERT_EQUAL(a, v1);
+	ASSERT(a == v1);
+	libnormalform_free(a);
+
+	/* XOR (FALSE, x) -> x */
+	ASSUME(a = XOR(F, REF(v1)));
+	ASSERT_EQUAL(a, v1);
+	ASSERT(a == v1);
+	libnormalform_free(a);
+
+#ifndef USE_TWO
+
+	/* XOR (x, FALSE, FALSE) -> x */
+	ASSUME(a = XOR(REF(v1), F, F));
+	ASSERT_EQUAL(a, v1);
+	ASSERT(a == v1);
+	libnormalform_free(a);
+
+	/* XOR (x, FALSE, TRUE) -> NOT x */
+	ASSUME(a = XOR(REF(v1), F, T));
+	ASSERT_INVEQUAL(a, v1);
+	libnormalform_free(a);
+
+	/* XOR (x, TRUE, FALSE) -> NOT x */
+	ASSUME(a = XOR(REF(v1), T, F));
+	ASSERT_INVEQUAL(a, v1);
+	libnormalform_free(a);
+
+	/* XOR (x, TRUE, TRUE) -> x */
+	ASSUME(a = XOR(REF(v1), T, T));
+	ASSERT_EQUAL(a, v1);
+	ASSERT(a == v1);
+	libnormalform_free(a);
+
+	/* XOR (FALSE, x, FALSE) -> x */
+	ASSUME(a = XOR(F, REF(v1), F));
+	ASSERT_EQUAL(a, v1);
+	ASSERT(a == v1);
+	libnormalform_free(a);
+
+	/* XOR (FALSE, x, TRUE) -> NOT x */
+	ASSUME(a = XOR(F, REF(v1), T));
+	ASSERT_INVEQUAL(a, v1);
+	libnormalform_free(a);
+
+	/* XOR (TRUE, x, FALSE) -> NOT x */
+	ASSUME(a = XOR(T, REF(v1), F));
+	ASSERT_INVEQUAL(a, v1);
+	libnormalform_free(a);
+
+	/* XOR (TRUE, x, TRUE) -> x */
+	ASSUME(a = XOR(T, REF(v1), T));
+	ASSERT_EQUAL(a, v1);
+	ASSERT(a == v1);
+	libnormalform_free(a);
+
+	/* XOR (FALSE, FALSE, x) -> x */
+	ASSUME(a = XOR(F, F, REF(v1)));
+	ASSERT_EQUAL(a, v1);
+	ASSERT(a == v1);
+	libnormalform_free(a);
+
+	/* XOR (FALSE, TRUE, x) -> NOT x */
+	ASSUME(a = XOR(F, T, REF(v1)));
+	ASSERT_INVEQUAL(a, v1);
+	libnormalform_free(a);
+
+	/* XOR (TRUE, FALSE, x) -> NOT x */
+	ASSUME(a = XOR(T, F, REF(v1)));
+	ASSERT_INVEQUAL(a, v1);
+	libnormalform_free(a);
+
+	/* XOR (TRUE, TRUE, x) -> x */
+	ASSUME(a = XOR(T, T, REF(v1)));
+	ASSERT_EQUAL(a, v1);
+	ASSERT(a == v1);
+	libnormalform_free(a);
+
+#endif
+
+	/* XOR (x, x) -> FALSE */
+	ASSUME(a = XOR(REF(v1), REF(v1)));
+	ASSERT(a->type == TYPE_FALSE);
+	libnormalform_free(a);
+
+#ifndef USE_TWO
+
+	/* XOR (x, x, FALSE) -> FALSE */
+	ASSUME(a = XOR(REF(v1), REF(v1), F));
+	ASSERT(a->type == TYPE_FALSE);
+	libnormalform_free(a);
+
+	/* XOR (x, x, FALSE, FALSE) -> FALSE */
+	ASSUME(a = XOR(REF(v1), REF(v1), F, F));
+	ASSERT(a->type == TYPE_FALSE);
+	libnormalform_free(a);
+
+	/* XOR (x, x, TRUE) -> TRUE */
+	ASSUME(a = XOR(REF(v1), REF(v1), T));
+	ASSERT(a->type == TYPE_TRUE);
+	libnormalform_free(a);
+
+#endif
+
+	/* XOR (x, NOT x) -> TRUE */
+	ASSUME(a = libnormalform_not(REF(v1)));
+	ASSUME(a = XOR(REF(v1), a));
+	ASSERT(a->type == TYPE_TRUE);
+	libnormalform_free(a);
+
+	/* XOR (x, y) -> XOR (x, y) */
+	ASSUME(a = XOR(REF(v1), REF(v2)));
+	ASSUME(b = XOR(REF(v1), REF(v2)));
+	ASSERT_EQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* XOR (y, x) -> XOR (x, y) */
+	ASSUME(a = XOR(REF(v2), REF(v1)));
+	ASSUME(b = XOR(REF(v1), REF(v2)));
+	ASSERT_EQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+#ifndef USE_TWO
+
+	/* XOR (TRUE, x, y) -> NOT XOR (x, y) */
+	ASSUME(a = XOR(T, REF(v1), REF(v2)));
+	ASSUME(b = XOR(REF(v1), REF(v2)));
+	ASSERT_INVEQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* XOR (x, TRUE, y) -> NOT XOR (x, y) */
+	ASSUME(a = XOR(REF(v1), T, REF(v2)));
+	ASSUME(b = XOR(REF(v1), REF(v2)));
+	ASSERT_INVEQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* XOR (x, y, TRUE) -> NOT XOR (x, y) */
+	ASSUME(a = XOR(REF(v1), REF(v2), T));
+	ASSUME(b = XOR(REF(v1), REF(v2)));
+	ASSERT_INVEQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* XOR (FALSE, x, y) -> XOR (x, y) */
+	ASSUME(a = XOR(F, REF(v1), REF(v2)));
+	ASSUME(b = XOR(REF(v1), REF(v2)));
+	ASSERT_EQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* XOR (x, FALSE, y) -> XOR (x, y) */
+	ASSUME(a = XOR(REF(v1), F, REF(v2)));
+	ASSUME(b = XOR(REF(v1), REF(v2)));
+	ASSERT_EQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* XOR (x, y, FALSE) -> XOR (x, y) */
+	ASSUME(a = XOR(REF(v1), REF(v2), F));
+	ASSUME(b = XOR(REF(v1), REF(v2)));
+	ASSERT_EQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+#endif
+
+	/* NOT XOR (x, y) -> XOR (NOT x, y) */
+	ASSUME(a = XOR(REF(v1), REF(v2)));
+	ASSUME(a = libnormalform_not(a));
+	ASSUME(b = libnormalform_not(REF(v1)));
+	ASSUME(b = libnormalform_xorl(b, REF(v2), NULL));
+	ASSERT_EQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* NOT XOR (x, y) -> XOR (x, NOT y) */
+	ASSUME(a = XOR(REF(v1), REF(v2)));
+	ASSUME(a = libnormalform_not(a));
+	ASSUME(b = libnormalform_not(REF(v2)));
+	ASSUME(b = libnormalform_xorl(REF(v1), b, NULL));
+	ASSERT_EQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* NOT XOR (x, y) -> XOR (x, y, TRUE) */
+	ASSUME(a = XOR(REF(v1), REF(v2)));
+	ASSUME(a = libnormalform_not(a));
+	ASSUME(b = libnormalform_xorl(REF(v1), REF(v2), T, NULL));
+	ASSERT_EQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* XOR (x, y) -> independence from XOR (x, z) */
+	ASSUME(a = XOR(REF(v1), REF(v2)));
+	ASSUME(b = libnormalform_xor2(REF(v1), REF(v3)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* XOR (x, y) -> independence from XOR (z, x) */
+	ASSUME(a = XOR(REF(v1), REF(v2)));
+	ASSUME(b = libnormalform_xor2(REF(v3), REF(v2)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* XOR (x, y) -> independence from XOR (z, w) */
+	ASSUME(a = XOR(REF(v1), REF(v2)));
+	ASSUME(b = libnormalform_xor2(REF(v3), REF(v4)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* XOR (x, y) -> independence from AND (x, y) */
+	ASSUME(a = REF(v1));
+	ASSUME(b = REF(v2));
+	ASSUME(b = libnormalform_and2(a, b));
+	ASSUME(a = XOR(REF(v1), REF(v2)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* XOR (x, y) -> independence from AND (x, NOT y) */
+	ASSUME(a = REF(v1));
+	ASSUME(b = libnormalform_not(REF(v2)));
+	ASSUME(b = libnormalform_and2(a, b));
+	ASSUME(a = XOR(REF(v1), REF(v2)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* XOR (x, y) -> independence from AND (NOT x, y) */
+	ASSUME(a = libnormalform_not(REF(v1)));
+	ASSUME(b = REF(v2));
+	ASSUME(b = libnormalform_and2(a, b));
+	ASSUME(a = XOR(REF(v1), REF(v2)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* XOR (x, y) -> independence from AND (NOT x, NOT y) */
+	ASSUME(a = libnormalform_not(REF(v1)));
+	ASSUME(b = libnormalform_not(REF(v2)));
+	ASSUME(b = libnormalform_and2(a, b));
+	ASSUME(a = XOR(REF(v1), REF(v2)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* XOR (x, y) -> independence from OR (x, y) */
+	ASSUME(a = REF(v1));
+	ASSUME(b = REF(v2));
+	ASSUME(b = libnormalform_or2(a, b));
+	ASSUME(a = XOR(REF(v1), REF(v2)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* XOR (x, y) -> independence from OR (x, NOT y) */
+	ASSUME(a = REF(v1));
+	ASSUME(b = libnormalform_not(REF(v2)));
+	ASSUME(b = libnormalform_or2(a, b));
+	ASSUME(a = XOR(REF(v1), REF(v2)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* XOR (x, y) -> independence from OR (NOT x, y) */
+	ASSUME(a = libnormalform_not(REF(v1)));
+	ASSUME(b = REF(v2));
+	ASSUME(b = libnormalform_or2(a, b));
+	ASSUME(a = XOR(REF(v1), REF(v2)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* XOR (x, y) -> independence from OR (NOT x, NOT y) */
+	ASSUME(a = libnormalform_not(REF(v1)));
+	ASSUME(b = libnormalform_not(REF(v2)));
+	ASSUME(b = libnormalform_or2(a, b));
+	ASSUME(a = XOR(REF(v1), REF(v2)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* XOR (x, y) -> independence from TRUE */
+	ASSUME(a = XOR(REF(v1), REF(v2)));
+	ASSUME(b = libnormalform_true());
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* XOR (x, y) -> independence from FALSE */
+	ASSUME(a = XOR(REF(v1), REF(v2)));
+	ASSUME(b = libnormalform_false());
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* XOR (x, y) -> independence from variable1 */
+	ASSUME(a = XOR(REF(v1), REF(v2)));
+	ASSERT_NOTEQUAL(a, v1);
+	libnormalform_free(a);
+
+	/* XOR (x, y) -> independence from NOT variable1 */
+	ASSUME(a = XOR(REF(v1), REF(v2)));
+	ASSUME(b = libnormalform_not(REF(v1)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* XOR (x, y) -> independence from function1 */
+	ASSUME(a = XOR(REF(v1), REF(v2)));
+	ASSERT_NOTEQUAL(a, f1);
+	libnormalform_free(a);
+
+	/* XOR (x, y) -> independence from NOT function1 */
+	ASSUME(a = XOR(REF(v1), REF(v2)));
+	ASSUME(b = libnormalform_not(REF(f1)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* XOR (x, y) -> independence from T(function1) */
+	ASSUME(a = XOR(REF(v1), REF(v2)));
+	ASSUME(b = libnormalform_transformation(&trans, REF(f1)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* XOR (x, y) -> independence from ALL (domain1, function1, function2) */
+	ASSUME(a = XOR(REF(v1), REF(v2)));
+	ASSUME(b = libnormalform_all(&domain, REF(f1), REF(f2)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* XOR (x, y) -> independence from ANY (domain1, function1, function2) */
+	ASSUME(a = XOR(REF(v1), REF(v2)));
+	ASSUME(b = libnormalform_any(&domain, REF(f1), REF(f2)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* XOR (x, y) -> independence from ONE (domain1, function1, function2) */
+	ASSUME(a = XOR(REF(v1), REF(v2)));
+	ASSUME(b = libnormalform_one(&domain, REF(f1), REF(f2)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* XOR (x, y) -> independence from NOT ONE (domain1, function1, function2) */
+	ASSUME(a = XOR(REF(v1), REF(v2)));
+	ASSUME(b = libnormalform_one(&domain, REF(f1), REF(f2)));
+	ASSUME(b = libnormalform_not(b));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* XOR (x, y) -> OR (AND (x, NOT y), AND (NOT x, y)) */
+	ASSUME(a = libnormalform_not(REF(v2)));
+	ASSUME(a = libnormalform_and2(REF(v1), a));
+	ASSUME(b = libnormalform_not(REF(v1)));
+	ASSUME(b = libnormalform_and2(b, REF(v2)));
+	ASSUME(b = libnormalform_or2__(a, b));
+	ASSUME(a = XOR(REF(v1), REF(v2)));
+	ASSERT(a->type == TYPE_XOR);
+	ASSERT(b->type == TYPE_OR);
+	ASSERT_EQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* XOR (x, y) -> AND (OR (x, y), OR (NOT x, NOT y)) */
+	ASSUME(a = libnormalform_not(REF(v1)));
+	ASSUME(b = libnormalform_not(REF(v2)));
+	ASSUME(b = libnormalform_or2(a, b));
+	ASSUME(a = libnormalform_or2(REF(v1), REF(v2)));
+	ASSUME(b = libnormalform_and2__(a, b));
+	ASSUME(a = XOR(REF(v1), REF(v2)));
+	ASSERT(a->type == TYPE_XOR);
+	ASSERT(b->type == TYPE_AND);
+	ASSERT_EQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* XOR (x, y) -> OR (AND (x, NOT y), AND (NOT x, y)) */
+	ASSUME(a = libnormalform_not(REF(v2)));
+	ASSUME(a = libnormalform_and2(REF(v1), a));
+	ASSUME(b = libnormalform_not(REF(v1)));
+	ASSUME(b = libnormalform_and2(b, REF(v2)));
+	ASSUME(b = libnormalform_or2(a, b));
+	ASSUME(a = XOR(REF(v1), REF(v2)));
+	ASSERT(a->type == TYPE_XOR);
+	ASSERT(b->type == TYPE_XOR);
+	ASSERT_EQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* XOR (x, y) -> AND (OR (x, y), OR (NOT x, NOT y)) */
+	ASSUME(a = libnormalform_not(REF(v1)));
+	ASSUME(b = libnormalform_not(REF(v2)));
+	ASSUME(b = libnormalform_or2(a, b));
+	ASSUME(a = libnormalform_or2(REF(v1), REF(v2)));
+	ASSUME(b = libnormalform_and2(a, b));
+	ASSUME(a = XOR(REF(v1), REF(v2)));
+	ASSERT(a->type == TYPE_XOR);
+	ASSERT(b->type == TYPE_XOR);
+	ASSERT_EQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* XOR (x, y) -> OR (AND (NOT x, y), AND (x, NOT y)) */
+	ASSUME(a = libnormalform_not(REF(v2)));
+	ASSUME(a = libnormalform_and2(REF(v1), a));
+	ASSUME(b = libnormalform_not(REF(v1)));
+	ASSUME(b = libnormalform_and2(b, REF(v2)));
+	ASSUME(b = libnormalform_or2__(b, a));
+	ASSUME(a = XOR(REF(v1), REF(v2)));
+	ASSERT(a->type == TYPE_XOR);
+	ASSERT(b->type == TYPE_OR);
+	ASSERT_EQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* XOR (x, y) -> AND (OR (NOT x, NOT y), OR (x, y)) */
+	ASSUME(a = libnormalform_not(REF(v1)));
+	ASSUME(b = libnormalform_not(REF(v2)));
+	ASSUME(b = libnormalform_or2(a, b));
+	ASSUME(a = libnormalform_or2(REF(v1), REF(v2)));
+	ASSUME(b = libnormalform_and2__(b, a));
+	ASSUME(a = XOR(REF(v1), REF(v2)));
+	ASSERT(a->type == TYPE_XOR);
+	ASSERT(b->type == TYPE_AND);
+	ASSERT_EQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* XOR (x, y) -> OR (AND (NOT x, y), AND (x, NOT y)) */
+	ASSUME(a = libnormalform_not(REF(v2)));
+	ASSUME(a = libnormalform_and2(REF(v1), a));
+	ASSUME(b = libnormalform_not(REF(v1)));
+	ASSUME(b = libnormalform_and2(b, REF(v2)));
+	ASSUME(b = libnormalform_or2(b, a));
+	ASSUME(a = XOR(REF(v1), REF(v2)));
+	ASSERT(a->type == TYPE_XOR);
+	ASSERT(b->type == TYPE_XOR);
+	ASSERT_EQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+	/* XOR (x, y) -> AND (OR (NOT x, NOT y), OR (x, y)) */
+	ASSUME(a = libnormalform_not(REF(v1)));
+	ASSUME(b = libnormalform_not(REF(v2)));
+	ASSUME(b = libnormalform_or2(a, b));
+	ASSUME(a = libnormalform_or2(REF(v1), REF(v2)));
+	ASSUME(b = libnormalform_and2(b, a));
+	ASSUME(a = XOR(REF(v1), REF(v2)));
+	ASSERT(a->type == TYPE_XOR);
+	ASSERT(b->type == TYPE_XOR);
+	ASSERT_EQUAL(a, b);
+	libnormalform_free(a);
+	libnormalform_free(b);
+
+#undef T
+#undef F
+#undef TV
+#undef FV
+
+#undef ASSERT_CONST
+#undef ASSERT_EVAL2
+#undef ASSERT_EVAL3
+
+	libnormalform_free(v1);
+	libnormalform_free(v2);
+	libnormalform_free(v3);
+	libnormalform_free(v4);
+	libnormalform_free(f1);
+	libnormalform_free(f2);
+	libnormalform_free(ts);
+	libnormalform_free(fs);
+
+	/* cascading of evaluation failure is tested in libnormalform_function.c */
+
+	TEST_END;
+}
+
+
+#endif