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


extern inline LIBNORMALFORM_SENTENCE *(libnormalform_uniquely)(struct libnormalform_map *, LIBNORMALFORM_SENTENCE *);


#else


static int
evalbool(void *user_data, void *input)
{
	int *vp = input;
	(void) user_data;
	return *vp;
}


int
main(void)
{
	TEST_BEGIN;

	struct libnormalform_variable var1;
	struct libnormalform_function fun1;
	struct libnormalform_map dom1, dom2;
	struct libnormalform_mapping map[3];
	struct libnormalform_transformer trans;
	LIBNORMALFORM_SENTENCE *a, *b, *v1;
	int t = 1, f = 0;

	ASSUME(v1 = libnormalform_variable(&var1));

	errno = 0;
	ASSERT(!libnormalform_uniquely(&dom1, NULL) && errno == 0);
	errno = 1;
	ASSERT(!libnormalform_uniquely(&dom1, NULL) && errno == 1);

	dom1.mappings = map;
	memset(map, 0, sizeof(map));

	/* ∃!x.⊥ = ⊥ */
	ASSUME(a = libnormalform_uniquely(&dom1, libnormalform_false()));
	ASSERT(a->type == TYPE_FALSE);
	libnormalform_free(a);

	/* ∃!x.φ irreducable */
	ASSUME(a = libnormalform_uniquely(&dom1, REF(v1)));
	ASSERT(a->type == TYPE_ONE);
	libnormalform_free(a);

	/* ∃!x.⊤ irreducable */
	ASSUME(a = libnormalform_uniquely(&dom1, libnormalform_true()));
	ASSERT(a->type == TYPE_ONE);
	libnormalform_free(a);

	ASSUME(a = libnormalform_uniquely(&dom1, REF(v1)));
	ASSERT(a->type == TYPE_ONE);
	ASSERT(a->refcount == 1);

	dom1.nmappings = 1;

	/* ∃!x∈{a}.⊥ = ⊥ */
	var1.value = LIBNORMALFORM_FALSE;
	ASSERT(libnormalform_evaluate(a) == 0);

	/* ∃!x∈{a}.⊤ = ⊤ */
	var1.value = LIBNORMALFORM_TRUE;
	ASSERT(libnormalform_evaluate(a) == 1);

	dom1.nmappings = 2;

	/* ∃!x∈{a,b}.⊥ = ⊥ */
	var1.value = LIBNORMALFORM_FALSE;
	ASSERT(libnormalform_evaluate(a) == 0);

	/* ∃!x∈{a,b}.⊤ = ⊥ */
	var1.value = LIBNORMALFORM_TRUE;
	ASSERT(libnormalform_evaluate(a) == 0);

	dom1.nmappings = 0;

	/* ∃!x∈∅.⊥ = ⊥ */
	var1.value = LIBNORMALFORM_FALSE;
	ASSERT(libnormalform_evaluate(a) == 0);

	/* ∃!x∈∅.⊤ = ⊥ */
	var1.value = LIBNORMALFORM_TRUE;
	ASSERT(libnormalform_evaluate(a) == 0);

	dom1.nmappings = 0;

	libnormalform_free(a);

	fun1.evaluate = &evalbool;
	dom1.nmappings = 2;

	ASSUME(a = libnormalform_uniquely(&dom1, libnormalform_function(&fun1)));
	ASSERT(a->type == TYPE_ONE);
	map[0].key = NULL;
	map[1].key = NULL;

	/* ∃!x∈{⊥, ⊥}.x = ⊥ */
	map[0].value = &f;
	map[1].value = &f;
	ASSERT(libnormalform_evaluate(a) == 0);

	/* ∃!x∈{⊥, ⊤}.x = ⊤ */
	map[0].value = &f;
	map[1].value = &t;
	ASSERT(libnormalform_evaluate(a) == 1);

	/* ∃!x∈{⊤, ⊥}.x = ⊤ */
	map[0].value = &t;
	map[1].value = &f;
	ASSERT(libnormalform_evaluate(a) == 1);

	/* ∃!x∈{⊤, ⊤}.x = ⊥ */
	map[0].value = &t;
	map[1].value = &t;
	ASSERT(libnormalform_evaluate(a) == 0);

	/* ∃!x∈{⊤, ⊤, ⊤}.x = ⊥ */
	map[0].value = &t;
	map[1].value = &t;
	map[2].value = &t;
	ASSERT(libnormalform_evaluate(a) == 0);

	libnormalform_free(a);

	ASSUME(a = libnormalform_uniquely(&dom1, REF(v1)));

	/* ∃!x∈X.P(x) = ∃!x∈X.(⊤ ∧ P(x)) */
	ASSUME(b = libnormalform_one(&dom1, libnormalform_true(), REF(v1)));
	ASSERT_EQUAL(a, b);
	libnormalform_free(b);

	/* ¬∃!x∈X.P(x) = ¬∃!x∈X.P(x) */
	ASSUME(b = libnormalform_not(REF(a)));
	ASSERT_INVEQUAL(a, b);
	ASSERT(b->type == TYPE_NOT_ONE);
	libnormalform_free(b);

	/* ∃!x∈X.P(x) independent from ∃!x∈X.Q(x) */
	ASSUME(b = libnormalform_uniquely(&dom1, libnormalform_function(&fun1)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);

	/* ∃!x∈X.P(x) independent from ∃!x∈Y.P(x)) */
	ASSUME(b = libnormalform_uniquely(&dom2, REF(v1)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);

	/* ∃!x∈X.P(x) independent from TRUE */
	ASSUME(b = libnormalform_true());
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);

	/* ∃!x∈X.P(x) independent from FALSE */
	ASSUME(b = libnormalform_false());
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);

	/* ∃!x∈X.P(x) independent from variable1 */
	ASSUME(b = libnormalform_variable(&var1));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);

	/* ∃!x∈X.P(x) independent from NOT variable1 */
	ASSUME(b = libnormalform_not(libnormalform_variable(&var1)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);

	/* ∃!x∈X.P(x) independent from function1 */
	ASSUME(b = libnormalform_function(&fun1));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);

	/* ∃!x∈X.P(x) independent from NOT function1 */
	ASSUME(b = libnormalform_not(libnormalform_function(&fun1)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);

	/* ∃!x∈X.P(x) independent from T(function1) */
	ASSUME(b = libnormalform_transformation(&trans, libnormalform_function(&fun1)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);

	/* ∃!x∈X.P(x) independent from ∀x∈X.(⊤ → P(x)) */
	ASSUME(b = libnormalform_all(&dom1, libnormalform_true(), REF(v1)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);

	/* ∃!x∈X.P(x) independent from ∃x∈X.(⊤ ∧ P(x)) */
	ASSUME(b = libnormalform_any(&dom1, libnormalform_true(), REF(v1)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);

	/* ∃!x∈X.P(x) independent from AND (P, P) */
	ASSUME(b = libnormalform_and2__(REF(v1), REF(v1)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);

	/* ∃!x∈X.P(X) independent from OR (P, P) */
	ASSUME(b = libnormalform_or2__(REF(v1), REF(v1)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);

	/* ∃!x∈X.P(x) independent from XOR (P, P) */
	ASSUME(b = libnormalform_xor2__(REF(v1), REF(v1)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);

	libnormalform_free(a);

	libnormalform_free(v1);

	TEST_END;
}


#endif