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