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


/**
 * Check if two clauses have a term in common or
 * a term in common but mutually inverse
 * 
 * Both clauses must be clauses of binary connectives
 * 
 * @param   a               One of the clauses
 * @param   b               The other clause
 * @param   common_inv_out  Output parameter for whether the common term is mutually inverted
 * @param   a_common_out    Output parameter for `a`'s copy of the common term
 * @param   a_unique_out    Output parameter for `a`'s uncommon term
 * @param   b_common_out    Output parameter for `b`'s copy of the common term
 * @param   b_unique_out    Output parameter for `b`'s uncommon term
 * @return                  Whether the the clauses have a common or inversely common term
 */
static int
has_common(LIBNORMALFORM_SENTENCE *a, LIBNORMALFORM_SENTENCE *b, int *common_inv_out,
           LIBNORMALFORM_SENTENCE **a_common_out, LIBNORMALFORM_SENTENCE **a_unique_out,
           LIBNORMALFORM_SENTENCE **b_common_out, LIBNORMALFORM_SENTENCE **b_unique_out)
{
	LIBNORMALFORM_SENTENCE *al = LEFT(a);
	LIBNORMALFORM_SENTENCE *ar = RIGHT(a);
	LIBNORMALFORM_SENTENCE *bl = LEFT(b);
	LIBNORMALFORM_SENTENCE *br = RIGHT(b);

	if (al->equals(al, bl, common_inv_out)) {
		*a_common_out = al;
		*b_common_out = bl;
		*a_unique_out = ar;
		*b_unique_out = br;
		return 1;
	} else if (ar->equals(ar, br, common_inv_out)) {
		*a_common_out = ar;
		*b_common_out = br;
		*a_unique_out = al;
		*b_unique_out = bl;
		return 1;
	} else if (al->equals(al, br, common_inv_out)) {
		*a_common_out = al;
		*b_common_out = br;
		*a_unique_out = ar;
		*b_unique_out = bl;
		return 1;
	} else if (ar->equals(ar, bl, common_inv_out)) {
		*a_common_out = ar;
		*b_common_out = bl;
		*a_unique_out = al;
		*b_unique_out = br;
		return 1;
	}

	return 0;
}


