/* 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   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
is_in(LIBNORMALFORM_SENTENCE *x, LIBNORMALFORM_SENTENCE **among, size_t n, int *inv_out)
{
	while (n--)
		if (x->equals(x, among[n], inv_out))
			return 1;
	return 0;
}


LIBNORMALFORM_SENTENCE *
(libnormalform_and)(LIBNORMALFORM_SENTENCE **xs)
{
	LIBNORMALFORM_SENTENCE *x, *ret, **saved = xs;
	size_t n = 0;
	int inv;

	for (; (x = *xs); xs++) {
		if (x->type == TYPE_FALSE) {
			/* ⋀X ∧ 0 = 0 */
			ret = *xs++;
			goto return_asis;

		} else if (x->type == TYPE_TRUE) {
		redundant:
			/* ⋀X ∧ 1 = ⋀X */
			libnormalform_free(x);

		} else if (is_in(x, saved, n, &inv)) {
			if (!inv) {
				/* x ∧ x = x */
				goto redundant;

			} else {
				/* x ∧ ¬x = 0 */
				libnormalform_free(*xs++);
				ret = libnormalform_false();
				goto return_asis;
			}

		} else {
			saved[n++] = x;
		}
	}

	if (!n) {
		/* ⋀∅ = ∀x∈∅.x = {vacuous truth} = 1 */
		return libnormalform_true();
	}

	saved[n] = NULL;
	/* ⋀{x} = x */
	ret = *saved++;
	/* ⋀(X ∪ x) = ⋀X ∧ x */
	for (; *saved; saved++)
		ret = libnormalform_and2(ret, *saved);

	return ret;

return_asis:
	while (*xs)
		libnormalform_free(*xs++);
	while (n)
		libnormalform_free(saved[--n]);
	return ret;
}


#else


