1 /*========================================================================
2 Copyright (C) 1996-2002 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: /cvsroot/buddy/buddy/src/bddio.c,v 1.1.1.1 2004/06/25 13:22:14 haimcohen Exp $
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
44 static void bdd_printset_rec(FILE *, int, int *);
45 static void bdd_fprintdot_rec(FILE*, BDD);
46 static int bdd_save_rec(FILE*, int);
47 static int bdd_loaddata(FILE *);
48 static int loadhash_get(int);
49 static void loadhash_add(int, int);
50
51 static bddfilehandler filehandler;
52
53 typedef struct s_LoadHash
54 {
55 int key;
56 int data;
57 int first;
58 int next;
59 } LoadHash;
60
61 static LoadHash *lh_table;
62 static int lh_freepos;
63 static int lh_nodenum;
64 static int *loadvar2level;
65
66 /*=== PRINTING ========================================================*/
67
68
69 /*
70 NAME {* bdd\_file\_hook *}
71 SECTION {* kernel *}
72 SHORT {* Specifies a printing callback handler *}
73 PROTO {* bddfilehandler bdd_file_hook(bddfilehandler handler) *}
74 DESCR {* 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}
79 void 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. *}
92 RETURN {* The old handler *}
93 ALSO {* bdd\_printset, bdd\_strm\_hook, fdd\_file\_hook *}
94 */
bdd_file_hook(bddfilehandler handler)95 bddfilehandler bdd_file_hook(bddfilehandler handler)
96 {
97 bddfilehandler old = filehandler;
98 filehandler = handler;
99 return old;
100 }
101
102
103 /*
104 NAME {* bdd\_printall *}
105 EXTRA {* bdd\_fprintall *}
106 SECTION {* fileio *}
107 SHORT {* prints all used entries in the node table *}
108 PROTO {* void bdd_printall(void)
109 void bdd_fprintall(FILE* ofile) *}
110 DESCR {* 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. *}
117 ALSO {* bdd\_printtable, bdd\_printset, bdd\_printdot *}
118 */
bdd_printall(void)119 void bdd_printall(void)
120 {
121 bdd_fprintall(stdout);
122 }
123
124
bdd_fprintall(FILE * ofile)125 void 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 /*
148 NAME {* bdd\_printtable *}
149 EXTRA {* bdd\_fprinttable *}
150 SECTION {* fileio *}
151 SHORT {* prints the node table entries used by a BDD *}
152 PROTO {* void bdd_printtable(BDD r)
153 void bdd_fprinttable(FILE* ofile, BDD r) *}
154 DESCR {* 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. *}
161 ALSO {* bdd\_printall, bdd\_printset, bdd\_printdot *}
162 */
bdd_printtable(BDD r)163 void bdd_printtable(BDD r)
164 {
165 bdd_fprinttable(stdout, r);
166 }
167
168
bdd_fprinttable(FILE * ofile,BDD r)169 void 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 /*
203 NAME {* bdd\_printset *}
204 EXTRA {* bdd\_fprintset *}
205 SECTION {* fileio *}
206 SHORT {* prints the set of truth assignments specified by a BDD *}
207 PROTO {* bdd_printset(BDD r)
208 bdd_fprintset(FILE* ofile, BDD r) *}
209 DESCR {* 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}. *}
224 ALSO {* bdd\_printall, bdd\_printtable, bdd\_printdot, bdd\_file\_hook, bdd\_strm\_hook *}
225 */
bdd_printset(BDD r)226 void bdd_printset(BDD r)
227 {
228 bdd_fprintset(stdout, r);
229 }
230
231
bdd_fprintset(FILE * ofile,BDD r)232 void 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
bdd_printset_rec(FILE * ofile,int r,int * set)254 static 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 /*
298 NAME {* bdd\_printdot *}
299 EXTRA {* bdd\_fprintdot *}
300 SECTION {* fileio *}
301 SHORT {* prints a description of a BDD in DOT format *}
302 PROTO {* void bdd_printdot(BDD r)
303 int bdd_fnprintdot(char* fname, BDD r)
304 void bdd_fprintdot(FILE* ofile, BDD r) *}
305 DESCR {* 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. *}
310 ALSO {* bdd\_printall, bdd\_printtable, bdd\_printset *}
311 */
bdd_printdot(BDD r)312 void bdd_printdot(BDD r)
313 {
314 bdd_fprintdot(stdout, r);
315 }
316
317
bdd_fnprintdot(char * fname,BDD r)318 int 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
bdd_fprintdot(FILE * ofile,BDD r)329 void 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
bdd_fprintdot_rec(FILE * ofile,BDD r)343 static 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 /*
368 NAME {* bdd\_save *}
369 EXTRA {* bdd\_fnsave *}
370 SECTION {* fileio *}
371 SHORT {* saves a BDD to a file *}
372 PROTO {* int bdd_fnsave(char *fname, BDD r)
373 int bdd_save(FILE *ofile, BDD r) *}
374 DESCR {* 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. *}
378 ALSO {* bdd\_load *}
379 RETURN {* Zero on succes, otherwise an error code from {\tt bdd.h}. *}
380 */
bdd_fnsave(char * fname,BDD r)381 int 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
bdd_save(FILE * ofile,BDD r)395 int 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
bdd_save_rec(FILE * ofile,int root)420 static 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 /*
448 NAME {* bdd\_load *}
449 EXTRA {* bdd\_fnload *}
450 SECTION {* fileio *}
451 SHORT {* loads a BDD from a file *}
452 PROTO {* int bdd_fnload(char *fname, BDD *r)
453 int bdd_load(FILE *ifile, BDD *r) *}
454 DESCR {* 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. *}
472 ALSO {* bdd\_save *}
473 RETURN {* Zero on succes, otherwise an error code from {\tt bdd.h}. *}
474 */
bdd_fnload(char * fname,BDD * root)475 int 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
bdd_load(FILE * ifile,BDD * root)489 int 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
bdd_loaddata(FILE * ifile)540 static 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
loadhash_add(int key,int data)566 static 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
loadhash_get(int key)580 static 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