LIBNORMALFORM_SENTENCE *
(libnormalform_xor2)(LIBNORMALFORM_SENTENCE *l, LIBNORMALFORM_SENTENCE *r)
{
	int inv;
	LIBNORMALFORM_SENTENCE *t, *not_a, *a, *b, *c;

	if (!l || !r) {
		libnormalform_free(l);
		libnormalform_free(r);
		return NULL;
	}

        if (l->equals(l, r, &inv)) {
		libnormalform_free(l);
		libnormalform_free(r);

		if (!inv) {
			/* x ⊕ x = 0 */
			return libnormalform_false();

		} else {
			/* x ⊕ ¬x = 1 */
			return libnormalform_true();
		}

	} else if (l->type == TYPE_TRUE) {
		/* 1 ⊕ x = (1 ∨ x) ∧ ¬(1 ∧ x) = 1 ∧ ¬x = ¬x */
		r = libnormalform_not(r);
	return_r:
		libnormalform_free(l);
		return r;

	} else if (l->type == TYPE_FALSE) {
		/* 0 ⊕ x = (0 ∨ x) ∧ ¬(0 ∧ x) = x ∧ ¬0 = x ∧ 1 = x */
		goto return_r;

	} else if (r->type == TYPE_TRUE) {
		/* x ⊕ 1 = 1 ⊕ x = ¬x */
		l = libnormalform_not(l);
	return_l:
		libnormalform_free(r);
		return l;

	} else if (r->type == TYPE_FALSE) {
		/* x ⊕ 0 = 0 ⊕ x = x */
		goto return_l;

	} else if (l->type == TYPE_OR && r->type == TYPE_OR) { /* TODO test */
		if (!has_common(l, r, &inv, &a, &b, &not_a, &c) || !inv)
			goto asis;
		/* (a ∨ b) ⊕ (¬a ∨ c) =
		 *     (a ∨ b ∨ ¬a ∨ c) ∧ ¬((a ∨ b) ∧ (¬a ∨ c)) =
		 *     ¬(a ∨ b) ∨ ¬(¬a ∨ c) */
		return libnormalform_or2(libnormalform_not(l), libnormalform_not(r));

	} else if (l->type == TYPE_AND && r->type == TYPE_AND) { /* TODO test */
		if (!has_common(l, r, &inv, &a, &b, &not_a, &c))
			goto asis;
		if (!inv) {
			/* (a ∧ b) ⊕ (a ∧ c) =
			 *     ((a ∧ b) ∨ (a ∧ c)) ∧ ¬((a ∧ b) ∧ (a ∧ c)) =
			 *     a ∧ (b ∨ c) ∧ ¬(a ∧ b ∧ c) =
			 *     a ∧ (b ∨ c) ∧ (¬a ∨ ¬b ∨ ¬c) =
			 *     a ∧ (b ∨ c) ∧ (¬b ∨ ¬c) =
			 *     a ∧ (b ⊕ c)
			 */
			a = libnormalform_ref(a);
			b = libnormalform_ref(b);
			c = libnormalform_ref(c);
			libnormalform_free(l);
			libnormalform_free(r);
			return libnormalform_and2(a, libnormalform_xor2(c, b));
		} else {
			/* (a ∧ b) ⊕ (¬a ∧ c) =
			 *     ((a ∧ b) ∨ (¬a ∧ c)) ∧ ¬((a ∧ b) ∧ (¬a ∧ c)) =
			 *     ((a ∧ b) ∨ (¬a ∧ c)) ∧ ¬(a ∧ b ∧ ¬a ∧ c) =
			 *     ((a ∧ b) ∨ (¬a ∧ c)) ∧ ¬⊥ =
			 *     (a ∧ b) ∨ (¬a ∧ c)
			 */
			return libnormalform_or2__(l, r);
		}

	} else if (l->type == TYPE_OR && r->type == TYPE_AND) { /* TODO test */
		t = l, l = r, r = t;
		goto and_xor_or;

	} else if (l->type == TYPE_AND && r->type == TYPE_OR) { /* TODO test */
	and_xor_or:
		if (!has_common(l, r, &inv, &a, &b, &not_a, &c))
			goto asis;
		if (!inv) {
			/* (a ∧ b) ⊕ (a ∨ c) =
			 *     ((a ∧ b) ∨ (a ∨ c)) ∧ ¬((a ∧ b) ∧ (a ∨ c)) =
			 *     ((a ∧ b) ∨ a ∨ c) ∧ ¬(a ∧ b ∧ (a ∨ c)) =
			 *     (a ∨ c) ∧ ¬(a ∧ b) =
			 *     ¬(a ∧ b) ∧ (a ∨ c)
			 */
			return libnormalform_and2__(libnormalform_not(l), r);
		} else {
			/* (a ∧ b) ⊕ (¬a ∨ c) =
			 *     ((a ∧ b) ∨ (¬a ∨ c)) ∧ ¬((a ∧ b) ∧ (¬a ∨ c)) =
			 *     ((a ∧ b) ∨ ¬a ∨ c) ∧ ¬(a ∧ b ∧ (¬a ∨ c)) =
			 *     ((a ∧ b) ∨ ¬a ∨ c) ∧ ¬(a ∧ b ∧ (⊥ ∨ c)) =
			 *     ((a ∧ b) ∨ ¬a ∨ c) ∧ ¬(a ∧ b ∧ c) =
			 *     ((a ∧ b) ∨ ¬a ∨ c) ∧ (¬a ∨ ¬b ∨ ¬c) =
			 *     (b ∨ ¬a ∨ c) ∧ (¬a ∨ ¬b ∨ ¬c) =
			 *     (¬a ∨ b ∨ c) ∧ (¬a ∨ ¬b ∨ ¬c) =
			 *     ¬a ∨ ((b ∨ c) ∧ (¬b ∨ ¬c)) =
			 *     ¬a ∨ (b ⊕ c)
			 */
			not_a = libnormalform_ref(not_a);
			b = libnormalform_ref(b);
			c = libnormalform_ref(c);
			libnormalform_free(l);
			libnormalform_free(r);
			return libnormalform_or2(not_a, libnormalform_xor2(c, b));
		}

	} else {
	asis:
		return libnormalform_xor2__(l, r);
	}
}


#else

#define USE_TWO
#include "libnormalform_xor.c"

#endif