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


LIBNORMALFORM_SENTENCE *
(libnormalform_not)(LIBNORMALFORM_SENTENCE *x)
{
	LIBNORMALFORM_SENTENCE *ret;
	if (!x)
		return NULL;
	ret = x->inverse(x);
	libnormalform_free(x);
	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;
}


int
main(void)
{
	TEST_BEGIN;

	struct libnormalform_variable var1, var2;
	struct libnormalform_function fun1, fun2;
	struct libnormalform_map domain;
	LIBNORMALFORM_SENTENCE *a, *b, *v1, *v2, *f1, *f2;
	int r1, r2;

	var1.value = LIBNORMALFORM_FALSE;
	var2.value = LIBNORMALFORM_TRUE;
	fun1.evaluate = &tautology;
	fun2.evaluate = &contradiction;
	domain.nmappings = 0;

	errno = 0;
	ASSERT(!libnormalform_not(NULL) && errno == 0);
	errno = 1;
	ASSERT(!libnormalform_not(NULL) && errno == 1);

	ASSUME(v1 = libnormalform_variable(&var1));
	ASSUME(v2 = libnormalform_variable(&var2));
	ASSUME(f1 = libnormalform_function(&fun1));
	ASSUME(f2 = libnormalform_function(&fun2));

#define CHECK(X)\
	do {\
		ASSUME(a = libnormalform_not(REF(X)));\
		ASSERT((X)->refcount == 1);\
		ASSERT(a->refcount == 1);\
		ASSERT_INVEQUAL(a, (X));\
		ASSERT((r1 = a->evaluate(a, NULL)) >= 0);\
		ASSERT((r2 = (X)->evaluate((X), NULL)) >= 0);\
		ASSERT(r1 == 1 - r2);\
		libnormalform_free(a);\
	} while (0)

	CHECK(v1);
	CHECK(f1);

#undef CHECK

#define CHECK(X)\
	do {\
		ASSUME(b = (X));\
		ASSUME(a = libnormalform_not(REF(b)));\
		ASSERT(b->refcount == 1);\
		ASSERT(a->refcount == 1);\
		ASSERT_INVEQUAL(a, b);\
		ASSERT((r1 = a->evaluate(a, NULL)) >= 0);\
		ASSERT((r2 = b->evaluate(b, NULL)) >= 0);\
		ASSERT(r1 == 1 - r2);\
		libnormalform_free(a);\
		libnormalform_free(b);\
	} while (0)

	CHECK(libnormalform_and2(REF(v1), REF(v2)));
	CHECK(libnormalform_or2(REF(v1), REF(v2)));
	CHECK(libnormalform_xor2(REF(v1), REF(v2)));
	CHECK(libnormalform_all(&domain, REF(f1), REF(f2)));
	CHECK(libnormalform_any(&domain, REF(f1), REF(f2)));
	CHECK(libnormalform_one(&domain, REF(f1), REF(f2)));

#undef CHECK

	libnormalform_free(v1);
	libnormalform_free(v2);
	libnormalform_free(f1);
	libnormalform_free(f2);

	TEST_END;
}


#endif