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


/**
 * Create a shallow clone of a sentence
 * 
 * Any non-`NULL` `.copy_for_clone` in any
 * `struct libnormalform_variable *`,
 * `struct libnormalform_function *`, or
 * `struct libnormalform_map *` will be applied
 * 
 * @param   this    The sentence
 * @param   map     Sufficiently large array of already constructed clones,
 *                  will be updated with a the clone if `this` has a slot
 *                  and `NULL` is stored in the slot
 * @param   ap_out  Output parameter for one of `this`'s substatements;
 *                  `NULL` will be stored in `*ap_out` if `this` does not
 *                  have any substatements
 * @param   bp_out  Output parameter for `this`'s other substatement;
 *                  `NULL` will be stored in `*bp_out` if `this` does not
 *                  have any substatements
 * @return          The clone of `this`, `NULL` on failure
 */
USE_RESULT SOME_NONNULL_INPUT(1, 3, 4)
static LIBNORMALFORM_SENTENCE *
shallow_clone(LIBNORMALFORM_SENTENCE *this, LIBNORMALFORM_SENTENCE **map,
              LIBNORMALFORM_SENTENCE ***ap_out, LIBNORMALFORM_SENTENCE ***bp_out)
{
	LIBNORMALFORM_SENTENCE *ret;

	*ap_out = NULL;
	*bp_out = NULL;

	if (this->travel_count > 1 && map[this->travel_index]) {
		map[this->travel_index]->refcount += 1;
		return map[this->travel_index];
	}

	ret = malloc(sizeof(*ret));
	if (!ret)
		return NULL;

	memcpy(ret, this, sizeof(*ret));
	ret->refcount = 1;
	ret->atom = NULL;

	switch (ret->type) {
	case TYPE_ALL:
	case TYPE_ANY:
	case TYPE_ONE:
	case TYPE_NOT_ONE:
		if (ret->data.qualifier.domain->copy_for_clone)
			ret->data.qualifier.domain = ret->data.qualifier.domain->copy_for_clone;
		/* fall through */

	case TYPE_AND:
	case TYPE_OR:
	case TYPE_XOR:
		*ap_out = &LEFT(ret);
		*bp_out = &RIGHT(ret);
		/* fall through */

	case TYPE_TRUE:
	case TYPE_FALSE:
		break;

	case TYPE_VARIABLE:
		if (ret->data.literal.atom.variable->copy_for_clone)
			ret->data.literal.atom.variable = ret->data.literal.atom.variable->copy_for_clone;
		break;

	case TYPE_FUNCTION:
		if (ret->data.literal.atom.function->copy_for_clone)
			ret->data.literal.atom.function = ret->data.literal.atom.function->copy_for_clone;
		break;

	case TYPE_TRANS:
		if (ret->data.trans.function->copy_for_clone)
			ret->data.trans.function = ret->data.trans.function->copy_for_clone;
		*bp_out = &ret->data.trans.input;
		break;

	default:
		abort();
	}

	if (this->travel_count > 1)
		map[this->travel_index] = ret;

	return ret;
}


/**
 * Create a deep clone of a sentence
 *
 * @param   ret_out  Output parameter for the clone
 * @param   this     The sentence
 * @param   map      Sufficiently large array of already constructed clones,
 *                   will be updated with a the clone if `this` has a slot
 *                   and `NULL` is stored in the slot
 * @return           0 on success, -1 on failure
 */
USE_RESULT SOME_NONNULL_INPUT(1, 2)
static int
deep_clone(LIBNORMALFORM_SENTENCE **ret_out, LIBNORMALFORM_SENTENCE *this, LIBNORMALFORM_SENTENCE **map)
{
	LIBNORMALFORM_SENTENCE **ap, **bp;
	LIBNORMALFORM_SENTENCE *a = NULL, *b = NULL; /* initialised to silence compiler */

	for (;;) {
		*ret_out = shallow_clone(this, map, &ap, &bp);
		if (ap && !bp)
			bp = ap, ap = NULL;
		if (ap)
			a = *ap, *ap = NULL;
		if (bp)
			b = *bp, *bp = NULL;
		if (!*ret_out)
			return -1;

		if (ap)
			if (deep_clone(ap, a, map))
				return -1;

		if (!bp)
			break;
		ret_out = bp;
		this = b;
	}

	return 0;
}


