-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathHH.c
75 lines (64 loc) · 1.41 KB
/
HH.c
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
#include <stdlib.h>
#define DECL(Name) \
struct Name; \
typedef struct Name Name
#define UDECL(Name) \
union Name; \
typedef union Name Name
#define STRUCT(Name) \
struct Name; \
typedef struct Name Name; \
struct Name
#define UNION(Name) \
union Name; \
typedef struct Name Name; \
union Name
DECL(Goal);
DECL(AndGoal);
DECL(OrGoal);
DECL(ExistsGoal);
DECL(ForallGoal);
DECL(IfGoal);
DECL(Clause);
DECL(HornClause);
DECL(AndClause);
DECL(ForallClause);
DECL(Atom);
DECL(Unification);
DECL(Relation);
STRUCT(Variable) { Clause* c; };
STRUCT(Universe) {
Universe* parent;
Variable* v;
};
STRUCT(Atom) { char* name; };
STRUCT(AndGoal) { Goal* g1; Goal* g2; };
STRUCT(OrGoal) { Goal* g1; Goal* g2; };
STRUCT(ExistsGoal) { Universe u; Goal* g; };
STRUCT(ForallGoal) { Universe u; Goal* g; };
STRUCT(IfGoal) { Clause* cond; Goal* then; };
STRUCT(Goal) {
union {
Atom a;
AndGoal ag;
OrGoal og;
ExistsGoal eg;
ForallGoal fg;
IfGoal ig;
};
unsigned char l;
};
STRUCT(HornClause) { Atom* a; };
STRUCT(AndClause) { Clause* c1; Clause* c2; };
STRUCT(ForallClause) { Universe u; Clause* c; };
STRUCT(Clause) {
union {
Atom a;
HornClause hc;
AndClause ac;
ForallClause fc;
}
unsigned char l;
}
typedef size_t Universe;
int main() {}