#define AND(...) LIBNORMALFORM_AND(__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(!AND(REF(v1), NULL) && errno == 0);
	errno = 1;
	ASSERT(!AND(REF(v1), NULL) && errno == 1);
	errno = 0;
	ASSERT(!AND(NULL, REF(v1)) && errno == 0);
	errno = 1;
	ASSERT(!AND(NULL, REF(v1)) && errno == 1);
	errno = 0;
	ASSERT(!AND(NULL, NULL) && errno == 0);
	errno = 1;
	ASSERT(!AND(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 = AND(__VA_ARGS__));\
		ASSERT(a->type == TYPE_##VALUE);\
		libnormalform_free(a);\
	} while (0)

#define ASSERT_EVAL2(VALUE, V1, V2)\
	do {\
		ASSUME(a = AND(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 = AND(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(TRUE); /* AND () -> TRUE */

#if defined(__GNUC__)
# pragma GCC diagnostic pop
#endif

	ASSERT_CONST(TRUE, T);  /* AND (TRUE) -> TRUE */
	ASSERT_CONST(FALSE, F); /* AND (FALSE) -> FALSE */

#endif

	ASSERT_CONST(FALSE, F, F); /* AND (FALSE, FALSE) -> FALSE */
	ASSERT_CONST(FALSE, F, T); /* AND (FALSE, TRUE) -> FALSE */
	ASSERT_CONST(FALSE, T, F); /* AND (TRUE, FALSE) -> FALSE */
	ASSERT_CONST(TRUE,  T, T); /* AND (TRUE, TRUE) -> TRUE */

	ASSERT_EVAL2(FALSE, F, F); /* AND (var(FALSE), var(FALSE)) => FALSE */
	ASSERT_EVAL2(FALSE, F, T); /* AND (var(FALSE), var(TRUE)) => FALSE */
	ASSERT_EVAL2(FALSE, T, F); /* AND (var(TRUE), var(FALSE)) => FALSE */
	ASSERT_EVAL2(TRUE,  T, T); /* AND (var(TRUE), var(TRUE)) => TRUE */

#ifndef USE_TWO

	ASSERT_CONST(FALSE, F, F, F); /* AND (FALSE, FALSE, FALSE) -> FALSE */
	ASSERT_CONST(FALSE, F, F, T); /* AND (FALSE, FALSE, TRUE) -> FALSE */
	ASSERT_CONST(FALSE, F, T, F); /* AND (FALSE, TRUE, FALSE) -> FALSE */
	ASSERT_CONST(FALSE, F, T, T); /* AND (FALSE, TRUE, TRUE) -> FALSE */
	ASSERT_CONST(FALSE, T, F, F); /* AND (TRUE, FALSE, FALSE) -> FALSE */
	ASSERT_CONST(FALSE, T, F, T); /* AND (TRUE, FALSE, TRUE) -> FALSE */
	ASSERT_CONST(FALSE, T, T, F); /* AND (TRUE, TRUE, FALSE) -> FALSE */
	ASSERT_CONST(TRUE,  T, T, T); /* AND (TRUE, TRUE, TRUE) -> TRUE */

	ASSERT_EVAL3(FALSE, F, F, F); /* AND (var(FALSE), var(FALSE), var(FALSE)) => FALSE */
	ASSERT_EVAL3(FALSE, F, F, T); /* AND (var(FALSE), var(FALSE), var(TRUE)) => FALSE */
	ASSERT_EVAL3(FALSE, F, T, F); /* AND (var(FALSE), var(TRUE), var(FALSE)) => FALSE */
	ASSERT_EVAL3(FALSE, F, T, T); /* AND (var(FALSE), var(TRUE), var(TRUE)) => FALSE */
	ASSERT_EVAL3(FALSE, T, F, F); /* AND (var(TRUE), var(FALSE), var(FALSE)) => FALSE */
	ASSERT_EVAL3(FALSE, T, F, T); /* AND (var(TRUE), var(FALSE), var(TRUE)) => FALSE */
	ASSERT_EVAL3(FALSE, T, T, F); /* AND (var(TRUE), var(TRUE), var(FALSE)) => FALSE */
	ASSERT_EVAL3(TRUE,  T, T, T); /* AND (var(TRUE), var(TRUE), var(TRUE)) => TRUE */

	/* AND (x) -> x */
	ASSUME(a = AND(REF(v1)));
	ASSERT(a == v1);
	ASSERT(a->refcount == 2);
	libnormalform_free(a);

#endif

	/* AND (x, FALSE) -> FALSE */
	ASSUME(a = AND(REF(v1), F));
	ASSERT(a->type == TYPE_FALSE);
	libnormalform_free(a);

	/* AND (FALSE, x) -> FALSE */
	ASSUME(a = AND(F, REF(v1)));
	ASSERT(a->type == TYPE_FALSE);
	libnormalform_free(a);

	/* AND (x, TRUE) -> x */
	ASSUME(a = AND(REF(v1), T));
	ASSERT_EQUAL(a, v1);
	ASSERT(a == v1);
	libnormalform_free(a);

	/* AND (TRUE, x) -> x */
	ASSUME(a = AND(T, REF(v1)));
	ASSERT_EQUAL(a, v1);
	ASSERT(a == v1);
	libnormalform_free(a);

#ifndef USE_TWO

	/* AND (x, FALSE, FALSE) -> FALSE */
	ASSUME(a = AND(REF(v1), F, F));
	ASSERT(a->type == TYPE_FALSE);
	libnormalform_free(a);

	/* AND (x, FALSE, TRUE) -> FALSE x */
	ASSUME(a = AND(REF(v1), F, T));
	ASSERT(a->type == TYPE_FALSE);
	libnormalform_free(a);

	/* AND (x, TRUE, FALSE) -> FALSE */
	ASSUME(a = AND(REF(v1), T, F));
	ASSERT(a->type == TYPE_FALSE);
	libnormalform_free(a);

	/* AND (x, TRUE, TRUE) -> x */
	ASSUME(a = AND(REF(v1), T, T));
	ASSERT_EQUAL(a, v1);
	ASSERT(a == v1);
	libnormalform_free(a);

	/* AND (FALSE, x, FALSE) -> FALSE */
	ASSUME(a = AND(F, REF(v1), F));
	ASSERT(a->type == TYPE_FALSE);
	libnormalform_free(a);

	/* AND (FALSE, x, TRUE) -> FALSE */
	ASSUME(a = AND(F, REF(v1), T));
	ASSERT(a->type == TYPE_FALSE);
	libnormalform_free(a);

	/* AND (TRUE, x, FALSE) -> FALSE */
	ASSUME(a = AND(T, REF(v1), F));
	ASSERT(a->type == TYPE_FALSE);
	libnormalform_free(a);

	/* AND (TRUE, x, TRUE) -> x */
	ASSUME(a = AND(T, REF(v1), T));
	ASSERT_EQUAL(a, v1);
	ASSERT(a == v1);
	libnormalform_free(a);

	/* AND (FALSE, FALSE, x) -> FALSE */
	ASSUME(a = AND(F, F, REF(v1)));
	ASSERT(a->type == TYPE_FALSE);
	libnormalform_free(a);

	/* AND (FALSE, TRUE, x) -> FALSE */
	ASSUME(a = AND(F, T, REF(v1)));
	ASSERT(a->type == TYPE_FALSE);
	libnormalform_free(a);

	/* AND (TRUE, FALSE, x) -> FALSE */
	ASSUME(a = AND(T, F, REF(v1)));
	ASSERT(a->type == TYPE_FALSE);
	libnormalform_free(a);

	/* AND (TRUE, TRUE, x) -> x */
	ASSUME(a = AND(T, T, REF(v1)));
	ASSERT_EQUAL(a, v1);
	ASSERT(a == v1);
	libnormalform_free(a);

#endif

	/* AND (x, x) -> x */
	ASSUME(a = AND(REF(v1), REF(v1)));
	ASSERT_EQUAL(a, v1);
	ASSERT(a == v1);
	libnormalform_free(a);

	/* AND (x, NOT x) -> FALSE */
	ASSUME(a = libnormalform_not(REF(v1)));
	ASSUME(a = AND(REF(v1), a));
	ASSERT(a->type == TYPE_FALSE);
	libnormalform_free(a);

	/* AND (x, y) -> AND (x, y) */
	ASSUME(a = AND(REF(v1), REF(v2)));
	ASSUME(b = AND(REF(v1), REF(v2)));
	ASSERT_EQUAL(a, b);
	libnormalform_free(a);
	libnormalform_free(b);

	/* AND (y, x) -> AND (x, y) */
	ASSUME(a = AND(REF(v2), REF(v1)));
	ASSUME(b = AND(REF(v1), REF(v2)));
	ASSERT_EQUAL(a, b);
	libnormalform_free(a);
	libnormalform_free(b);

	/* NOT AND (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 = AND(REF(v1), REF(v2)));
	ASSUME(a = libnormalform_not(a));
	ASSERT_EQUAL(a, b);
	libnormalform_free(a);
	libnormalform_free(b);

	/* AND (x, y) -> independence from AND (x, z) */
	ASSUME(a = AND(REF(v1), REF(v2)));
	ASSUME(b = libnormalform_and2(REF(v1), REF(v3)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(a);
	libnormalform_free(b);

	/* AND (x, y) -> independence from AND (z, x) */
	ASSUME(a = AND(REF(v1), REF(v2)));
	ASSUME(b = libnormalform_and2(REF(v3), REF(v2)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(a);
	libnormalform_free(b);

	/* AND (x, y) -> independence from AND (z, w) */
	ASSUME(a = AND(REF(v1), REF(v2)));
	ASSUME(b = libnormalform_and2(REF(v3), REF(v4)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(a);
	libnormalform_free(b);

	/* AND (x, y) -> independence from OR (x, y) */
	ASSUME(a = REF(v1));
	ASSUME(b = REF(v2));
	ASSUME(b = libnormalform_or2(a, b));
	ASSUME(a = AND(REF(v1), REF(v2)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(a);
	libnormalform_free(b);

	/* AND (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 = AND(REF(v1), REF(v2)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(a);
	libnormalform_free(b);

	/* AND (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 = AND(REF(v1), REF(v2)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(a);
	libnormalform_free(b);

	/* AND (x, y) -> independence from XOR (x, y) */
	ASSUME(a = REF(v1));
	ASSUME(b = REF(v2));
	ASSUME(b = libnormalform_xor2(a, b));
	ASSUME(a = AND(REF(v1), REF(v2)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(a);
	libnormalform_free(b);

	/* AND (x, y) -> independence from XOR (x, NOT y) */
	ASSUME(a = REF(v1));
	ASSUME(b = libnormalform_not(REF(v2)));
	ASSUME(b = libnormalform_xor2(a, b));
	ASSUME(a = AND(REF(v1), REF(v2)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(a);
	libnormalform_free(b);

	/* AND (x, y) -> independence from XOR (NOT x, y) */
	ASSUME(a = libnormalform_not(REF(v1)));
	ASSUME(b = REF(v2));
	ASSUME(b = libnormalform_xor2(a, b));
	ASSUME(a = AND(REF(v1), REF(v2)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(a);
	libnormalform_free(b);

	/* AND (x, y) -> independence from XOR (NOT x, NOT y) */
	ASSUME(a = libnormalform_not(REF(v1)));
	ASSUME(b = libnormalform_not(REF(v2)));
	ASSUME(b = libnormalform_xor2(a, b));
	ASSUME(a = AND(REF(v1), REF(v2)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(a);
	libnormalform_free(b);

	/* AND (x, y) -> independence from TRUE */
	ASSUME(a = AND(REF(v1), REF(v2)));
	ASSUME(b = libnormalform_true());
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(a);
	libnormalform_free(b);

	/* AND (x, y) -> independence from FALSE */
	ASSUME(a = AND(REF(v1), REF(v2)));
	ASSUME(b = libnormalform_false());
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(a);
	libnormalform_free(b);

	/* AND (x, y) -> independence from variable1 */
	ASSUME(a = AND(REF(v1), REF(v2)));
	ASSERT_NOTEQUAL(a, v1);
	libnormalform_free(a);

	/* AND (x, y) -> independence from NOT variable1 */
	ASSUME(a = AND(REF(v1), REF(v2)));
	ASSUME(b = libnormalform_not(REF(v1)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(a);
	libnormalform_free(b);

	/* AND (x, y) -> independence from function1 */
	ASSUME(a = AND(REF(v1), REF(v2)));
	ASSERT_NOTEQUAL(a, f1);
	libnormalform_free(a);

	/* AND (x, y) -> independence from NOT function1 */
	ASSUME(a = AND(REF(v1), REF(v2)));
	ASSUME(b = libnormalform_not(REF(f1)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(a);
	libnormalform_free(b);

	/* AND (x, y) -> independence from T(function1) */
	ASSUME(a = AND(REF(v1), REF(v2)));
	ASSUME(b = libnormalform_transformation(&trans, REF(f1)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(a);
	libnormalform_free(b);

	/* AND (x, y) -> independence from ALL (domain1, function1, function2) */
	ASSUME(a = AND(REF(v1), REF(v2)));
	ASSUME(b = libnormalform_all(&domain, REF(f1), REF(f2)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(a);
	libnormalform_free(b);

	/* AND (x, y) -> independence from ANY (domain1, function1, function2) */
	ASSUME(a = AND(REF(v1), REF(v2)));
	ASSUME(b = libnormalform_any(&domain, REF(f1), REF(f2)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(a);
	libnormalform_free(b);

	/* AND (x, y) -> independence from ONE (domain1, function1, function2) */
	ASSUME(a = AND(REF(v1), REF(v2)));
	ASSUME(b = libnormalform_one(&domain, REF(f1), REF(f2)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(a);
	libnormalform_free(b);

	/* AND (x, y) -> independence from NOT ONE (domain1, function1, function2) */
	ASSUME(a = AND(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);

	/* AND (OR (x, NOT y), OR (NOT x, y)) -> NOT XOR (x, y) */
	ASSUME(a = libnormalform_not(REF(v2)));
	ASSUME(b = libnormalform_not(REF(v1)));
	ASSUME(a = libnormalform_or2(REF(v1), a));
	ASSUME(b = libnormalform_or2(b, REF(v2)));
	ASSUME(a = AND(a, b));
	ASSUME(b = libnormalform_xor2(REF(v1), REF(v2)));
	ASSERT_INVEQUAL(a, b);
	ASSERT(a->type == TYPE_XOR);
	ASSERT(a->type == TYPE_XOR);
	libnormalform_free(a);
	libnormalform_free(b);

	/* AND (OR (NOT x, y), OR (x, NOT y)) -> NOT XOR (x, y) */
	ASSUME(a = libnormalform_not(REF(v2)));
	ASSUME(b = libnormalform_not(REF(v1)));
	ASSUME(a = libnormalform_or2(REF(v1), a));
	ASSUME(b = libnormalform_or2(b, REF(v2)));
	ASSUME(a = AND(b, a));
	ASSUME(b = libnormalform_xor2(REF(v1), REF(v2)));
	ASSERT_INVEQUAL(a, b);
	ASSERT(a->type == TYPE_XOR);
	ASSERT(a->type == TYPE_XOR);
	libnormalform_free(a);
	libnormalform_free(b);

	/* AND (OR (x, y), OR (NOT x, NOT y)) -> XOR (x, y) */
	ASSUME(a = libnormalform_not(REF(v2)));
	ASSUME(b = libnormalform_not(REF(v1)));
	ASSUME(b = libnormalform_or2(a, b));
	ASSUME(a = libnormalform_or2(REF(v1), REF(v2)));
	ASSUME(a = AND(a, b));
	ASSUME(b = libnormalform_xor2(REF(v1), REF(v2)));
	ASSERT_EQUAL(a, b);
	ASSERT(a->type == TYPE_XOR);
	ASSERT(a->type == TYPE_XOR);
	libnormalform_free(a);
	libnormalform_free(b);

	/* AND (OR (NOT x, NOT y), OR (x, y)) -> XOR (x, y) */
	ASSUME(a = libnormalform_not(REF(v2)));
	ASSUME(b = libnormalform_not(REF(v1)));
	ASSUME(b = libnormalform_or2(a, b));
	ASSUME(a = libnormalform_or2(REF(v1), REF(v2)));
	ASSUME(a = AND(b, a));
	ASSUME(b = libnormalform_xor2(REF(v1), REF(v2)));
	ASSERT_EQUAL(a, b);
	ASSERT(a->type == TYPE_XOR);
	ASSERT(a->type == TYPE_XOR);
	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