From 4294ec0ed06ee34920c9edaeebaeb8b65c720791 Mon Sep 17 00:00:00 2001 From: Mattias Andrée Date: Fri, 19 Jul 2024 01:29:42 +0200 Subject: First commit MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Signed-off-by: Mattias Andrée --- libnormalform_or2.c | 82 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 82 insertions(+) create mode 100644 libnormalform_or2.c (limited to 'libnormalform_or2.c') diff --git a/libnormalform_or2.c b/libnormalform_or2.c new file mode 100644 index 0000000..51ed628 --- /dev/null +++ b/libnormalform_or2.c @@ -0,0 +1,82 @@ +/* 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 -- cgit v1.3.1