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