-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathproplogic.y
129 lines (100 loc) · 2.4 KB
/
proplogic.y
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
116
117
118
119
120
121
122
123
124
125
126
127
128
129
%{
#include <stdio.h>
#include <stdlib.h>
#include <stdarg.h>
#include "proplogic.h"
/* prototypes */
nodeType *opr(int oper, int nops, ...);
nodeType *id(int i);
nodeType *con(int value);
void freeNode(nodeType *p);
int ex(nodeType *p);
int yylex(void);
void yyerror(char *s);
int sym[26]; /* symbol table */
%}
%union {
char sIndex; /* symbol table index */
nodeType *nPtr; /* node pointer */
};
%token <sIndex> VARIABLE
%token TRUE
%token FALSE
%left NOT EQUIV OR AND IMPLIES
%type <nPtr> formula term literal
%%
formula:
formula { $$ = $1;}
| term '|' formula {$$ = opr('|', 2, $1, $3); }
|
;
term:
literal {$$ = $1; }
| term '&' term { $$ = opr('&', 2, $1, $3); }
;
literal:
VARIABLE { $$ = id($1); }
| '!' literal {$$ = opr('!', 1, $2); }
;
%%
#define SIZEOF_NODETYPE ((char *)&p->con - (char *)p)
nodeType *con(int value) {
nodeType *p;
size_t nodeSize;
/* allocate node */
nodeSize = SIZEOF_NODETYPE + sizeof(conNodeType);
if ((p = malloc(nodeSize)) == NULL)
yyerror("out of memory");
/* copy information */
p->type = typeCon;
p->con.value = value;
return p;
}
nodeType *id(int i) {
nodeType *p;
size_t nodeSize;
/* allocate node */
nodeSize = SIZEOF_NODETYPE + sizeof(idNodeType);
if ((p = malloc(nodeSize)) == NULL)
yyerror("out of memory");
/* copy information */
p->type = typeId;
p->id.i = i;
return p;
}
nodeType *opr(int oper, int nops, ...) {
va_list ap;
nodeType *p;
size_t nodeSize;
int i;
/* allocate node */
nodeSize = SIZEOF_NODETYPE + sizeof(oprNodeType) +
(nops - 1) * sizeof(nodeType*);
if ((p = malloc(nodeSize)) == NULL)
yyerror("out of memory");
/* copy information */
p->type = typeOpr;
p->opr.oper = oper;
p->opr.nops = nops;
va_start(ap, nops);
for (i = 0; i < nops; i++)
p->opr.op[i] = va_arg(ap, nodeType*);
va_end(ap);
return p;
}
void freeNode(nodeType *p) {
int i;
if (!p) return;
if (p->type == typeOpr) {
for (i = 0; i < p->opr.nops; i++)
freeNode(p->opr.op[i]);
}
free (p);
}
void yyerror(char *s) {
fprintf(stdout, "%s\n", s);
}
int main(void) {
yyparse();
return 0;
}