LIBNORMALFORM_SENTENCE *
(libnormalform_clone)(LIBNORMALFORM_SENTENCE *this)
{
	LIBNORMALFORM_SENTENCE *ret = NULL;
	LIBNORMALFORM_SENTENCE **map;
	size_t dupcount;

	if (!this)
		return ret;

	map = NULL;
	dupcount = libnormalform_set_indices_and_counts__(this);
	if (dupcount) {
		/* ideality, we would skip this part and let shallow_clone,
		 * store the first clone, however since there is no guarantee
		 * that NULL and 0 have the same representation, we cannot reuse
		 * the memory of `.travel_index` (needed by libnormalform_to_string)
		 * for this purpose, so either we do this, or we add another
		 * seldomly used member to `struct libnormalform_sentence` */
		map = malloc(dupcount * sizeof(*map));
		if (!map)
			goto out;
		while (dupcount--)
			map[dupcount] = NULL;
	}
	if (deep_clone(&ret, this, map)) {
		libnormalform_free(ret);
		ret = NULL;
	}
	free(map);
out:
	libnormalform_reset_indices_and_counts__(this);
	return ret;
}


#else


static void
test_simple(void)
{
	struct libnormalform_variable var1, var2;
	struct libnormalform_function fun1, fun2;
	struct libnormalform_map dom1, dom2;
	LIBNORMALFORM_SENTENCE *a, *b;

	ASSUME(a = libnormalform_true());
	ASSUME(b = libnormalform_clone(a));
	ASSERT(a != b);
	ASSERT(a->refcount == 1);
	ASSERT(b->refcount == 1);
	ASSERT_EQUAL(a, b);
	libnormalform_free(a);
	libnormalform_free(b);

	ASSUME(a = libnormalform_false());
	ASSUME(b = libnormalform_clone(a));
	ASSERT(a != b);
	ASSERT(a->refcount == 1);
	ASSERT(b->refcount == 1);
	ASSERT_EQUAL(a, b);
	libnormalform_free(a);
	libnormalform_free(b);

	var1.copy_for_clone = NULL;
	ASSUME(a = libnormalform_variable(&var1));
	ASSUME(b = libnormalform_clone(a));
	ASSERT(a != b);
	ASSERT(a->refcount == 1);
	ASSERT(b->refcount == 1);
	ASSERT_EQUAL(a, b);
	libnormalform_free(a);
	libnormalform_free(b);

	var1.copy_for_clone = &var2;
	ASSUME(a = libnormalform_variable(&var1));
	ASSUME(b = libnormalform_clone(a));
	ASSERT(a != b);
	ASSERT(a->refcount == 1);
	ASSERT(b->refcount == 1);
	ASSERT(a->type == TYPE_VARIABLE);
	ASSERT(b->type == TYPE_VARIABLE);
	ASSERT(a->data.literal.atom.variable == &var1);
	ASSERT(b->data.literal.atom.variable == &var2);
	ASSERT_NOTEQUAL(a, b);
	b->data.literal.atom.variable = &var1;
	ASSERT_EQUAL(a, b);
	libnormalform_free(a);
	libnormalform_free(b);

	fun1.copy_for_clone = NULL;
	ASSUME(a = libnormalform_function(&fun1));
	ASSUME(b = libnormalform_clone(a));
	ASSERT(a != b);
	ASSERT(a->refcount == 1);
	ASSERT(b->refcount == 1);
	ASSERT_EQUAL(a, b);
	libnormalform_free(a);
	libnormalform_free(b);

	fun1.copy_for_clone = &fun2;
	ASSUME(a = libnormalform_function(&fun1));
	ASSUME(b = libnormalform_clone(a));
	ASSERT(a != b);
	ASSERT(a->refcount == 1);
	ASSERT(b->refcount == 1);
	ASSERT(a->type == TYPE_FUNCTION);
	ASSERT(b->type == TYPE_FUNCTION);
	ASSERT(a->data.literal.atom.function == &fun1);
	ASSERT(b->data.literal.atom.function == &fun2);
	ASSERT_NOTEQUAL(a, b);
	b->data.literal.atom.function = &fun1;
	ASSERT_EQUAL(a, b);
	libnormalform_free(a);
	libnormalform_free(b);

	var1.copy_for_clone = NULL;
	fun1.copy_for_clone = NULL;
	ASSUME(a = libnormalform_and2(libnormalform_variable(&var1), libnormalform_function(&fun1)));
	ASSUME(b = libnormalform_clone(a));
	ASSERT(a != b);
	ASSERT(a->refcount == 1);
	ASSERT(b->refcount == 1);
	ASSERT_EQUAL(a, b);
	libnormalform_free(a);
	libnormalform_free(b);

	var1.copy_for_clone = NULL;
	fun1.copy_for_clone = NULL;
	ASSUME(a = libnormalform_or2(libnormalform_variable(&var1), libnormalform_function(&fun1)));
	ASSUME(b = libnormalform_clone(a));
	ASSERT(a != b);
	ASSERT(a->refcount == 1);
	ASSERT(b->refcount == 1);
	ASSERT_EQUAL(a, b);
	libnormalform_free(a);
	libnormalform_free(b);

	var1.copy_for_clone = NULL;
	fun1.copy_for_clone = NULL;
	ASSUME(a = libnormalform_xor2(libnormalform_variable(&var1), libnormalform_function(&fun1)));
	ASSUME(b = libnormalform_clone(a));
	ASSERT(a != b);
	ASSERT(a->refcount == 1);
	ASSERT(b->refcount == 1);
	ASSERT_EQUAL(a, b);
	libnormalform_free(a);
	libnormalform_free(b);

	dom1.copy_for_clone = NULL;
	fun1.copy_for_clone = NULL;
	var1.copy_for_clone = NULL;
	ASSUME(a = libnormalform_all(&dom1, libnormalform_function(&fun1), libnormalform_variable(&var1)));
	ASSUME(b = libnormalform_clone(a));
	ASSERT(a != b);
	ASSERT(a->refcount == 1);
	ASSERT(b->refcount == 1);
	ASSERT_EQUAL(a, b);
	libnormalform_free(a);
	libnormalform_free(b);

	dom1.copy_for_clone = &dom2;
	fun1.copy_for_clone = NULL;
	var1.copy_for_clone = NULL;
	ASSUME(a = libnormalform_all(&dom1, libnormalform_function(&fun1), libnormalform_variable(&var1)));
	ASSUME(b = libnormalform_clone(a));
	ASSERT(a != b);
	ASSERT(a->refcount == 1);
	ASSERT(b->refcount == 1);
	ASSERT(a->type == TYPE_ALL);
	ASSERT(b->type == TYPE_ALL);
	ASSERT(a->data.qualifier.domain == &dom1);
	ASSERT(b->data.qualifier.domain == &dom2);
	ASSERT_NOTEQUAL(a, b);
	b->data.qualifier.domain = &dom1;
	ASSERT_EQUAL(a, b);
	libnormalform_free(a);
	libnormalform_free(b);

	dom1.copy_for_clone = NULL;
	fun1.copy_for_clone = NULL;
	var1.copy_for_clone = NULL;
	ASSUME(a = libnormalform_any(&dom1, libnormalform_function(&fun1), libnormalform_variable(&var1)));
	ASSUME(b = libnormalform_clone(a));
	ASSERT(a != b);
	ASSERT(a->refcount == 1);
	ASSERT(b->refcount == 1);
	ASSERT_EQUAL(a, b);
	libnormalform_free(a);
	libnormalform_free(b);

	dom1.copy_for_clone = &dom2;
	fun1.copy_for_clone = NULL;
	var1.copy_for_clone = NULL;
	ASSUME(a = libnormalform_any(&dom1, libnormalform_function(&fun1), libnormalform_variable(&var1)));
	ASSUME(b = libnormalform_clone(a));
	ASSERT(a != b);
	ASSERT(a->refcount == 1);
	ASSERT(b->refcount == 1);
	ASSERT(a->type == TYPE_ANY);
	ASSERT(b->type == TYPE_ANY);
	ASSERT(a->data.qualifier.domain == &dom1);
	ASSERT(b->data.qualifier.domain == &dom2);
	ASSERT_NOTEQUAL(a, b);
	b->data.qualifier.domain = &dom1;
	ASSERT_EQUAL(a, b);
	libnormalform_free(a);
	libnormalform_free(b);

	dom1.copy_for_clone = NULL;
	fun1.copy_for_clone = NULL;
	var1.copy_for_clone = NULL;
	ASSUME(a = libnormalform_one(&dom1, libnormalform_function(&fun1), libnormalform_variable(&var1)));
	ASSUME(b = libnormalform_clone(a));
	ASSERT(a != b);
	ASSERT(a->refcount == 1);
	ASSERT(b->refcount == 1);
	ASSERT_EQUAL(a, b);
	libnormalform_free(a);
	libnormalform_free(b);

	dom1.copy_for_clone = &dom2;
	fun1.copy_for_clone = NULL;
	var1.copy_for_clone = NULL;
	ASSUME(a = libnormalform_one(&dom1, libnormalform_function(&fun1), libnormalform_variable(&var1)));
	ASSUME(b = libnormalform_clone(a));
	ASSERT(a != b);
	ASSERT(a->refcount == 1);
	ASSERT(b->refcount == 1);
	ASSERT(a->type == TYPE_ONE);
	ASSERT(b->type == TYPE_ONE);
	ASSERT(a->data.qualifier.domain == &dom1);
	ASSERT(b->data.qualifier.domain == &dom2);
	ASSERT_NOTEQUAL(a, b);
	b->data.qualifier.domain = &dom1;
	ASSERT_EQUAL(a, b);
	libnormalform_free(a);
	libnormalform_free(b);

	dom1.copy_for_clone = NULL;
	fun1.copy_for_clone = NULL;
	var1.copy_for_clone = NULL;
	ASSUME(a = libnormalform_one(&dom1, libnormalform_function(&fun1), libnormalform_variable(&var1)));
	ASSUME(a = libnormalform_not(a));
	ASSUME(b = libnormalform_clone(a));
	ASSERT(a != b);
	ASSERT(a->refcount == 1);
	ASSERT(b->refcount == 1);
	ASSERT_EQUAL(a, b);
	libnormalform_free(a);
	libnormalform_free(b);

	dom1.copy_for_clone = &dom2;
	fun1.copy_for_clone = NULL;
	var1.copy_for_clone = NULL;
	ASSUME(a = libnormalform_one(&dom1, libnormalform_function(&fun1), libnormalform_variable(&var1)));
	ASSUME(a = libnormalform_not(a));
	ASSUME(b = libnormalform_clone(a));
	ASSERT(a != b);
	ASSERT(a->refcount == 1);
	ASSERT(b->refcount == 1);
	ASSERT(a->type == TYPE_NOT_ONE);
	ASSERT(b->type == TYPE_NOT_ONE);
	ASSERT(a->data.qualifier.domain == &dom1);
	ASSERT(b->data.qualifier.domain == &dom2);
	ASSERT_NOTEQUAL(a, b);
	b->data.qualifier.domain = &dom1;
	ASSERT_EQUAL(a, b);
	libnormalform_free(a);
	libnormalform_free(b);
}


