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


/** 
 * See `.inverse` in `struct libnormalform_sentence` (FOR ONE implementation)
 */
static LIBNORMALFORM_SENTENCE *
one_inverse(LIBNORMALFORM_SENTENCE *this)
{
	/* ¬∃x.φ ⇒ ∀x.¬φ */
	LIBNORMALFORM_SENTENCE *ret;
	ret = libnormalform_one(this->data.qualifier.domain,
	                        libnormalform_ref(this->data.qualifier.antecedent),
	                        libnormalform_ref(this->data.qualifier.predicate));
        if (ret) {
		if (this->atom) {
			ret->atom = this->atom;
			ret->atom->refcount += 1;
		}
		ret->type = TYPE_ONE ^ TYPE_NOT_ONE ^ this->type;
	}
	return ret;
}


/** 
 * See `.equals` in `struct libnormalform_sentence` (FOR ONE implementation)
 */
static int
one_equals(LIBNORMALFORM_SENTENCE *this, LIBNORMALFORM_SENTENCE *other, int *inv_out)
{
	int r;

	if (this->hash != other->hash)
		return 0;

	if (other->type != TYPE_ONE && other->type != TYPE_NOT_ONE)
		return 0;

	if (this->data.qualifier.domain != other->data.qualifier.domain)
		return 0;

	r = this->data.qualifier.antecedent->equals(this->data.qualifier.antecedent, other->data.qualifier.antecedent, inv_out);
	if (r <= 0)
		return r;
	if (*inv_out)
		return 0;

	r = this->data.qualifier.predicate->equals(this->data.qualifier.predicate, other->data.qualifier.predicate, inv_out);
	if (r <= 0)
		return r;
	if (*inv_out)
		return 0;

	*inv_out = this->type != other->type;
	return r;
}


/** 
 * See `.evaluate` in `struct libnormalform_sentence` (FOR ONE implementation)
 */
static int
one_evaluate(LIBNORMALFORM_SENTENCE *this, void *input)
{
	size_t i, n = this->data.qualifier.domain->nmappings;
	void *k, *v;
	int r, ret = 0;

	(void) input;

	for (i = 0; i < n; i++) {
		k = this->data.qualifier.domain->mappings[i].key;
		v = this->data.qualifier.domain->mappings[i].value;
		r = this->data.qualifier.antecedent->evaluate(this->data.qualifier.antecedent, k);
		if (r <= 0) {
			if (!r)
				continue;
			return r;
		}
		r = this->data.qualifier.predicate->evaluate(this->data.qualifier.predicate, v);
		if (r) {
			if (r < 0)
				return r;
			if (++ret == 2)
				return this->type == TYPE_NOT_ONE;
		}
	}

	return ret ^ (this->type == TYPE_NOT_ONE);
}


LIBNORMALFORM_SENTENCE *
(libnormalform_one)(struct libnormalform_map *d, LIBNORMALFORM_SENTENCE *k, LIBNORMALFORM_SENTENCE *v)
{
	static const struct libnormalform_sentence prototype = {
		PROTOTYPE_COMMON,
		.type = TYPE_ONE,
		.inverse = &one_inverse,
		.equals = &one_equals,
		.evaluate = &one_evaluate
	};

	LIBNORMALFORM_SENTENCE *ret;

	if (!k || !v) {
		libnormalform_free(k);
		libnormalform_free(v);
		return NULL;
	}

	if (k->type == TYPE_FALSE) {
		libnormalform_free(v);
		return k;
	}
	if (v->type == TYPE_FALSE) {
		libnormalform_free(k);
		return v;
	}

	ret = malloc(sizeof(*ret));
	if (ret) {
		*ret = prototype;
		ret->hash = ONE_HASH(d, k, v);
		ret->data.qualifier.domain = d;
		ret->data.qualifier.antecedent = k;
		ret->data.qualifier.predicate = v;
	}
	return ret;
}


