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


/** 
 * See `.inverse` in `struct libnormalform_sentence` (TRUE implementation)
 */
static LIBNORMALFORM_SENTENCE *
true_inverse(LIBNORMALFORM_SENTENCE *this)
{
	(void) this;
	return libnormalform_false();
}


/** 
 * See `.equals` in `struct libnormalform_sentence` (TRUE implementation)
 */
static int
true_equals(LIBNORMALFORM_SENTENCE *this, LIBNORMALFORM_SENTENCE *other, int *inv_out)
{
	(void) this;
	if (other->type == TYPE_TRUE) {
		*inv_out = 0;
		return 1;
	} else if (other->type == TYPE_FALSE) {
		*inv_out = 1;
		return 1;
	} else {
		return 0;
	}
}


/** 
 * See `.evaluate` in `struct libnormalform_sentence` (TRUE implementation)
 */
CONST static int
true_evaluate(LIBNORMALFORM_SENTENCE *this, void *input)
{
	(void) this;
	(void) input;
	return 1;
}


LIBNORMALFORM_SENTENCE *
(libnormalform_true)(void)
{
	static const struct libnormalform_sentence prototype = {
		PROTOTYPE_COMMON,
		.type = TYPE_TRUE,
		.hash = TRUE_FALSE_HASH,
		.inverse = &true_inverse,
		.equals = &true_equals,
		.evaluate = &true_evaluate
	};

	/*
	 * During normalisation, some fields may be set,
	 * therefore a new allocation is returned instead
	 * of a reference to a static allocation, so that
	 * converation can be done from the threads at
	 * the same time on different sentences, both
	 * including this constant.
	 */

	LIBNORMALFORM_SENTENCE *ret = malloc(sizeof(*ret));
	if (ret)
		*ret = prototype;
	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;

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

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

	ASSUME(a = libnormalform_true());
	ASSERT(a->type == TYPE_TRUE);
	ASSERT(a->refcount == 1);
	ASSERT_EQUAL(a, a);

	ASSERT(a->evaluate(a, NULL) == 1);

#define CHECK(CMP, X)\
	do {\
		ASSUME(b = (X));\
		ASSERT_##CMP(a, b);\
		libnormalform_free(b);\
	} while (0)

	CHECK(EQUAL, libnormalform_true());
	CHECK(INVEQUAL, libnormalform_false());
	CHECK(NOTEQUAL, libnormalform_and2(REF(v1), REF(v2)));
	CHECK(NOTEQUAL, libnormalform_or2(REF(v1), REF(v2)));
	CHECK(NOTEQUAL, libnormalform_xor2(REF(v1), REF(v2)));
	CHECK(NOTEQUAL, libnormalform_all(&domain, REF(f1), REF(f2)));
	CHECK(NOTEQUAL, libnormalform_any(&domain, REF(f1), REF(f2)));
	CHECK(NOTEQUAL, libnormalform_one(&domain, REF(f1), REF(f2)));
	CHECK(NOTEQUAL, libnormalform_not(libnormalform_one(&domain, REF(f1), REF(f2))));
	CHECK(NOTEQUAL, REF(v1));
	CHECK(NOTEQUAL, REF(f1));

#undef CHECK

	libnormalform_free(a);

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

	TEST_END;
}


#endif