1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
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
|