static void
test_multientry(void)
{
	struct libnormalform_variable var1;
	struct libnormalform_map dom1;
	LIBNORMALFORM_SENTENCE *a, *b;

	dom1.copy_for_clone = NULL;
	var1.copy_for_clone = NULL;
	ASSUME(a = libnormalform_variable(&var1));
	ASSUME(a = libnormalform_all(&dom1, REF(a), a));
	ASSERT(a->type == TYPE_ALL);
	ASSERT(LEFT(a) == RIGHT(a));
	ASSERT(LEFT(a)->refcount = 2);
	ASSUME(b = libnormalform_clone(a));
	ASSERT(a != b);
	ASSERT(a->refcount == 1);
	ASSERT(b->refcount == 1);
	ASSERT(b->type == TYPE_ALL);
	ASSERT(LEFT(b) == RIGHT(b));
	ASSERT(LEFT(b) != LEFT(a));
	ASSERT(LEFT(b)->refcount = 2);
	ASSERT_EQUAL(a, b);
	libnormalform_free(b);
	libnormalform_free(a);
}


static void
test_complex(void)
{
#define U(NAME) NAME = {.copy_for_clone = NULL, .identifier = #NAME}

	struct libnormalform_variable U(var1), U(var2);
	struct libnormalform_function U(fun1), U(fun2);
	struct libnormalform_map U(dom1);
	LIBNORMALFORM_SENTENCE *a, *b;

	ASSUME(a =
		libnormalform_any(&dom1,
			libnormalform_true(),
			LIBNORMALFORM_AND(
				libnormalform_function(&fun1),
				libnormalform_function(&fun2),
				libnormalform_variable(&var1),
				libnormalform_variable(&var2)
			)
		)
	);
	ASSUME(b = libnormalform_clone(a));
	ASSERT(a != b);
	ASSERT_EQUAL(a, b);

	ASSUME(a =
		LIBNORMALFORM_OR(
			a,
			libnormalform_xor2(
				libnormalform_function(&fun1),
				libnormalform_variable(&var1)),
			libnormalform_function(&fun2),
			libnormalform_all(&dom1,
				LIBNORMALFORM_AND(
					libnormalform_function(&fun1),
					libnormalform_function(&fun2),
					libnormalform_variable(&var1),
					libnormalform_variable(&var2)
				),
				libnormalform_xor2(
					libnormalform_function(&fun1),
					b)
			)
		)
	);
	ASSUME(b = libnormalform_clone(a));
	ASSERT(a != b);
	ASSERT_EQUAL(a, b);

	libnormalform_free(b);
	libnormalform_free(a);

#undef U
}


