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


/** 
 * See `.inverse` in `struct libnormalform_sentence` (Variable literal implementation)
 */
static LIBNORMALFORM_SENTENCE *
variable_inverse(LIBNORMALFORM_SENTENCE *this)
{
	LIBNORMALFORM_SENTENCE *ret = libnormalform_variable(this->data.literal.atom.variable);
	if (ret)
		ret->data.literal.inverted = this->data.literal.inverted ^ 1;
	return ret;
}


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


/** 
 * See `.evaluate` in `struct libnormalform_sentence` (Variable literal implementation)
 */
PURE static int
variable_evaluate(LIBNORMALFORM_SENTENCE *this, void *input)
{
	(void) input;
	return (this->data.literal.atom.variable->value != LIBNORMALFORM_FALSE) ^ this->data.literal.inverted;
}


LIBNORMALFORM_SENTENCE *
(libnormalform_variable)(struct libnormalform_variable *variable)
{
	static const struct libnormalform_sentence prototype = {
		PROTOTYPE_COMMON,
		.type = TYPE_VARIABLE,
		.inverse = &variable_inverse,
		.equals = &variable_equals,
		.evaluate = &variable_evaluate
	};

	LIBNORMALFORM_SENTENCE *ret = malloc(sizeof(*ret));
	if (ret) {
		*ret = prototype;
		ret->hash = LITERAL_HASH(variable);
		ret->data.literal.atom.variable = variable;
		ret->data.literal.inverted = 0;
	}
	return ret;
}


#else


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;

	ASSUME(a = libnormalform_variable(&var1));
	ASSERT(a->refcount == 1);
	ASSERT(a->travel_index == 0);
	ASSERT(a->travel_count == 0);
	ASSERT(a->type == TYPE_VARIABLE);
	ASSERT(a->data.literal.inverted == 0);
	ASSERT(a->data.literal.atom.variable == &var1);
	ASSERT_EQUAL(a, a);
	var1.value = LIBNORMALFORM_TRUE;
	ASSERT(libnormalform_evaluate(a) == 1);
	var1.value = LIBNORMALFORM_FALSE;
	ASSERT(libnormalform_evaluate(a) == 0);

	ASSUME(b = libnormalform_variable(&var1));
	ASSERT_EQUAL(a, b);
	ASSUME(b = libnormalform_not(b));
	ASSERT_INVEQUAL(a, b);
	ASSERT_INVEQUAL(b, a);
	libnormalform_free(b);

	ASSUME(b = libnormalform_variable(&var2));
	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(v2 = libnormalform_variable(&var2));
	ASSUME(f1 = libnormalform_function(&fun1));
	ASSUME(f2 = libnormalform_function(&fun2));

	ASSERT_NOTEQUAL(a, f1);

	ASSUME(b = libnormalform_and2(REF(v1), REF(v2)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);

	ASSUME(b = libnormalform_or2(REF(v1), REF(v2)));
	ASSERT_NOTEQUAL(a, b);
	libnormalform_free(b);

	ASSUME(b = libnormalform_xor2(REF(v1), REF(v2)));
	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);
	libnormalform_free(v1);
	libnormalform_free(v2);
	libnormalform_free(f1);
	libnormalform_free(f2);

	TEST_END;
}


#endif