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


/** 
 * See `.inverse` in `struct libnormalform_sentence` (FOR ALL implementation)
 */
static LIBNORMALFORM_SENTENCE *
all_inverse(LIBNORMALFORM_SENTENCE *this)
{
	/* ¬∀x.φ ⇒ ∃x.¬φ */
	LIBNORMALFORM_SENTENCE *ret;
	ret = libnormalform_any(this->data.qualifier.domain,
	                        libnormalform_ref(this->data.qualifier.antecedent),
	                        this->data.qualifier.predicate->inverse(this->data.qualifier.predicate));
        if (ret && this->atom) {
		ret->atom = this->atom;
                ret->atom->refcount += 1;
	}
	return ret;
}


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

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

	if (other->type == TYPE_ALL)
		inv_expect = 0;
	else if (other->type == TYPE_ANY)
		inv_expect = 1;
	else
		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 != inv_expect)
		return 0;

	return r;
}


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

	(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 <= 0)
			return r;
	}

	return 1;
}


LIBNORMALFORM_SENTENCE *
(libnormalform_all)(struct libnormalform_map *d, LIBNORMALFORM_SENTENCE *k, LIBNORMALFORM_SENTENCE *v)
{
	static const struct libnormalform_sentence prototype = {
		PROTOTYPE_COMMON,
		.type = TYPE_ALL,
		.inverse = &all_inverse,
		.equals = &all_equals,
		.evaluate = &all_evaluate
	};

	LIBNORMALFORM_SENTENCE *ret;

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

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

	ret = malloc(sizeof(*ret));
	if (ret) {
		*ret = prototype;
		ret->hash = ANY_ALL_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[2];
	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_all(&dom1, NULL, REF(v1)) && errno == 0);
	errno = 1;
	ASSERT(!libnormalform_all(&dom1, NULL, REF(v1)) && errno == 1);
	errno = 0;
	ASSERT(!libnormalform_all(&dom1, REF(v1), NULL) && errno == 0);
	errno = 1;
	ASSERT(!libnormalform_all(&dom1, REF(v1), NULL) && errno == 1);
	errno = 0;
	ASSERT(!libnormalform_all(&dom1, NULL, NULL) && errno == 0);
	errno = 1;
	ASSERT(!libnormalform_all(&dom1, NULL, NULL) && errno == 1);

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

	/* ∀x.(⊥ → φ(x)) = ⊤ */
	ASSUME(a = libnormalform_all(&dom1, libnormalform_false(), REF(v1)));
	ASSERT(a->type == TYPE_TRUE);
	libnormalform_free(a);

	/* ∀x.(⊤ → φ(x)) irreducable */
	ASSUME(a = libnormalform_all(&dom1, libnormalform_true(), REF(v1)));
	ASSERT(a->type == TYPE_ALL);
	libnormalform_free(a);

	/* ∀x.(φ(x) → ⊤) = ⊤ */
	ASSUME(a = libnormalform_all(&dom1, REF(v1), libnormalform_true()));
	ASSERT(a->type == TYPE_TRUE);
	libnormalform_free(a);

	/* ∀x.(φ(x) → ⊥) irreducable */
	ASSUME(a = libnormalform_all(&dom1, REF(v1), libnormalform_false()));
	ASSERT(a->type == TYPE_ALL);
	libnormalform_free(a);

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

	dom1.nmappings = 1;

	/* ∀x∈{a}.(⊥ → ⊥) = ⊤ */
	var1.value = LIBNORMALFORM_FALSE;
	var2.value = LIBNORMALFORM_FALSE;
	ASSERT(libnormalform_evaluate(a) == 1);

	/* ∀x∈{a}.(⊥ → ⊤) = ⊤ */
	var1.value = LIBNORMALFORM_FALSE;
	var2.value = LIBNORMALFORM_TRUE;
	ASSERT(libnormalform_evaluate(a) == 1);

	/* ∀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) == 1);

	/* ∀x∈{a,b}.(⊥ → ⊤) = ⊤ */
	var1.value = LIBNORMALFORM_FALSE;
	var2.value = LIBNORMALFORM_TRUE;
	ASSERT(libnormalform_evaluate(a) == 1);

	/* ∀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) == 1);

	dom1.nmappings = 0;

	/* ∀x∈∅.(⊥ → ⊥) = ⊤ */
	var1.value = LIBNORMALFORM_FALSE;
	var2.value = LIBNORMALFORM_FALSE;
	ASSERT(libnormalform_evaluate(a) == 1);

	/* ∀x∈∅.(⊥ → ⊤) = ⊤ */
	var1.value = LIBNORMALFORM_FALSE;
	var2.value = LIBNORMALFORM_TRUE;
	ASSERT(libnormalform_evaluate(a) == 1);

	/* ∀x∈∅.(⊤ → ⊥) = ⊤ */
	var1.value = LIBNORMALFORM_TRUE;
	var2.value = LIBNORMALFORM_FALSE;
	ASSERT(libnormalform_evaluate(a) == 1);

	/* ∀x∈∅.(⊤ → ⊤) = ⊤ */
	var1.value = LIBNORMALFORM_TRUE;
	var2.value = LIBNORMALFORM_TRUE;
	ASSERT(libnormalform_evaluate(a) == 1);

	dom1.nmappings = 0;

	libnormalform_free(a);

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

	ASSUME(a = libnormalform_function(&fun1));
	ASSUME(a = libnormalform_all(&dom1, libnormalform_true(), a));
	ASSERT(a->type == TYPE_ALL);
	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) == 0);

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

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

	libnormalform_free(a);

	ASSUME(a = libnormalform_function(&fun1));
	ASSUME(a = libnormalform_all(&dom1, a, libnormalform_false()));
	ASSERT(a->type == TYPE_ALL);
	map[0].value = NULL;
	map[1].value = NULL;

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

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

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

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

	libnormalform_free(a);

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

	/* ∀x∈X.(P(x) → Q(x)) = ∀x∈X.(P(x) → Q(x)) */
	ASSUME(b = libnormalform_all(&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_all(&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_all(&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(b = libnormalform_any(&dom1, REF(v1), libnormalform_not(REF(v2))));
	ASSERT_INVEQUAL(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_any(&dom1, REF(v1), libnormalform_not(REF(v2))));
	ASSERT_EQUAL(c, b);
	ASSERT(c->type == TYPE_ANY);
	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)) independent from ∃x∈X.(P(x) → Q(x)) */
	ASSUME(b = libnormalform_any(&dom1, REF(v1), REF(v2)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);

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

	/* ∀x∈X.(P(x) → Q(x)) independent from ¬∃!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.(P(x) → P(y)) = ∀⟨x,y⟩∈X.⊤ = ⊤ ∵ P → Q ⊭ P(x) → Q(y) */
	ASSUME(b = libnormalform_all(&dom1, libnormalform_true(), libnormalform_true()));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);
	ASSUME(b = libnormalform_true());
	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.(⊤ → Q(y)) ∵ 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(y)) ∵ P → ¬Q ⊭ P(x) → ¬Q(y) */
	ASSUME(b = libnormalform_all(&dom1, libnormalform_true(), REF(v2)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);
	ASSUME(b = libnormalform_all(&dom1, libnormalform_true(), libnormalform_not(REF(v1))));
	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