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
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
|
/* See LICENSE file for copyright and license details. */
#include "common.h"
#ifndef TEST
LIBNORMALFORM_SENTENCE *
(libnormalform_not)(LIBNORMALFORM_SENTENCE *x)
{
LIBNORMALFORM_SENTENCE *ret;
if (!x)
return NULL;
ret = x->inverse(x);
libnormalform_free(x);
return ret;
}
#else
static int
tautology(void *user_data, void *input)
{
(void) user_data;
(void) input;
return 1;
}
static int
contradiction(void *user_data, void *input)
{
(void) user_data;
(void) input;
return 0;
}
int
main(void)
{
TEST_BEGIN;
struct libnormalform_variable var1, var2;
struct libnormalform_function fun1, fun2;
struct libnormalform_map domain;
LIBNORMALFORM_SENTENCE *a, *b, *v1, *v2, *f1, *f2;
int r1, r2;
var1.value = LIBNORMALFORM_FALSE;
var2.value = LIBNORMALFORM_TRUE;
fun1.evaluate = &tautology;
fun2.evaluate = &contradiction;
domain.nmappings = 0;
errno = 0;
ASSERT(!libnormalform_not(NULL) && errno == 0);
errno = 1;
ASSERT(!libnormalform_not(NULL) && errno == 1);
ASSUME(v1 = libnormalform_variable(&var1));
ASSUME(v2 = libnormalform_variable(&var2));
ASSUME(f1 = libnormalform_function(&fun1));
ASSUME(f2 = libnormalform_function(&fun2));
#define CHECK(X)\
do {\
ASSUME(a = libnormalform_not(REF(X)));\
ASSERT((X)->refcount == 1);\
ASSERT(a->refcount == 1);\
ASSERT_INVEQUAL(a, (X));\
ASSERT((r1 = a->evaluate(a, NULL)) >= 0);\
ASSERT((r2 = (X)->evaluate((X), NULL)) >= 0);\
ASSERT(r1 == 1 - r2);\
libnormalform_free(a);\
} while (0)
CHECK(v1);
CHECK(f1);
#undef CHECK
#define CHECK(X)\
do {\
ASSUME(b = (X));\
ASSUME(a = libnormalform_not(REF(b)));\
ASSERT(b->refcount == 1);\
ASSERT(a->refcount == 1);\
ASSERT_INVEQUAL(a, b);\
ASSERT((r1 = a->evaluate(a, NULL)) >= 0);\
ASSERT((r2 = b->evaluate(b, NULL)) >= 0);\
ASSERT(r1 == 1 - r2);\
libnormalform_free(a);\
libnormalform_free(b);\
} while (0)
CHECK(libnormalform_and2(REF(v1), REF(v2)));
CHECK(libnormalform_or2(REF(v1), REF(v2)));
CHECK(libnormalform_xor2(REF(v1), REF(v2)));
CHECK(libnormalform_all(&domain, REF(f1), REF(f2)));
CHECK(libnormalform_any(&domain, REF(f1), REF(f2)));
CHECK(libnormalform_one(&domain, REF(f1), REF(f2)));
#undef CHECK
libnormalform_free(v1);
libnormalform_free(v2);
libnormalform_free(f1);
libnormalform_free(f2);
TEST_END;
}
#endif
|