#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, var2;
	struct libnormalform_function fun1;
	struct libnormalform_map dom1, dom2;
	struct libnormalform_mapping map[3];
	struct libnormalform_transformer trans;
	LIBNORMALFORM_SENTENCE *a, *b, *c, *v1, *v2;
	int t = 1, f = 0;

	ASSUME(v1 = libnormalform_variable(&var1));
	ASSUME(v2 = libnormalform_variable(&var2));

	errno = 0;
	ASSERT(!libnormalform_one(&dom1, NULL, REF(v1)) && errno == 0);
	errno = 1;
	ASSERT(!libnormalform_one(&dom1, NULL, REF(v1)) && errno == 1);
	errno = 0;
	ASSERT(!libnormalform_one(&dom1, REF(v1), NULL) && errno == 0);
	errno = 1;
	ASSERT(!libnormalform_one(&dom1, REF(v1), NULL) && errno == 1);
	errno = 0;
	ASSERT(!libnormalform_one(&dom1, NULL, NULL) && errno == 0);
	errno = 1;
	ASSERT(!libnormalform_one(&dom1, NULL, NULL) && errno == 1);

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

	/* ∃!x.(⊥ ∧ φ(x)) = ⊥ */
	ASSUME(a = libnormalform_one(&dom1, libnormalform_false(), REF(v1)));
	ASSERT(a->type == TYPE_FALSE);
	libnormalform_free(a);

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

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

	/* ∃!x.(φ(x) ∧ ⊥) = ⊥ */
	ASSUME(a = libnormalform_one(&dom1, REF(v1), libnormalform_false()));
	ASSERT(a->type == TYPE_FALSE);
	libnormalform_free(a);

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

	dom1.nmappings = 1;

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

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

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

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

	dom1.nmappings = 2;

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

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

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

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

	dom1.nmappings = 0;

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

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

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

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

	dom1.nmappings = 0;

	libnormalform_free(a);

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

	ASSUME(a = libnormalform_function(&fun1));
	ASSUME(a = libnormalform_one(&dom1, libnormalform_true(), a));
	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);

	libnormalform_free(a);

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

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

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

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

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

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

	libnormalform_free(a);

	ASSUME(a = libnormalform_one(&dom1, REF(v1), REF(v2)));

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

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

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

	/* ¬∃!x∈X.(P(x) ∧ Q(x)) = ¬∃!x∈X.(P(x) ∧ Q(x)) */
	ASSUME(c = libnormalform_not(REF(a)));
	ASSUME(b = libnormalform_not(libnormalform_one(&dom1, REF(v1), REF(v2))));
	ASSERT_EQUAL(c, b);
	ASSERT(c->type == TYPE_NOT_ONE);
	libnormalform_free(b);
	libnormalform_free(c);

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

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

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

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

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

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

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

	/* ∃!x∈X.(P(x) ∧ Q(x)) = ∀x∈X.(P(x) → Q(x)) */
	ASSUME(b = libnormalform_all(&dom1, REF(v1), REF(v2)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);

	/* ∃!x∈X.(P(x) ∧ Q(x)) = ∃x∈X.(P(x) ∧ Q(x)) */
	ASSUME(b = libnormalform_any(&dom1, REF(v1), REF(v2)));
	ASSERT_NOTEQUAL(a, b);

	/* ∃!x∈X.(P(x) ∧ Q(x)) = ¬∃x∈X.(P(x) ∧ Q(x)) */
	ASSUME(b = libnormalform_not(b));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);

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

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

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

	/* P = ¬Q ⊭ ∃!⟨x,y⟩∈X.(P(x) ∧ Q(y)) = ∃!⟨x,y⟩∈X.(¬Q(x) ∧ Q(y)) = ∃!⟨x,y⟩∈X.⊥ = ⊥ ∵ P = ¬Q ⊭ P(x) = ¬Q(y) */
	/* P = ¬Q ⊭ ∃!⟨x,y⟩∈X.(P(x) ∧ Q(y)) = ∃!⟨x,y⟩∈X.(P(x) ∧ ¬P(y)) = ∃!⟨x,y⟩∈X.⊥ = ⊥ ∵ P = ¬Q ⊭ P(x) = ¬Q(y) */
	ASSUME(b = libnormalform_one(&dom1, libnormalform_false(), libnormalform_false()));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);
	ASSUME(b = libnormalform_false());
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);

	libnormalform_free(a);

	libnormalform_free(v1);
	libnormalform_free(v2);

	/* cascading of evaluation failure is tested in libnormalform_function.c */

	TEST_END;
}


#endif