1 /*************************************************************************
2 FILE: parser.y
3 DESCR: BISON rules and main program for BDD calculator
4 AUTH: Jorn Lind
5 DATE: (C) may 1999
6 *************************************************************************/
7
8 %{
9 #include <string.h>
10 #include <stdarg.h>
11 #include <fstream>
12 #include <getopt.h>
13 #define IMPLEMENTSLIST /* Special for list template handling */
14 #include "slist.h"
15 #include "hashtbl.h"
16 #include "parser_.h"
17
18 using namespace std;
19
20 /* Definitions for storing and caching of identifiers */
21 #define inputTag 0
22 #define exprTag 1
23
24 struct nodeData
25 {
nodeDatanodeData26 nodeData(const nodeData &d) { tag=d.tag; name=sdup(d.name); val=d.val; }
nodeDatanodeData27 nodeData(int t, char *n, bdd v) { tag=t; name=n; val=v; }
~nodeDatanodeData28 ~nodeData(void) { delete[] name; }
29 int tag;
30 char *name;
31 bdd val;
32 };
33
34 typedef SList<nodeData> nodeLst;
35 nodeLst inputs;
36 hashTable names;
37
38 /* Other */
39 int linenum;
40
41 bddgbchandler gbcHandler = bdd_default_gbchandler;
42
43 /* Prototypes */
44 void actInit(token *nodes, token *cache);
45 void actInputs(void);
46 void actAddInput(token *id);
47 void actAssign(token *id, token *expr);
48 void actOpr2(token *res, token *left, token *right, int opr);
49 void actNot(token *res, token *right);
50 void actId(token *res, token *id);
51 void actConst(token *res, int);
52 void actSize(token *id);
53 void actDot(token *fname, token *id);
54 void actAutoreorder(token *times, token *method);
55 void actCache(void);
56 void actTautology(token *id);
57 void actExist(token *res, token *var, token *expr);
58 void actForall(token *res, token *var, token *expr);
59 void actQuantVar2(token *res, token *id, token *list);
60 void actQuantVar1(token *res, token *id);
61 void actPrint(token *id);
62
63 %}
64
65 /*************************************************************************
66 Token definitions
67 *************************************************************************/
68
69 %token T_id T_str T_intval T_true T_false
70
71 %token T_initial T_inputs T_actions
72 %token T_size T_dumpdot
73 %token T_autoreorder T_reorder T_win2 T_win2ite T_sift T_siftite T_none
74 %token T_cache T_tautology T_print
75
76 %token T_lpar T_rpar
77 %token T_equal
78 %token T_semi T_dot
79
80 %right T_exist T_forall T_dot
81 %left T_biimp
82 %left T_imp
83 %left T_or T_nor
84 %left T_xor
85 %left T_nand T_and
86 %right T_not
87
88 /*************************************************************************
89 BISON rules
90 *************************************************************************/
91 %%
92
93 /*=[ Top ]==============================================================*/
94
95 calc:
96 initial inputs actions
97 ;
98
99 /*=[ Initializers ]=====================================================*/
100
101 initial:
102 T_initial T_intval T_intval T_semi { actInit(&$2,&$3); }
103 ;
104
105 inputs:
106 T_inputs inputSeq T_semi { actInputs(); }
107 ;
108
109 inputSeq:
110 inputSeq T_id { actAddInput(&$2); }
111 | T_id { actAddInput(&$1); }
112 ;
113
114
115 /*=[ Actions ]==========================================================*/
116
117 actions:
118 T_actions actionSeq
119 ;
120
121 actionSeq:
122 actionSeq action T_semi
123 | action T_semi
124 ;
125
126 action:
127 assign
128 | size
129 | dot
130 | reorder
131 | cache
132 | tautology
133 | print
134 ;
135
136 assign:
137 T_id T_equal expr { actAssign(&$1,&$3); }
138 ;
139
140 expr:
141 expr T_and expr { actOpr2(&$$,&$1,&$3,bddop_and); }
142 | expr T_nand expr { actOpr2(&$$,&$1,&$3,bddop_nand); }
143 | expr T_xor expr { actOpr2(&$$,&$1,&$3,bddop_xor); }
144 | expr T_or expr { actOpr2(&$$,&$1,&$3,bddop_or); }
145 | expr T_nor expr { actOpr2(&$$,&$1,&$3,bddop_nor); }
146 | expr T_imp expr { actOpr2(&$$,&$1,&$3,bddop_imp); }
147 | expr T_biimp expr { actOpr2(&$$,&$1,&$3,bddop_biimp); }
148 | T_not expr { actNot(&$$,&$2); }
149 | T_lpar expr T_rpar { $$.bval = $2.bval; }
150 | T_id { actId(&$$,&$1); }
151 | T_true { $$.bval = new bdd(bddtrue); }
152 | T_false { $$.bval = new bdd(bddfalse); }
153 | quantifier { $$.bval = $1.bval; }
154 ;
155
156 quantifier:
157 T_exist varlist T_dot expr { actExist(&$$,&$2,&$4); }
158 | T_forall varlist T_dot expr { actForall(&$$,&$2,&$4); }
159 ;
160
161 varlist:
162 varlist T_id { actQuantVar2(&$$,&$2,&$1); }
163 | T_id { actQuantVar1(&$$,&$1); }
164 ;
165
166
167 size:
168 T_size T_id { actSize(&$2); }
169 ;
170
171 dot:
172 T_dumpdot T_str T_id { actDot(&$2,&$3); }
173 ;
174
175 reorder:
176 T_reorder method { bdd_reorder($2.ival); }
177 | T_autoreorder T_intval method { actAutoreorder(&$2,&$3); }
178 ;
179
180 method:
181 T_win2 { $$.ival = BDD_REORDER_WIN2; }
182 | T_win2ite { $$.ival = BDD_REORDER_WIN2ITE; }
183 | T_sift { $$.ival = BDD_REORDER_SIFT; }
184 | T_siftite { $$.ival = BDD_REORDER_SIFTITE; }
185 | T_none { $$.ival = BDD_REORDER_NONE; }
186 ;
187
188 cache:
189 T_cache { actCache(); }
190 ;
191
192 tautology:
193 T_tautology T_id { actTautology(&$2); }
194 ;
195
196 print:
197 T_print T_id { actPrint(&$2); }
198
199 %%
200 /*************************************************************************
201 Main and more
202 *************************************************************************/
203
204 void usage(void)
205 {
206 cerr << "USAGE: bddcalc [-hg] file\n";
207 cerr << " -h : print this message\n";
208 cerr << " -g : disable garbage collection info\n";
209 }
210
211
main(int ac,char ** av)212 int main(int ac, char **av)
213 {
214 int c;
215
216 while ((c=getopt(ac, av, "hg")) != EOF)
217 {
218 switch (c)
219 {
220 case 'h':
221 usage();
222 break;
223 case 'g':
224 gbcHandler = bdd_default_gbchandler;
225 break;
226 }
227 }
228
229 if (optind >= ac)
230 usage();
231
232 yyin = fopen(av[optind],"r");
233 if (!yyin)
234 {
235 cerr << "Could not open file: " << av[optind] << endl;
236 exit(2);
237 }
238
239 linenum = 1;
240 bdd_setcacheratio(2);
241 yyparse();
242
243 bdd_printstat();
244 bdd_done();
245
246 return 0;
247 }
248
249
yyerror(const char * fmt,...)250 void yyerror(const char *fmt, ...)
251 {
252 va_list argp;
253 va_start(argp,fmt);
254 fprintf(stderr, "Parse error in (or before) line %d: ", linenum);
255 vfprintf(stderr, fmt, argp);
256 va_end(argp);
257 exit(3);
258 }
259
260
261 /*************************************************************************
262 Semantic actions
263 *************************************************************************/
264
actInit(token * nodes,token * cache)265 void actInit(token *nodes, token *cache)
266 {
267 bdd_init(nodes->ival, cache->ival);
268 bdd_gbc_hook(gbcHandler);
269 bdd_reorder_verbose(0);
270 }
271
272
actInputs(void)273 void actInputs(void)
274 {
275 bdd_setvarnum(inputs.size());
276
277 int vnum=0;
278 for (nodeLst::ite i=inputs.first() ; i.more() ; i++, vnum++)
279 {
280 if (names.exists((*i).name))
281 yyerror("Redefinition of input %s", (*i).name);
282
283 (*i).val = bdd_ithvar(vnum);
284 hashData hd((*i).name, 0, &(*i));
285 names.add(hd);
286 }
287
288 bdd_varblockall();
289 }
290
291
actAddInput(token * id)292 void actAddInput(token *id)
293 {
294 inputs.append( nodeData(inputTag,sdup(id->id),bddtrue) );
295 }
296
297
actAssign(token * id,token * expr)298 void actAssign(token *id, token *expr)
299 {
300 if (names.exists(id->id))
301 yyerror("Redefinition of %s", id->id);
302
303 nodeData *d = new nodeData(exprTag, sdup(id->id), *expr->bval);
304 hashData hd(d->name, 0, d);
305 names.add(hd);
306 delete expr->bval;
307 }
308
309
actOpr2(token * res,token * left,token * right,int opr)310 void actOpr2(token *res, token *left, token *right, int opr)
311 {
312 res->bval = new bdd( bdd_apply(*left->bval, *right->bval, opr) );
313 delete left->bval;
314 delete right->bval;
315 }
316
317
actNot(token * res,token * right)318 void actNot(token *res, token *right)
319 {
320 res->bval = new bdd( bdd_not(*right->bval) );
321 delete right->bval;
322 //printf("%5d -> %f\n", fixme, bdd_satcount(*res->bval));
323 }
324
325
actId(token * res,token * id)326 void actId(token *res, token *id)
327 {
328 hashData hd;
329
330 if (names.lookup(id->id,hd) == 0)
331 {
332 res->bval = new bdd( ((nodeData*)hd.def)->val );
333 }
334 else
335 yyerror("Unknown variable %s", id->id);
336 }
337
338
actExist(token * res,token * var,token * expr)339 void actExist(token *res, token *var, token *expr)
340 {
341 res->bval = new bdd( bdd_exist(*expr->bval, *var->bval) );
342 delete var->bval;
343 delete expr->bval;
344 }
345
346
actForall(token * res,token * var,token * expr)347 void actForall(token *res, token *var, token *expr)
348 {
349 res->bval = new bdd( bdd_forall(*expr->bval, *var->bval) );
350 delete var->bval;
351 delete expr->bval;
352 }
353
354
actQuantVar2(token * res,token * id,token * list)355 void actQuantVar2(token *res, token *id, token *list)
356 {
357 hashData hd;
358
359 if (names.lookup(id->id,hd) == 0)
360 {
361 if (hd.type == inputTag)
362 {
363 res->bval = list->bval;
364 *res->bval &= ((nodeData*)hd.def)->val;
365 }
366 else
367 yyerror("%s is not a variable", id->id);
368 }
369 else
370 yyerror("Unknown variable %s", id->id);
371 }
372
373
actQuantVar1(token * res,token * id)374 void actQuantVar1(token *res, token *id)
375 {
376 hashData hd;
377
378 if (names.lookup(id->id,hd) == 0)
379 {
380 if (hd.type == inputTag)
381 res->bval = new bdd( ((nodeData*)hd.def)->val );
382 else
383 yyerror("%s is not a variable", id->id);
384 }
385 else
386 yyerror("Unknown variable %s", id->id);
387 }
388
389
actSize(token * id)390 void actSize(token *id)
391 {
392 hashData hd;
393
394 if (names.lookup(id->id,hd) == 0)
395 {
396 cout << "Number of nodes used for " << id->id << " = "
397 << bdd_nodecount(((nodeData*)hd.def)->val) << endl;
398 }
399 else
400 yyerror("Unknown variable %s", id->id);
401 }
402
403
actDot(token * fname,token * id)404 void actDot(token *fname, token *id)
405 {
406 hashData hd;
407
408 if (names.lookup(id->id,hd) == 0)
409 {
410 if (bdd_fnprintdot(fname->str, ((nodeData*)hd.def)->val) < 0)
411 cout << "Could not open file: " << fname->str << endl;
412 }
413 else
414 yyerror("Unknown variable %s", id->id);
415 }
416
417
actAutoreorder(token * times,token * method)418 void actAutoreorder(token *times, token *method)
419 {
420 if (times->ival == 0)
421 bdd_autoreorder(method->ival);
422 else
423 bdd_autoreorder_times(method->ival, times->ival);
424 }
425
426
actCache(void)427 void actCache(void)
428 {
429 bdd_printstat();
430 }
431
432
actTautology(token * id)433 void actTautology(token *id)
434 {
435 hashData hd;
436
437 if (names.lookup(id->id,hd) == 0)
438 {
439 if (((nodeData*)hd.def)->val == bddtrue)
440 cout << "Formula " << id->id << " is a tautology!\n";
441 else
442 cout << "Formula " << id->id << " is NOT a tautology!\n";
443 }
444 else
445 yyerror("Unknown variable %s", id->id);
446 }
447
448
actPrint(token * id)449 void actPrint(token *id)
450 {
451 hashData hd;
452
453 if (names.lookup(id->id,hd) == 0)
454 cout << id->id << " = " << bddset << ((nodeData*)hd.def)->val << endl;
455 else
456 yyerror("Unknown variable %s", id->id);
457 }
458
459 /* EOF */
460