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


LIBNORMALFORM_SENTENCE *
(libnormalform_and2)(LIBNORMALFORM_SENTENCE *l, LIBNORMALFORM_SENTENCE *r)
{
	LIBNORMALFORM_SENTENCE *ll, *lr;
	LIBNORMALFORM_SENTENCE *rl, *rr;
	int inv;

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

	if (l->equals(l, r, &inv)) {
		if (!inv) {
			/* x ∧ x = x */
			goto return_either;

		} else {
			/* x ∧ ¬x = 0 */
			libnormalform_free(l);
			libnormalform_free(r);
			return libnormalform_false();
		}

	} else if (l->type == TYPE_FALSE || r->type == TYPE_TRUE) {
		/* 0 ∧ x = 0 */
		/* x ∧ 1 = x */
	return_either:
		libnormalform_free(r);
		return l;

	} else if (r->type == TYPE_FALSE || l->type == TYPE_TRUE) {
		/* x ∧ 0 = 0 */
		/* 1 ∧ x = x */
		libnormalform_free(l);
		return r;

	} else if (l->hash == r->hash && l->type == TYPE_OR && r->type == TYPE_OR) {
		/* (x ∨ y) ∧ (¬x ∨ ¬y) = (x ∨ y) ∧ ¬(x ∧ y) = x ⊕ y */
		ll = l->data.binary.l;
		lr = l->data.binary.r;
		rl = r->data.binary.l;
		rr = r->data.binary.r;
		if (ll->hash != rl->hash || lr->hash != rr->hash)
			goto fallback;
		if (!ll->equals(ll, rl, &inv)) {
			if (ll->hash == lr->hash) {
				rl = r->data.binary.r;
				rr = r->data.binary.l;
				if (!ll->equals(ll, rl, &inv))
					goto fallback;
			} else {
				goto fallback;
			}
		}
		if (!inv || !lr->equals(lr, rr, &inv) || !inv)
			goto fallback;
		l->data.binary.l = NULL;
		l->data.binary.r = NULL;
		libnormalform_free(l);
		libnormalform_free(r);
		return libnormalform_xor2__(ll, lr);

	} else {
	fallback:
		return libnormalform_and2__(l, r);
	}
}


#else

#define USE_TWO
#include "libnormalform_and.c"

#endif