source: vis_dev/glu-2.3/src/calBdd/calPrint.c @ 26

Last change on this file since 26 was 13, checked in by cecile, 13 years ago

library glu 2.3
File size: 13.7 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [calPrint.c]
4
5  PackageName [cal]
6
7  Synopsis    [Routine for printing a BDD.]
8
9  Description []
10
11  SeeAlso     [None]
12
13  Author      [Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) and
14               Jagesh V. Sanghavi (sanghavi@eecs.berkeley.edu)
15               Originally written by David Long.
16               ]
17
18  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
19  All rights reserved.
20
21  Permission is hereby granted, without written agreement and without license
22  or royalty fees, to use, copy, modify, and distribute this software and its
23  documentation for any purpose, provided that the above copyright notice and
24  the following two paragraphs appear in all copies of this software.
25
26  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
27  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
28  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
29  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
30
31  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
32  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
33  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
34  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
35  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
36
37  Revision    [$Id: calPrint.c,v 1.2 1998/09/16 16:40:41 ravi Exp $]
38
39******************************************************************************/
40
41#include "calInt.h"
42
43/*---------------------------------------------------------------------------*/
44/* Constant declarations                                                     */
45/*---------------------------------------------------------------------------*/
46
47
48/*---------------------------------------------------------------------------*/
49/* Type declarations                                                         */
50/*---------------------------------------------------------------------------*/
51
52
53/*---------------------------------------------------------------------------*/
54/* Stucture declarations                                                     */
55/*---------------------------------------------------------------------------*/
56
57
58/*---------------------------------------------------------------------------*/
59/* Variable declarations                                                     */
60/*---------------------------------------------------------------------------*/
61static char defaultTerminalId[]="terminal XXXXXXXXXX XXXXXXXXXX";
62static char defaultVarName[]="var.XXXXXXXXXX";
63
64
65/*---------------------------------------------------------------------------*/
66/* Macro declarations                                                        */
67/*---------------------------------------------------------------------------*/
68
69
70/**AutomaticStart*************************************************************/
71
72/*---------------------------------------------------------------------------*/
73/* Static function prototypes                                                */
74/*---------------------------------------------------------------------------*/
75
76static void Chars(char c, int n, FILE *fp);
77static void BddPrintTopVar(Cal_BddManager_t *bddManager, Cal_Bdd_t f, Cal_VarNamingFn_t VarNamingFn, Cal_Pointer_t env, FILE *fp);
78static void BddPrintBddStep(Cal_BddManager_t *bddManager, Cal_Bdd_t f, Cal_VarNamingFn_t VarNamingFn, Cal_TerminalIdFn_t TerminalIdFn, Cal_Pointer_t env, FILE *fp, CalHashTable_t* hashTable, int indentation);
79static char * BddTerminalId(Cal_BddManager_t *bddManager, Cal_Bdd_t f, Cal_TerminalIdFn_t TerminalIdFn, Cal_Pointer_t env);
80static void BddTerminalValueAux(Cal_BddManager_t *bddManager, Cal_Bdd_t f, CalAddress_t *value1, CalAddress_t *value2);
81
82/**AutomaticEnd***************************************************************/
83
84
85/*---------------------------------------------------------------------------*/
86/* Definition of exported functions                                          */
87/*---------------------------------------------------------------------------*/
88/**Function********************************************************************
89
90  Synopsis    [Prints a BDD in the human readable form.]
91
92  Description [Prints a human-readable representation of the BDD f to
93  the file given by fp. The namingFn should be a pointer to a function
94  taking a bddManager, a BDD and the pointer given by env. This
95  function should return either a null pointer or a srting that is the
96  name of the supplied variable. If it returns a null pointer, a
97  default name is generated based on the index of the variable. It is
98  also legal for naminFN to e null; in this case, default names are
99  generated for all variables. The macro bddNamingFnNone is a null
100  pointer of suitable type. terminalIdFn should be apointer to a
101  function taking a bddManager and two longs. plus the pointer given
102  by the env. It should return either a null pointer. If it returns a
103  null pointer, or if terminalIdFn is null, then default names are
104  generated for the terminals. The macro bddTerminalIdFnNone is a null
105  pointer of suitable type.]
106
107  SideEffects [None.]
108
109******************************************************************************/
110void
111Cal_BddPrintBdd(Cal_BddManager bddManager,
112                Cal_Bdd fUserBdd, Cal_VarNamingFn_t VarNamingFn,
113                Cal_TerminalIdFn_t TerminalIdFn,
114                Cal_Pointer_t env, FILE *fp)
115{
116  long next;
117  CalHashTable_t *hashTable;
118
119  Cal_Bdd_t f = CalBddGetInternalBdd(bddManager,fUserBdd);
120  CalBddMarkSharedNodes(bddManager, f);
121  hashTable = CalHashTableOneInit(bddManager, sizeof(long));
122  next = 0;
123  CalBddNumberSharedNodes(bddManager, f, hashTable, &next);
124  BddPrintBddStep(bddManager, f, VarNamingFn, TerminalIdFn, env, fp,
125                  hashTable, 0);
126  CalHashTableOneQuit(hashTable);
127}
128
129/*---------------------------------------------------------------------------*/
130/* Definition of internal functions                                          */
131/*---------------------------------------------------------------------------*/
132/**Function********************************************************************
133
134  Synopsis    [required]
135
136  Description [optional]
137
138  SideEffects [required]
139
140  SeeAlso     [optional]
141
142******************************************************************************/
143char *
144CalBddVarName(Cal_BddManager_t *bddManager, Cal_Bdd_t v,
145           Cal_VarNamingFn_t VarNamingFn,  Cal_Pointer_t env)
146{
147  char *name;
148  if (VarNamingFn){
149    Cal_Bdd userV = CalBddGetExternalBdd(bddManager, v);
150    name = (*VarNamingFn)(bddManager, userV, env);
151    Cal_BddFree(bddManager, userV);
152  }
153 else
154   name=0;
155  if (!name){
156    sprintf(defaultVarName, "var.%d", CalBddGetBddIndex(bddManager, v));
157    name = defaultVarName;
158  }
159  return (name);
160}
161
162/**Function********************************************************************
163
164  Synopsis    [required]
165
166  Description [optional]
167
168  SideEffects [required]
169
170  SeeAlso     [optional]
171
172******************************************************************************/
173void
174CalBddNumberSharedNodes(Cal_BddManager_t *bddManager, Cal_Bdd_t f,
175                     CalHashTable_t *hashTable, long *next)
176{
177  Cal_Bdd_t thenBdd, elseBdd;
178  int mark;
179 
180  if (CalBddIsBddConst(f) || ((1 << CalBddTypeAux(bddManager, f)) &
181                           ((1 << CAL_BDD_TYPE_POSVAR) |
182                            (1 << CAL_BDD_TYPE_NEGVAR))))
183    return;
184  mark = CalBddGetMark(f);
185  if (mark == 0) return;
186  if (mark  == 2) {
187    CalHashTableOneInsert(hashTable, f, (char *)next);
188    ++*next;
189  }
190  CalBddPutMark(f, 0);
191  CalBddGetThenBdd(f, thenBdd);
192  CalBddGetElseBdd(f, elseBdd);
193  CalBddNumberSharedNodes(bddManager, thenBdd, hashTable, next);
194  CalBddNumberSharedNodes(bddManager, elseBdd, hashTable, next);
195}
196
197/**Function********************************************************************
198
199  Synopsis    [required]
200
201  Description [optional]
202
203  SideEffects [required]
204
205  SeeAlso     [optional]
206
207******************************************************************************/
208void
209CalBddMarkSharedNodes(Cal_BddManager_t *bddManager, Cal_Bdd_t f)
210{
211  int mark;
212  Cal_Bdd_t thenBdd, elseBdd;
213 
214  if (CalBddIsOutPos(f) == 0){
215    CalBddNot(f,f);
216  }
217  if (CalBddIsBddConst(f) || CalBddTypeAux(bddManager, f) ==
218      CAL_BDD_TYPE_POSVAR)
219    return; 
220  if ((mark = CalBddGetMark(f))){
221    if (mark == 1){
222      CalBddPutMark(f, 2);
223      return;
224    }
225  }
226  CalBddPutMark(f, 1);
227  CalBddGetThenBdd(f, thenBdd);
228  CalBddGetElseBdd(f, elseBdd);
229  CalBddMarkSharedNodes(bddManager, thenBdd);
230  CalBddMarkSharedNodes(bddManager, elseBdd);
231}
232
233/*---------------------------------------------------------------------------*/
234/* Definition of static functions                                            */
235/*---------------------------------------------------------------------------*/
236
237/**Function********************************************************************
238
239  Synopsis    [required]
240
241  Description [optional]
242
243  SideEffects [required]
244
245  SeeAlso     [optional]
246
247******************************************************************************/
248static void
249Chars(char c, int n,FILE *fp)
250{
251  int i;
252  for (i=0; i < n; ++i){
253    fputc(c, fp);
254  }
255}
256
257
258/**Function********************************************************************
259
260  Synopsis    [required]
261
262  Description [optional]
263
264  SideEffects [required]
265
266  SeeAlso     [optional]
267
268******************************************************************************/
269static void
270BddPrintTopVar(Cal_BddManager_t *bddManager, Cal_Bdd_t f,
271               Cal_VarNamingFn_t VarNamingFn, Cal_Pointer_t env, FILE *fp)
272{
273  Cal_Bdd_t ifVar;
274  ifVar = CalBddIf(bddManager, f);
275  fputs(CalBddVarName(bddManager, ifVar, VarNamingFn, env), fp); 
276  fputc('\n', fp);
277}
278
279
280/**Function********************************************************************
281
282  Synopsis    [required]
283
284  Description [optional]
285
286  SideEffects [required]
287
288  SeeAlso     [optional]
289
290******************************************************************************/static void
291BddPrintBddStep(Cal_BddManager_t *bddManager,
292                Cal_Bdd_t f, Cal_VarNamingFn_t VarNamingFn,
293                Cal_TerminalIdFn_t TerminalIdFn,
294                Cal_Pointer_t env, FILE *fp, CalHashTable_t* hashTable,
295                int indentation)
296{
297  int negated;
298  long *number;
299  Cal_Bdd_t fNot, thenBdd, elseBdd;
300 
301  Chars(' ', indentation, fp);
302  switch (CalBddTypeAux(bddManager, f)){
303      case CAL_BDD_TYPE_ZERO:
304      case CAL_BDD_TYPE_ONE:
305        fputs(BddTerminalId(bddManager, f, TerminalIdFn, env), fp);
306        fputc('\n', fp);
307        break;
308      case CAL_BDD_TYPE_NEGVAR:
309        fputc('!', fp);
310        /* fall through */
311      case CAL_BDD_TYPE_POSVAR:
312        BddPrintTopVar(bddManager, f, VarNamingFn, env, fp);
313        break;
314      case CAL_BDD_TYPE_NONTERMINAL:
315        CalBddNot(f, fNot);
316        if (CalHashTableOneLookup(hashTable, fNot, Cal_Nil(char *))){
317          f = fNot;
318          negated = 1;
319        }
320        else {
321          negated=0;
322        }
323        CalHashTableOneLookup(hashTable, f, (char **)&number);
324        if (number && *number < 0){
325          if (negated)
326            fputc('!', fp);
327          fprintf(fp, "subformula %d\n", (int)-*number-1);
328        }
329      else {
330        if (number){
331              fprintf(fp, "%d: ", (int) *number);
332              *number= -*number-1;
333            }
334        fputs("if ", fp);
335        BddPrintTopVar(bddManager, f, VarNamingFn, env, fp);
336        CalBddGetThenBdd(f, thenBdd);
337        BddPrintBddStep(bddManager, thenBdd, VarNamingFn,
338                        TerminalIdFn, env, fp, hashTable, indentation+2);
339        Chars(' ', indentation, fp);
340        fputs("else if !", fp);
341        BddPrintTopVar(bddManager, f, VarNamingFn, env, fp);
342        CalBddGetElseBdd(f, elseBdd);
343        BddPrintBddStep(bddManager, elseBdd, VarNamingFn,
344                        TerminalIdFn, env, fp, hashTable, indentation+2); 
345        Chars(' ', indentation, fp);
346        fputs("endif ", fp);
347        BddPrintTopVar(bddManager, f, VarNamingFn, env, fp);
348      }
349        break;
350      default:
351        CalBddFatalMessage("BddPrintBddStep: unknown type returned by Cal_BddType"); 
352  }
353}
354
355/**Function********************************************************************
356
357  Synopsis    [required]
358
359  Description [optional]
360
361  SideEffects [required]
362
363  SeeAlso     [optional]
364
365******************************************************************************/
366static char *
367BddTerminalId(Cal_BddManager_t *bddManager, Cal_Bdd_t f,
368              Cal_TerminalIdFn_t TerminalIdFn, Cal_Pointer_t env)
369{
370  char *id;
371  CalAddress_t  v1, v2;
372  BddTerminalValueAux(bddManager, f, &v1, &v2);
373  if (TerminalIdFn) id = (*TerminalIdFn)(bddManager, v1, v2, env);
374  else id=0;
375  if (!id){
376    if (CalBddIsBddOne(bddManager, f)) return ("1");
377    if (CalBddIsBddZero(bddManager, f)) return ("0");
378    sprintf(defaultTerminalId, "terminal %ld %ld", (long)v1, (long)v2);
379    id = defaultTerminalId;
380  }
381  return (id);
382}
383
384
385
386/**Function********************************************************************
387
388  Synopsis    [required]
389
390  Description [optional]
391
392  SideEffects [required]
393
394  SeeAlso     [optional]
395
396******************************************************************************/
397static void
398BddTerminalValueAux(Cal_BddManager_t *bddManager, Cal_Bdd_t f,
399                    CalAddress_t *value1, CalAddress_t *value2)
400{
401  if (CalBddIsOutPos(f)){
402    *value1 = (CalAddress_t)CalBddGetThenBddNode(f);
403    *value2 = (CalAddress_t)CalBddGetElseBddNode(f);
404  }
405  else
406    (*bddManager->TransformFn)(bddManager,
407                               (CalAddress_t)CalBddGetThenBddNode(f),
408                               (CalAddress_t)CalBddGetElseBddNode(f),
409                                value1, value2, bddManager->transformEnv); 
410}
411
412
413
414
415
416
417
418
Note: See TracBrowser for help on using the repository browser.