diff options
Diffstat (limited to '')
| -rw-r--r-- | libnormalform_xor2.c | 128 |
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, ¬_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, ¬_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, ¬_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); } } |