static void
test_complex_multientry(void)
{
#define U(NAME) NAME = {.copy_for_clone = NULL, .identifier = #NAME}

	struct libnormalform_variable U(var1), U(var2);
	struct libnormalform_function U(fun1), U(fun2);
	struct libnormalform_map U(dom1);
	LIBNORMALFORM_SENTENCE *a, *b, *ref1, *ref2, *ref3, *ref4;

	ASSUME(a =
		libnormalform_any(&dom1,
			libnormalform_true(),
			ref4 = REF(LIBNORMALFORM_AND(
				ref1 = REF(libnormalform_function(&fun1)),
				ref2 = REF(libnormalform_function(&fun2)),
				ref3 = REF(libnormalform_variable(&var1)),
				libnormalform_variable(&var2)
			))
		)
	);
	ASSUME(a =
		LIBNORMALFORM_OR(
			a,
			libnormalform_xor2(REF(ref1), REF(ref3)),
			REF(ref2),
			libnormalform_all(&dom1,
				REF(ref4),
				libnormalform_xor2(REF(ref1), REF(a))
			)
		)
	);

	libnormalform_free(ref1);
	libnormalform_free(ref2);
	libnormalform_free(ref3);
	libnormalform_free(ref4);

	ASSUME(b = libnormalform_clone(a));
	ASSERT(a != b);
	ASSERT_EQUAL(a, b);
	libnormalform_free(b);
	libnormalform_free(a);

#undef U
}


int
main(void)
{
	TEST_BEGIN;

	test_simple();
	test_multientry();
	test_complex();
	test_complex_multientry();

	TEST_END;
}


#endif