/* See LICENSE file for copyright and license details. */
#include "common.h"
#ifndef TEST


LIBNORMALFORM_SENTENCE *
(libnormalform_nand)(LIBNORMALFORM_SENTENCE **xs)
{
	LIBNORMALFORM_SENTENCE *x, *ret;
	int inv;

	/* 1 ⊼ x = ¬x, but 0 ⊼ x = 1, so at least one argument is required */
	ret = *xs++;
	if (!ret) {
		errno = EDOM;
		return NULL;
	}

	for (; (x = *xs); xs++) {
		if (!ret) {
			/* error handling */
			libnormalform_free(x);

		} else if (x->type == TYPE_FALSE || ret->type == TYPE_FALSE) {
		set_to_true:
			/* x ⊼ 0 = 0 ⊼ x = 1 */
			libnormalform_free(ret);
			libnormalform_free(x);
			ret = libnormalform_true();

		} else if (x->type == TYPE_TRUE) {
			/* x ⊼ 1 = ¬x */
			libnormalform_free(x);
			ret = libnormalform_not(ret);

		} else if (ret->type == TYPE_TRUE) {
		set_to_not_x:
			/* 1 ⊼ x = ¬x */
			libnormalform_free(ret);
			ret = libnormalform_not(x);

		} else if (ret->equals(ret, x, &inv)) {
			if (!inv) {
				/* x ⊼ x = ¬x */
				goto set_to_not_x;
			} else {
				/* x ⊼ ¬x = 1 */
				goto set_to_true;
			}

		} else {
			/* a ⊼ b = ¬(a ∧ b) = ¬a ∨ ¬b */
			ret = libnormalform_or2(libnormalform_not(ret), libnormalform_not(x));
		}
	}

	return ret;
}


#else


#define NAND(...) LIBNORMALFORM_NAND(__VA_ARGS__)


int
main(void)
{
	TEST_BEGIN;

	struct libnormalform_variable var1, var2, var3;
	LIBNORMALFORM_SENTENCE *a, *b, *v1, *v2, *v3;
	LIBNORMALFORM_SENTENCE *ts, *fs;

	ASSUME(v1 = libnormalform_variable(&var1));
	ASSUME(v2 = libnormalform_variable(&var2));
	ASSUME(v3 = libnormalform_variable(&var3));
	ASSUME(ts = libnormalform_true());
	ASSUME(fs = libnormalform_false());

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

#define ASSERT_EVAL2(VALUE, V1, V2)\
	do {\
		ASSUME(a = NAND(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)

#ifndef USE_TWO

#if defined(__GNUC__)
# pragma GCC diagnostic push
# pragma GCC diagnostic ignored "-Wformat"
#endif

	/* NAND () -> EDOM */
	errno = 0;
	ASSERT(!NAND() && errno == EDOM);

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

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

#endif

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

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

#ifndef USE_TWO

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

#endif

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

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

	/* NAND (x, TRUE) -> NOT x */
	ASSUME(a = NAND(REF(v1), T));
	ASSERT_INVEQUAL(a, v1);
	libnormalform_free(a);

	/* NAND (TRUE, x) -> NOT x */
	ASSUME(a = NAND(T, REF(v1)));
	ASSERT_INVEQUAL(a, v1);
	libnormalform_free(a);

	/* NAND (x, x) -> NOT x */
	ASSUME(a = NAND(REF(v1), REF(v1)));
	ASSERT_INVEQUAL(a, v1);
	libnormalform_free(a);

	/* NAND (x, NOT x) -> TRUE */
	ASSUME(a = libnormalform_not(REF(v1)));
	ASSUME(a = NAND(REF(v1), a));
	ASSERT(a->type == TYPE_TRUE);
	libnormalform_free(a);

	/* NAND (x, y) -> NOT AND (x, y) */
	ASSUME(b = libnormalform_and2(REF(v1), REF(v2)));
	ASSUME(a = NAND(REF(v1), REF(v2)));
	ASSERT_INVEQUAL(a, b);
	libnormalform_free(a);
	libnormalform_free(b);

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

#ifndef USE_TWO

	/* NAND (x, y, z) -> NOT AND (NOT AND (x, y), z) */
	ASSUME(b = libnormalform_and2(REF(v1), REF(v2)));
	ASSUME(b = libnormalform_not(b));
	ASSUME(b = libnormalform_and2(b, REF(v3)));
	ASSUME(a = NAND(REF(v1), REF(v2), REF(v3)));
	ASSERT_INVEQUAL(a, b);
	libnormalform_free(a);
	libnormalform_free(b);

#endif

#undef T
#undef F
#undef TV
#undef FV

#undef ASSERT_CONST
#undef ASSERT_EVAL2

	libnormalform_free(v1);
	libnormalform_free(v2);
	libnormalform_free(v3);
	libnormalform_free(ts);
	libnormalform_free(fs);

	TEST_END;
}


#endif