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


/** 
 * See `.inverse` in `struct libnormalform_sentence` (Function literal implementation)
 */
static LIBNORMALFORM_SENTENCE *
function_inverse(LIBNORMALFORM_SENTENCE *this)
{
	LIBNORMALFORM_SENTENCE *ret = libnormalform_function(this->data.literal.atom.function);
	if (ret)
		ret->data.literal.inverted = this->data.literal.inverted ^ 1;
	return ret;
}


/** 
 * See `.equals` in `struct libnormalform_sentence` (Function literal implementation)
 */
static int
function_equals(LIBNORMALFORM_SENTENCE *this, LIBNORMALFORM_SENTENCE *other, int *inv_out)
{
	if (other->type != TYPE_FUNCTION || this->data.literal.atom.function != other->data.literal.atom.function)
		return 0;
	*inv_out = this->data.literal.inverted ^ other->data.literal.inverted;
	return 1;
}


/** 
 * See `.evaluate` in `struct libnormalform_sentence` (Function literal implementation)
 */
static int
function_evaluate(LIBNORMALFORM_SENTENCE *this, void *input)
{
	int r = this->data.literal.atom.function->evaluate(this->data.literal.atom.function->user_data, input);
	return r < 0 ? r : ((r > 0) ^ this->data.literal.inverted);
}


LIBNORMALFORM_SENTENCE *
(libnormalform_function)(struct libnormalform_function *function)
{
	static const struct libnormalform_sentence prototype = {
		PROTOTYPE_COMMON,
		.type = TYPE_FUNCTION,
		.inverse = &function_inverse,
		.equals = &function_equals,
		.evaluate = &function_evaluate
	};

	LIBNORMALFORM_SENTENCE *ret = malloc(sizeof(*ret));
	if (ret) {
		*ret = prototype;
		ret->hash = LITERAL_HASH(function);
		ret->data.literal.atom.function = function;
		ret->data.literal.inverted = 0;
	}
	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;
}


static int
einval(void *user_data, void *input)
{
	(void) user_data;
	(void) input;
	errno = EINVAL;
	return -1;
}


