Second commitHEADmaster

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

1 files changed, 128 insertions, 0 deletions

diff --git a/libnormalform_xor2.c b/libnormalform_xor2.c
index a00c575..447d787 100644
--- a/libnormalform_xor2.c
+++ b/libnormalform_xor2.c
@@ -3,10 +3,66 @@
 #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);
@@ -49,7 +105,79 @@ LIBNORMALFORM_SENTENCE *
 		/* 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);
 	}
 }