1/*======================================================================== 2 Copyright (C) 1996-2001 by Jorn Lind-Nielsen 3 All rights reserved 4 5 Permission is hereby granted, without written agreement and without 6 license or royalty fees, to use, reproduce, prepare derivative 7 works, distribute, and display this software and its documentation 8 for any purpose, provided that (1) the above copyright notice and 9 the following two paragraphs appear in all copies of the source code 10 and (2) redistributions, including without limitation binaries, 11 reproduce these notices in the supporting documentation. Substantial 12 modifications to this software may be copyrighted by their authors 13 and need not follow the licensing terms described here, provided 14 that the new terms are clearly indicated in all files where they apply. 15 16 IN NO EVENT SHALL JORN LIND-NIELSEN, OR DISTRIBUTORS OF THIS 17 SOFTWARE BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, 18 INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS 19 SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE AUTHORS OR ANY OF THE 20 ABOVE PARTIES HAVE BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. 21 22 JORN LIND-NIELSEN SPECIFICALLY DISCLAIM ANY WARRANTIES, INCLUDING, 23 BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND 24 FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS 25 ON AN "AS IS" BASIS, AND THE AUTHORS AND DISTRIBUTORS HAVE NO 26 OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR 27 MODIFICATIONS. 28========================================================================*/ 29 30/************************************************************************* 31 $Header$ 32 FILE: bddio.c 33 DESCR: File I/O routines for BDD package 34 AUTH: Jorn Lind 35 DATE: (C) june 1997 36*************************************************************************/ 37#include <string.h> 38#include <stdlib.h> 39#include <fcntl.h> 40#include <assert.h> 41#include <sys/stat.h> 42#include "kernel.h" 43 44static void bdd_printset_rec(FILE *, int, int *); 45static void bdd_fprintdot_rec(FILE*, BDD); 46static int bdd_save_rec(FILE*, int); 47static int bdd_loaddata(FILE *); 48static int loadhash_get(int); 49static void loadhash_add(int, int); 50 51static bddfilehandler filehandler; 52 53typedef struct s_LoadHash 54{ 55 int key; 56 int data; 57 int first; 58 int next; 59} LoadHash; 60 61static LoadHash *lh_table; 62static int lh_freepos; 63static int lh_nodenum; 64static int *loadvar2level; 65 66/*=== PRINTING ========================================================*/ 67 68 69/* 70NAME {* bdd\_file\_hook *} 71SECTION {* kernel *} 72SHORT {* Specifies a printing callback handler *} 73PROTO {* bddfilehandler bdd_file_hook(bddfilehandler handler) *} 74DESCR {* A printing callback handler for use with BDDs is used to 75 convert the BDD variable number into something readable by the 76 end user. Typically the handler will print a string name 77 instead of the number. A handler could look like this: 78 \begin{verbatim} 79void printhandler(FILE *o, int var) 80{ 81 extern char **names; 82 fprintf(o, "%s", names[var]); 83} 84\end{verbatim} 85 86 \noindent 87 The handler can then be passed to BuDDy like this: 88 {\tt bdd\_file\_hook(printhandler)}. 89 90 No default handler is supplied. The argument {\tt handler} may be 91 NULL if no handler is needed. *} 92RETURN {* The old handler *} 93ALSO {* bdd\_printset, bdd\_strm\_hook, fdd\_file\_hook *} 94*/ 95bddfilehandler bdd_file_hook(bddfilehandler handler) 96{ 97 bddfilehandler old = filehandler; 98 filehandler = handler; 99 return old; 100} 101 102 103/* 104NAME {* bdd\_printall *} 105EXTRA {* bdd\_fprintall *} 106SECTION {* fileio *} 107SHORT {* prints all used entries in the node table *} 108PROTO {* void bdd_printall(void) 109void bdd_fprintall(FILE* ofile) *} 110DESCR {* Prints to either stdout or the file {\tt ofile} all the used 111 entries in the main node table. The format is: 112 \begin{Ill} 113 {\tt [Nodenum] Var/level Low High} 114 \end{Ill} 115 Where {\tt Nodenum} is the position in the node table and level 116 is the position in the current variable order. *} 117ALSO {* bdd\_printtable, bdd\_printset, bdd\_printdot *} 118*/ 119void bdd_printall(void) 120{ 121 bdd_fprintall(stdout); 122} 123 124 125void bdd_fprintall(FILE *ofile) 126{ 127 int n; 128 129 for (n=0 ; n<bddnodesize ; n++) 130 { 131 if (LOW(n) != -1) 132 { 133 fprintf(ofile, "[%5d - %2d] ", n, bddnodes[n].refcou); 134 if (filehandler) 135 filehandler(ofile, bddlevel2var[LEVEL(n)]); 136 else 137 fprintf(ofile, "%3d", bddlevel2var[LEVEL(n)]); 138 139 fprintf(ofile, ": %3d", LOW(n)); 140 fprintf(ofile, " %3d", HIGH(n)); 141 fprintf(ofile, "\n"); 142 } 143 } 144} 145 146 147/* 148NAME {* bdd\_printtable *} 149EXTRA {* bdd\_fprinttable *} 150SECTION {* fileio *} 151SHORT {* prints the node table entries used by a BDD *} 152PROTO {* void bdd_printtable(BDD r) 153void bdd_fprinttable(FILE* ofile, BDD r) *} 154DESCR {* Prints to either stdout or the file {\tt ofile} all the entries 155 in the main node table used by {\tt r}. The format is: 156 \begin{Ill} 157 {\tt [Nodenum] Var/level : Low High} 158 \end{Ill} 159 Where {\tt Nodenum} is the position in the node table and level 160 is the position in the current variable order. *} 161ALSO {* bdd\_printall, bdd\_printset, bdd\_printdot *} 162*/ 163void bdd_printtable(BDD r) 164{ 165 bdd_fprinttable(stdout, r); 166} 167 168 169void bdd_fprinttable(FILE *ofile, BDD r) 170{ 171 BddNode *node; 172 int n; 173 174 fprintf(ofile, "ROOT: %d\n", r); 175 if (r < 2) 176 return; 177 178 bdd_mark(r); 179 180 for (n=0 ; n<bddnodesize ; n++) 181 { 182 if (LEVEL(n) & MARKON) 183 { 184 node = &bddnodes[n]; 185 186 LEVELp(node) &= MARKOFF; 187 188 fprintf(ofile, "[%5d] ", n); 189 if (filehandler) 190 filehandler(ofile, bddlevel2var[LEVELp(node)]); 191 else 192 fprintf(ofile, "%3d", bddlevel2var[LEVELp(node)]); 193 194 fprintf(ofile, ": %3d", LOWp(node)); 195 fprintf(ofile, " %3d", HIGHp(node)); 196 fprintf(ofile, "\n"); 197 } 198 } 199} 200 201 202/* 203NAME {* bdd\_printset *} 204EXTRA {* bdd\_fprintset *} 205SECTION {* fileio *} 206SHORT {* prints the set of truth assignments specified by a BDD *} 207PROTO {* bdd_printset(BDD r) 208bdd_fprintset(FILE* ofile, BDD r) *} 209DESCR {* Prints all the truth assignments for {\tt r} that would yield 210 it true. The format is: 211 \begin{Ill} 212 {\tt < $x_{1,1}:c_{1,1},\ldots,x_{1,n_1}:c_{1,n_1}$ >\\ 213 < $x_{2,1}:c_{2,1},\ldots,x_{2,n_2}:c_{2,n_2}$ >\\ 214 $\ldots$ \\ 215 < $x_{N,1}:c_{N,1},\ldots,x_{N,n_3}:c_{N,n_3}$ > } 216 \end{Ill} 217 Where the $x$'s are variable numbers (and the position in the 218 current order) and the $c$'s are the 219 possible assignments to these. Each set of brackets designates 220 one possible assignment to the set of variables that make up the 221 BDD. All variables not shown are don't cares. It is possible to 222 specify a callback handler for printing of the variables using 223 {\tt bdd\_file\_hook} or {\tt bdd\_strm\_hook}. *} 224ALSO {* bdd\_printall, bdd\_printtable, bdd\_printdot, bdd\_file\_hook, bdd\_strm\_hook *} 225*/ 226void bdd_printset(BDD r) 227{ 228 bdd_fprintset(stdout, r); 229} 230 231 232void bdd_fprintset(FILE *ofile, BDD r) 233{ 234 int *set; 235 236 if (r < 2) 237 { 238 fprintf(ofile, "%s", r == 0 ? "F" : "T"); 239 return; 240 } 241 242 if ((set=(int *)malloc(sizeof(int)*bddvarnum)) == NULL) 243 { 244 bdd_error(BDD_MEMORY); 245 return; 246 } 247 248 memset(set, 0, sizeof(int) * bddvarnum); 249 bdd_printset_rec(ofile, r, set); 250 free(set); 251} 252 253 254static void bdd_printset_rec(FILE *ofile, int r, int *set) 255{ 256 int n; 257 int first; 258 259 if (r == 0) 260 return; 261 else 262 if (r == 1) 263 { 264 fprintf(ofile, "<"); 265 first = 1; 266 267 for (n=0 ; n<bddvarnum ; n++) 268 { 269 if (set[n] > 0) 270 { 271 if (!first) 272 fprintf(ofile, ", "); 273 first = 0; 274 if (filehandler) 275 filehandler(ofile, bddlevel2var[n]); 276 else 277 fprintf(ofile, "%d", bddlevel2var[n]); 278 fprintf(ofile, ":%d", (set[n]==2 ? 1 : 0)); 279 } 280 } 281 282 fprintf(ofile, ">"); 283 } 284 else 285 { 286 set[LEVEL(r)] = 1; 287 bdd_printset_rec(ofile, LOW(r), set); 288 289 set[LEVEL(r)] = 2; 290 bdd_printset_rec(ofile, HIGH(r), set); 291 292 set[LEVEL(r)] = 0; 293 } 294} 295 296 297/* 298NAME {* bdd\_printdot *} 299EXTRA {* bdd\_fprintdot *} 300SECTION {* fileio *} 301SHORT {* prints a description of a BDD in DOT format *} 302PROTO {* void bdd_printdot(BDD r) 303int bdd_fnprintdot(char* fname, BDD r) 304void bdd_fprintdot(FILE* ofile, BDD r) *} 305DESCR {* Prints a BDD in a format suitable for use with the graph 306 drawing program DOT to either stdout, a designated file 307 {\tt ofile} or the file named by {\tt fname}. In the last case 308 the file will be opened for writing, any previous contents 309 destroyed and then closed again. *} 310ALSO {* bdd\_printall, bdd\_printtable, bdd\_printset *} 311*/ 312void bdd_printdot(BDD r) 313{ 314 bdd_fprintdot(stdout, r); 315} 316 317 318int bdd_fnprintdot(char *fname, BDD r) 319{ 320 FILE *ofile = fopen(fname, "w"); 321 if (ofile == NULL) 322 return bdd_error(BDD_FILE); 323 bdd_fprintdot(ofile, r); 324 fclose(ofile); 325 return 0; 326} 327 328 329void bdd_fprintdot(FILE* ofile, BDD r) 330{ 331 fprintf(ofile, "digraph G {\n"); 332 fprintf(ofile, "0 [shape=box, label=\"0\", style=filled, shape=box, height=0.3, width=0.3];\n"); 333 fprintf(ofile, "1 [shape=box, label=\"1\", style=filled, shape=box, height=0.3, width=0.3];\n"); 334 335 bdd_fprintdot_rec(ofile, r); 336 337 fprintf(ofile, "}\n"); 338 339 bdd_unmark(r); 340} 341 342 343static void bdd_fprintdot_rec(FILE* ofile, BDD r) 344{ 345 if (ISCONST(r) || MARKED(r)) 346 return; 347 348 fprintf(ofile, "%d [label=\"", r); 349 if (filehandler) 350 filehandler(ofile, bddlevel2var[LEVEL(r)]); 351 else 352 fprintf(ofile, "%d", bddlevel2var[LEVEL(r)]); 353 fprintf(ofile, "\"];\n"); 354 355 fprintf(ofile, "%d -> %d [style=dotted];\n", r, LOW(r)); 356 fprintf(ofile, "%d -> %d [style=filled];\n", r, HIGH(r)); 357 358 SETMARK(r); 359 360 bdd_fprintdot_rec(ofile, LOW(r)); 361 bdd_fprintdot_rec(ofile, HIGH(r)); 362} 363 364 365/*=== SAVE =============================================================*/ 366 367/* 368NAME {* bdd\_save *} 369EXTRA {* bdd\_fnsave *} 370SECTION {* fileio *} 371SHORT {* saves a BDD to a file *} 372PROTO {* int bdd_fnsave(char *fname, BDD r) 373int bdd_save(FILE *ofile, BDD r) *} 374DESCR {* Saves the nodes used by {\tt r} to either a file {\tt ofile} 375 which must be opened for writing or to the file named {\tt fname}. 376 In the last case the file will be truncated and opened for 377 writing. *} 378ALSO {* bdd\_load *} 379RETURN {* Zero on succes, otherwise an error code from {\tt bdd.h}. *} 380*/ 381int bdd_fnsave(char *fname, BDD r) 382{ 383 FILE *ofile; 384 int ok; 385 386 if ((ofile=fopen(fname,"w")) == NULL) 387 return bdd_error(BDD_FILE); 388 389 ok = bdd_save(ofile, r); 390 fclose(ofile); 391 return ok; 392} 393 394 395int bdd_save(FILE *ofile, BDD r) 396{ 397 int err, n=0; 398 399 if (r < 2) 400 { 401 fprintf(ofile, "0 0 %d\n", r); 402 return 0; 403 } 404 405 bdd_markcount(r, &n); 406 bdd_unmark(r); 407 fprintf(ofile, "%d %d\n", n, bddvarnum); 408 409 for (n=0 ; n<bddvarnum ; n++) 410 fprintf(ofile, "%d ", bddvar2level[n]); 411 fprintf(ofile, "\n"); 412 413 err = bdd_save_rec(ofile, r); 414 bdd_unmark(r); 415 416 return err; 417} 418 419 420static int bdd_save_rec(FILE *ofile, int root) 421{ 422 BddNode *node = &bddnodes[root]; 423 int err; 424 425 if (root < 2) 426 return 0; 427 428 if (LEVELp(node) & MARKON) 429 return 0; 430 LEVELp(node) |= MARKON; 431 432 if ((err=bdd_save_rec(ofile, LOWp(node))) < 0) 433 return err; 434 if ((err=bdd_save_rec(ofile, HIGHp(node))) < 0) 435 return err; 436 437 fprintf(ofile, "%d %d %d %d\n", 438 root, bddlevel2var[LEVELp(node) & MARKHIDE], 439 LOWp(node), HIGHp(node)); 440 441 return 0; 442} 443 444 445/*=== LOAD =============================================================*/ 446 447/* 448NAME {* bdd\_load *} 449EXTRA {* bdd\_fnload *} 450SECTION {* fileio *} 451SHORT {* loads a BDD from a file *} 452PROTO {* int bdd_fnload(char *fname, BDD *r) 453int bdd_load(FILE *ifile, BDD *r) *} 454DESCR {* Loads a BDD from a file into the BDD pointed to by {\tt r}. 455 The file can either be the file {\tt ifile} which must be opened 456 for reading or the file named {\tt fname} which will be opened 457 automatically for reading. 458 459 The input file format consists of integers arranged in the following 460 manner. First the number of nodes $N$ used by the BDD and then the 461 number of variables $V$ allocated and the variable ordering 462 in use at the time the BDD was saved. 463 If $N$ and $V$ are both zero then the BDD is either the constant 464 true or false BDD, indicated by a $1$ or a $0$ as the next integer. 465 466 In any other case the next $N$ sets of $4$ integers will describe 467 the nodes used by the BDD. Each set consists of first the node 468 number, then the variable number and then the low and high nodes. 469 470 The nodes {\it must} be saved in a order such that any low or 471 high node must be defined before it is mentioned. *} 472ALSO {* bdd\_save *} 473RETURN {* Zero on succes, otherwise an error code from {\tt bdd.h}. *} 474*/ 475int bdd_fnload(char *fname, BDD *root) 476{ 477 FILE *ifile; 478 int ok; 479 480 if ((ifile=fopen(fname,"r")) == NULL) 481 return bdd_error(BDD_FILE); 482 483 ok = bdd_load(ifile, root); 484 fclose(ifile); 485 return ok; 486} 487 488 489int bdd_load(FILE *ifile, BDD *root) 490{ 491 int n, vnum, tmproot; 492 493 if (fscanf(ifile, "%d %d", &lh_nodenum, &vnum) != 2) 494 return bdd_error(BDD_FORMAT); 495 496 /* Check for constant true / false */ 497 if (lh_nodenum==0 && vnum==0) 498 { 499 fscanf(ifile, "%d", root); 500 return 0; 501 } 502 503 if ((loadvar2level=(int*)malloc(sizeof(int)*vnum)) == NULL) 504 return bdd_error(BDD_MEMORY); 505 for (n=0 ; n<vnum ; n++) 506 fscanf(ifile, "%d", &loadvar2level[n]); 507 508 if (vnum > bddvarnum) 509 bdd_setvarnum(vnum); 510 511 if ((lh_table=(LoadHash*)malloc(lh_nodenum*sizeof(LoadHash))) == NULL) 512 return bdd_error(BDD_MEMORY); 513 514 for (n=0 ; n<lh_nodenum ; n++) 515 { 516 lh_table[n].first = -1; 517 lh_table[n].next = n+1; 518 } 519 lh_table[lh_nodenum-1].next = -1; 520 lh_freepos = 0; 521 522 tmproot = bdd_loaddata(ifile); 523 524 for (n=0 ; n<lh_nodenum ; n++) 525 bdd_delref(lh_table[n].data); 526 527 free(lh_table); 528 free(loadvar2level); 529 530 *root = 0; 531 if (tmproot < 0) 532 return tmproot; 533 else 534 *root = tmproot; 535 536 return 0; 537} 538 539 540static int bdd_loaddata(FILE *ifile) 541{ 542 int key,var,low,high,root=0,n; 543 544 for (n=0 ; n<lh_nodenum ; n++) 545 { 546 if (fscanf(ifile,"%d %d %d %d", &key, &var, &low, &high) != 4) 547 return bdd_error(BDD_FORMAT); 548 549 if (low >= 2) 550 low = loadhash_get(low); 551 if (high >= 2) 552 high = loadhash_get(high); 553 554 if (low<0 || high<0 || var<0) 555 return bdd_error(BDD_FORMAT); 556 557 root = bdd_addref( bdd_ite(bdd_ithvar(var), high, low) ); 558 559 loadhash_add(key, root); 560 } 561 562 return root; 563} 564 565 566static void loadhash_add(int key, int data) 567{ 568 int hash = key % lh_nodenum; 569 int pos = lh_freepos; 570 571 lh_freepos = lh_table[pos].next; 572 lh_table[pos].next = lh_table[hash].first; 573 lh_table[hash].first = pos; 574 575 lh_table[pos].key = key; 576 lh_table[pos].data = data; 577} 578 579 580static int loadhash_get(int key) 581{ 582 int hash = lh_table[key % lh_nodenum].first; 583 584 while (hash != -1 && lh_table[hash].key != key) 585 hash = lh_table[hash].next; 586 587 if (hash == -1) 588 return -1; 589 return lh_table[hash].data; 590} 591 592 593/* EOF */ 594