int
main(void)
{
	TEST_BEGIN;

	struct libnormalform_function fun1, fun2;
	struct libnormalform_variable var1;
	struct libnormalform_mapping map[1];
	struct libnormalform_map domain;
	LIBNORMALFORM_SENTENCE *a, *b, *v1, *f1, *f2;

	domain.nmappings = 0;

	ASSUME(a = libnormalform_function(&fun1));
	ASSERT(a->refcount == 1);
	ASSERT(a->travel_index == 0);
	ASSERT(a->travel_count == 0);
	ASSERT(a->type == TYPE_FUNCTION);
	ASSERT(a->data.literal.inverted == 0);
	ASSERT(a->data.literal.atom.function == &fun1);
	ASSERT_EQUAL(a, a);
	fun1.evaluate = tautology;
	ASSERT(libnormalform_evaluate(a) == 1);
	fun1.evaluate = contradiction;
	ASSERT(libnormalform_evaluate(a) == 0);
	fun1.evaluate = einval;
	errno = 0;
	ASSERT(libnormalform_evaluate(a) == -1 && errno == EINVAL);

	ASSUME(b = libnormalform_function(&fun1));
	ASSERT_EQUAL(a, b);
	ASSUME(b = libnormalform_not(b));
	ASSERT_INVEQUAL(a, b);
	ASSERT_INVEQUAL(b, a);
	libnormalform_free(b);

	ASSUME(b = libnormalform_function(&fun2));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);

	ASSUME(b = libnormalform_true());
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);

	ASSUME(b = libnormalform_false());
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);

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

	ASSERT_NOTEQUAL(a, v1);

	ASSUME(b = libnormalform_and2(REF(f1), REF(f2)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);

	ASSUME(b = libnormalform_or2(REF(f1), REF(f2)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);

	ASSUME(b = libnormalform_xor2(REF(f1), REF(f2)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);

	ASSUME(b = libnormalform_all(&domain, REF(f1), REF(f2)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);

	ASSUME(b = libnormalform_any(&domain, REF(f1), REF(f2)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);

	ASSUME(b = libnormalform_one(&domain, REF(f1), REF(f2)));
	ASSERT_NOTEQUAL(a, b);
	ASSUME(b = libnormalform_not(b));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);

	libnormalform_free(a);

	ASSUME(a = libnormalform_function(&fun1));
	ASSUME(b = libnormalform_function(&fun2));
	ASSUME(a = libnormalform_and2(a, b));
	fun1.evaluate = tautology;
	fun2.evaluate = einval;
	errno = 0;
	ASSERT(libnormalform_evaluate(a) == -1 && errno == EINVAL);
	fun1.evaluate = einval;
	fun2.evaluate = tautology;
	errno = 0;
	ASSERT(libnormalform_evaluate(a) == -1 && errno == EINVAL);
	fun1.evaluate = tautology;
	fun2.evaluate = tautology;
	ASSERT(libnormalform_evaluate(a) == 1);
	libnormalform_free(a);

	ASSUME(a = libnormalform_function(&fun1));
	ASSUME(b = libnormalform_function(&fun2));
	ASSUME(a = libnormalform_or2(a, b));
	fun1.evaluate = contradiction;
	fun2.evaluate = einval;
	errno = 0;
	ASSERT(libnormalform_evaluate(a) == -1 && errno == EINVAL);
	fun1.evaluate = einval;
	fun2.evaluate = contradiction;
	errno = 0;
	ASSERT(libnormalform_evaluate(a) == -1 && errno == EINVAL);
	fun1.evaluate = contradiction;
	fun2.evaluate = contradiction;
	ASSERT(libnormalform_evaluate(a) == 0);
	libnormalform_free(a);

	ASSUME(a = libnormalform_function(&fun1));
	ASSUME(b = libnormalform_function(&fun2));
	ASSUME(a = libnormalform_xor2(a, b));
	fun1.evaluate = contradiction;
	fun2.evaluate = einval;
	errno = 0;
	ASSERT(libnormalform_evaluate(a) == -1 && errno == EINVAL);
	fun1.evaluate = einval;
	fun2.evaluate = contradiction;
	errno = 0;
	ASSERT(libnormalform_evaluate(a) == -1 && errno == EINVAL);
	fun1.evaluate = contradiction;
	fun2.evaluate = contradiction;
	ASSERT(libnormalform_evaluate(a) == 0);
	libnormalform_free(a);

	domain.nmappings = 1;
	domain.mappings = map;
	map[0].key = NULL;
	map[0].value = NULL;

	ASSUME(a = libnormalform_function(&fun1));
	ASSUME(b = libnormalform_function(&fun2));
	ASSUME(a = libnormalform_all(&domain, a, b));
	fun1.evaluate = tautology;
	fun2.evaluate = einval;
	errno = 0;
	ASSERT(libnormalform_evaluate(a) == -1 && errno == EINVAL);
	fun1.evaluate = einval;
	fun2.evaluate = tautology;
	errno = 0;
	ASSERT(libnormalform_evaluate(a) == -1 && errno == EINVAL);
	fun1.evaluate = tautology;
	fun2.evaluate = tautology;
	ASSERT(libnormalform_evaluate(a) == 1);
	libnormalform_free(a);

	ASSUME(a = libnormalform_function(&fun1));
	ASSUME(b = libnormalform_function(&fun2));
	ASSUME(a = libnormalform_any(&domain, a, b));
	fun1.evaluate = tautology;
	fun2.evaluate = einval;
	errno = 0;
	ASSERT(libnormalform_evaluate(a) == -1 && errno == EINVAL);
	fun1.evaluate = einval;
	fun2.evaluate = tautology;
	errno = 0;
	ASSERT(libnormalform_evaluate(a) == -1 && errno == EINVAL);
	fun1.evaluate = tautology;
	fun2.evaluate = tautology;
	ASSERT(libnormalform_evaluate(a) == 1);
	libnormalform_free(a);

	ASSUME(a = libnormalform_function(&fun1));
	ASSUME(b = libnormalform_function(&fun2));
	ASSUME(a = libnormalform_one(&domain, a, b));
	fun1.evaluate = tautology;
	fun2.evaluate = einval;
	errno = 0;
	ASSERT(libnormalform_evaluate(a) == -1 && errno == EINVAL);
	fun1.evaluate = einval;
	fun2.evaluate = tautology;
	errno = 0;
	ASSERT(libnormalform_evaluate(a) == -1 && errno == EINVAL);
	fun1.evaluate = tautology;
	fun2.evaluate = tautology;
	ASSERT(libnormalform_evaluate(a) == 1);
	libnormalform_free(a);

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

	TEST_END;
}


#endif