diff options
Diffstat (limited to '')
| -rw-r--r-- | libnormalform_xor2__.c | 174 |
1 files changed, 174 insertions, 0 deletions
diff --git a/libnormalform_xor2__.c b/libnormalform_xor2__.c new file mode 100644 index 0000000..c495428 --- /dev/null +++ b/libnormalform_xor2__.c @@ -0,0 +1,174 @@ +/* See LICENSE file for copyright and license details. */ +#include "common.h" +#ifndef TEST + + +/** + * See `.inverse` in `struct libnormalform_sentence` (XOR implementation) + */ +static LIBNORMALFORM_SENTENCE * +xor_inverse(LIBNORMALFORM_SENTENCE *this) +{ + /* ¬(l ⊕ r) = ¬l ⊕ r, (¬l ⊕ ¬r = l ⊕ r) */ + LIBNORMALFORM_SENTENCE *l, *r, *ret; + l = this->data.binary.l->inverse(this->data.binary.l); + if (!l) + return NULL; + r = libnormalform_ref(this->data.binary.r); + if (!r) { + libnormalform_free(l); + return NULL; + } + ret = libnormalform_xor2__(l, r); + if (ret && this->atom) { + ret->atom = this->atom; + ret->atom->refcount += 1; + } + return ret; +} + + +/** + * See `.equals` in `struct libnormalform_sentence` (XOR implementation) + */ +static int +xor_equals(LIBNORMALFORM_SENTENCE *this, LIBNORMALFORM_SENTENCE *other, int *inv_out) +{ + LIBNORMALFORM_SENTENCE *tl, *tr, *oll, *olr; + LIBNORMALFORM_SENTENCE *ol, *or, *orl, *orr; + int inv; + + if (other->type != TYPE_XOR) { + int invll, invrl, invlr, invrr; + if (this->hash != other->hash) + return 0; + if (other->type != TYPE_AND && other->type != TYPE_OR) + return 0; + /* a ⊕ b = (a ∨ b) ∧ (¬a ∨ ¬b) */ + /* ¬(a ⊕ b) = (a ∧ b) ∨ (¬a ∧ ¬b) */ + /* ¬(a ⊕ b) = (a ∨ ¬b) ∧ (¬a ∨ b) */ + /* a ⊕ b = (a ∧ ¬b) ∨ (¬a ∧ b) */ + tl = this->data.binary.l; + tr = this->data.binary.r; + ol = other->data.binary.l; + or = other->data.binary.r; + if (ol->hash != or->hash) + return 0; + if (ol->type != or->type) + return 0; + if ((ol->type ^ other->type) != (TYPE_AND ^ TYPE_OR)) + return 0; + oll = ol->data.binary.l; + olr = ol->data.binary.r; + orl = or->data.binary.l; + orr = or->data.binary.r; + if (!tl->equals(tl, oll, &invll)) { + oll = ol->data.binary.r; + olr = ol->data.binary.l; + if (!tl->equals(tl, oll, &invll)) + return 0; + } + if (!tl->equals(tl, orl, &invrl)) { + orl = or->data.binary.r; + orr = or->data.binary.l; + if (!tl->equals(tl, orl, &invrl)) + return 0; + } + if (invll == invrl) + return 0; + if (!tr->equals(tr, olr, &invlr)) + return 0; + if (!tr->equals(tr, orr, &invrr)) + return 0; + if (invlr == invrr) + return 0; + *inv_out = (invll == invlr) == (other->type == TYPE_OR); + return 1; + } + + tl = this->data.binary.l; + tr = this->data.binary.r; + ol = other->data.binary.l; + or = other->data.binary.r; + + if (tl->hash != ol->hash || tr->hash != or->hash) + return 0; + + if (!tl->equals(tl, ol, inv_out)) { + if (tl->hash == tr->hash) { + ol = other->data.binary.r; + or = other->data.binary.l; + if (!tl->equals(tl, ol, inv_out)) + return 0; + } else { + return 0; + } + } + if (!tr->equals(tr, or, &inv)) + return 0; + *inv_out ^= inv; + return 1; +} + + +/** + * See `.evaluate` in `struct libnormalform_sentence` (XOR implementation) + */ +static int +xor_evaluate(LIBNORMALFORM_SENTENCE *this, void *input) +{ + int l, r; + + l = this->data.binary.l->evaluate(this->data.binary.l, input); + if (l < 0) + return l; + + r = this->data.binary.r->evaluate(this->data.binary.r, input); + if (r < 0) + return r; + + return l ^ r; +} + + +LIBNORMALFORM_SENTENCE * +(libnormalform_xor2__)(LIBNORMALFORM_SENTENCE *l, LIBNORMALFORM_SENTENCE *r) +{ + static const struct libnormalform_sentence prototype = { + PROTOTYPE_COMMON, + .type = TYPE_XOR, + .inverse = &xor_inverse, + .equals = &xor_equals, + .evaluate = &xor_evaluate + }; + + LIBNORMALFORM_SENTENCE *ret = malloc(sizeof(*ret)); + if (!ret) { + libnormalform_free(l); + libnormalform_free(r); + return NULL; + } + *ret = prototype; + ret->hash = XOR_HASH(l, r); + if (l->hash <= r->hash) { + ret->data.binary.l = l; + ret->data.binary.r = r; + } else { + ret->data.binary.l = r; + ret->data.binary.r = l; + } + return ret; +} + + +#else + + +CONST int +main(void) +{ + return 0; /* indirectly tested */ +} + + +#endif |