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