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


LIBNORMALFORM_SENTENCE *
(libnormalform_or2)(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 = 1 */
			libnormalform_free(l);
			libnormalform_free(r);
			return libnormalform_true();
		}

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

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

	} else if (l->hash == r->hash && l->type == TYPE_AND && r->type == TYPE_AND) {
		/* (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;
		r->data.binary.r = NULL;
		libnormalform_free(l);
		libnormalform_free(r);
		return libnormalform_xor2__(ll, rr);

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


#else

#define USE_TWO
#include "libnormalform_or.c"

#endif