First commit

Signed-off-by: Mattias Andrée <maandree@kth.se>

1 files changed, 82 insertions, 0 deletions

diff --git a/libnormalform_and2.c b/libnormalform_and2.c
new file mode 100644
index 0000000..62d8db3
--- /dev/null
+++ b/libnormalform_and2.c
@@ -0,0 +1,82 @@
+/* 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