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