src/calBdd/calPrint.c File Reference

#include "calInt.h"
Include dependency graph for calPrint.c:

Go to the source code of this file.

Functions

static void Chars (char c, int n, FILE *fp)
static void BddPrintTopVar (Cal_BddManager_t *bddManager, Cal_Bdd_t f, Cal_VarNamingFn_t VarNamingFn, Cal_Pointer_t env, FILE *fp)
static 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)
static char * BddTerminalId (Cal_BddManager_t *bddManager, Cal_Bdd_t f, Cal_TerminalIdFn_t TerminalIdFn, Cal_Pointer_t env)
static void BddTerminalValueAux (Cal_BddManager_t *bddManager, Cal_Bdd_t f, CalAddress_t *value1, CalAddress_t *value2)
void Cal_BddPrintBdd (Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_VarNamingFn_t VarNamingFn, Cal_TerminalIdFn_t TerminalIdFn, Cal_Pointer_t env, FILE *fp)
char * CalBddVarName (Cal_BddManager_t *bddManager, Cal_Bdd_t v, Cal_VarNamingFn_t VarNamingFn, Cal_Pointer_t env)
void CalBddNumberSharedNodes (Cal_BddManager_t *bddManager, Cal_Bdd_t f, CalHashTable_t *hashTable, long *next)
void CalBddMarkSharedNodes (Cal_BddManager_t *bddManager, Cal_Bdd_t f)

Variables

static char defaultTerminalId [] = "terminal XXXXXXXXXX XXXXXXXXXX"
static char defaultVarName [] = "var.XXXXXXXXXX"

Function Documentation

static 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 
) [static]

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 291 of file calPrint.c.

00296 {
00297   int negated;
00298   long *number;
00299   Cal_Bdd_t fNot, thenBdd, elseBdd;
00300   
00301   Chars(' ', indentation, fp);
00302   switch (CalBddTypeAux(bddManager, f)){
00303       case CAL_BDD_TYPE_ZERO:
00304       case CAL_BDD_TYPE_ONE:
00305         fputs(BddTerminalId(bddManager, f, TerminalIdFn, env), fp);
00306         fputc('\n', fp);
00307         break;
00308       case CAL_BDD_TYPE_NEGVAR:
00309         fputc('!', fp);
00310         /* fall through */
00311       case CAL_BDD_TYPE_POSVAR:
00312         BddPrintTopVar(bddManager, f, VarNamingFn, env, fp);
00313         break;
00314       case CAL_BDD_TYPE_NONTERMINAL:
00315         CalBddNot(f, fNot);
00316         if (CalHashTableOneLookup(hashTable, fNot, Cal_Nil(char *))){
00317           f = fNot;
00318           negated = 1;
00319         }
00320         else {
00321           negated=0;
00322         }
00323         CalHashTableOneLookup(hashTable, f, (char **)&number);
00324         if (number && *number < 0){
00325           if (negated)
00326             fputc('!', fp);
00327           fprintf(fp, "subformula %d\n", (int)-*number-1);
00328         }
00329       else {
00330         if (number){
00331               fprintf(fp, "%d: ", (int) *number);
00332               *number= -*number-1;
00333             }
00334         fputs("if ", fp);
00335         BddPrintTopVar(bddManager, f, VarNamingFn, env, fp);
00336         CalBddGetThenBdd(f, thenBdd);
00337         BddPrintBddStep(bddManager, thenBdd, VarNamingFn,
00338                         TerminalIdFn, env, fp, hashTable, indentation+2);
00339         Chars(' ', indentation, fp);
00340         fputs("else if !", fp);
00341         BddPrintTopVar(bddManager, f, VarNamingFn, env, fp);
00342         CalBddGetElseBdd(f, elseBdd);
00343         BddPrintBddStep(bddManager, elseBdd, VarNamingFn,
00344                         TerminalIdFn, env, fp, hashTable, indentation+2); 
00345         Chars(' ', indentation, fp);
00346         fputs("endif ", fp);
00347         BddPrintTopVar(bddManager, f, VarNamingFn, env, fp);
00348       }
00349         break;
00350       default:
00351         CalBddFatalMessage("BddPrintBddStep: unknown type returned by Cal_BddType"); 
00352   }
00353 }

static void BddPrintTopVar ( Cal_BddManager_t *  bddManager,
Cal_Bdd_t  f,
Cal_VarNamingFn_t  VarNamingFn,
Cal_Pointer_t  env,
FILE *  fp 
) [static]

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 270 of file calPrint.c.

00272 {
00273   Cal_Bdd_t ifVar;
00274   ifVar = CalBddIf(bddManager, f);
00275   fputs(CalBddVarName(bddManager, ifVar, VarNamingFn, env), fp);  
00276   fputc('\n', fp);
00277 }

static char * BddTerminalId ( Cal_BddManager_t *  bddManager,
Cal_Bdd_t  f,
Cal_TerminalIdFn_t  TerminalIdFn,
Cal_Pointer_t  env 
) [static]

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 367 of file calPrint.c.

00369 {
00370   char *id;
00371   CalAddress_t  v1, v2;
00372   BddTerminalValueAux(bddManager, f, &v1, &v2);
00373   if (TerminalIdFn) id = (*TerminalIdFn)(bddManager, v1, v2, env);
00374   else id=0;
00375   if (!id){
00376     if (CalBddIsBddOne(bddManager, f)) return ("1");
00377     if (CalBddIsBddZero(bddManager, f)) return ("0");
00378     sprintf(defaultTerminalId, "terminal %ld %ld", (long)v1, (long)v2);
00379     id = defaultTerminalId;
00380   }
00381   return (id);
00382 }

static void BddTerminalValueAux ( Cal_BddManager_t *  bddManager,
Cal_Bdd_t  f,
CalAddress_t *  value1,
CalAddress_t *  value2 
) [static]

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 398 of file calPrint.c.

00400 {
00401   if (CalBddIsOutPos(f)){
00402     *value1 = (CalAddress_t)CalBddGetThenBddNode(f);
00403     *value2 = (CalAddress_t)CalBddGetElseBddNode(f);
00404   }
00405   else
00406     (*bddManager->TransformFn)(bddManager,
00407                                (CalAddress_t)CalBddGetThenBddNode(f),
00408                                (CalAddress_t)CalBddGetElseBddNode(f),
00409                                 value1, value2, bddManager->transformEnv);  
00410 }

void Cal_BddPrintBdd ( Cal_BddManager  bddManager,
Cal_Bdd  fUserBdd,
Cal_VarNamingFn_t  VarNamingFn,
Cal_TerminalIdFn_t  TerminalIdFn,
Cal_Pointer_t  env,
FILE *  fp 
)

AutomaticEnd Function********************************************************************

Synopsis [Prints a BDD in the human readable form.]

Description [Prints a human-readable representation of the BDD f to the file given by fp. The namingFn should be a pointer to a function taking a bddManager, a BDD and the pointer given by env. This function should return either a null pointer or a srting that is the name of the supplied variable. If it returns a null pointer, a default name is generated based on the index of the variable. It is also legal for naminFN to e null; in this case, default names are generated for all variables. The macro bddNamingFnNone is a null pointer of suitable type. terminalIdFn should be apointer to a function taking a bddManager and two longs. plus the pointer given by the env. It should return either a null pointer. If it returns a null pointer, or if terminalIdFn is null, then default names are generated for the terminals. The macro bddTerminalIdFnNone is a null pointer of suitable type.]

SideEffects [None.]

Definition at line 111 of file calPrint.c.

00115 {
00116   long next;
00117   CalHashTable_t *hashTable;
00118 
00119   Cal_Bdd_t f = CalBddGetInternalBdd(bddManager,fUserBdd);
00120   CalBddMarkSharedNodes(bddManager, f);
00121   hashTable = CalHashTableOneInit(bddManager, sizeof(long));
00122   next = 0;
00123   CalBddNumberSharedNodes(bddManager, f, hashTable, &next);
00124   BddPrintBddStep(bddManager, f, VarNamingFn, TerminalIdFn, env, fp,
00125                   hashTable, 0);
00126   CalHashTableOneQuit(hashTable);
00127 }

void CalBddMarkSharedNodes ( Cal_BddManager_t *  bddManager,
Cal_Bdd_t  f 
)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 209 of file calPrint.c.

00210 {
00211   int mark;
00212   Cal_Bdd_t thenBdd, elseBdd;
00213   
00214   if (CalBddIsOutPos(f) == 0){
00215     CalBddNot(f,f);
00216   }
00217   if (CalBddIsBddConst(f) || CalBddTypeAux(bddManager, f) ==
00218       CAL_BDD_TYPE_POSVAR)
00219     return; 
00220   if ((mark = CalBddGetMark(f))){
00221     if (mark == 1){
00222       CalBddPutMark(f, 2);
00223       return;
00224     }
00225   }
00226   CalBddPutMark(f, 1);
00227   CalBddGetThenBdd(f, thenBdd);
00228   CalBddGetElseBdd(f, elseBdd);
00229   CalBddMarkSharedNodes(bddManager, thenBdd);
00230   CalBddMarkSharedNodes(bddManager, elseBdd);
00231 }

void CalBddNumberSharedNodes ( Cal_BddManager_t *  bddManager,
Cal_Bdd_t  f,
CalHashTable_t *  hashTable,
long *  next 
)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 174 of file calPrint.c.

00176 {
00177   Cal_Bdd_t thenBdd, elseBdd;
00178   int mark;
00179   
00180   if (CalBddIsBddConst(f) || ((1 << CalBddTypeAux(bddManager, f)) &
00181                            ((1 << CAL_BDD_TYPE_POSVAR) |
00182                             (1 << CAL_BDD_TYPE_NEGVAR))))
00183     return;
00184   mark = CalBddGetMark(f);
00185   if (mark == 0) return;
00186   if (mark  == 2) {
00187     CalHashTableOneInsert(hashTable, f, (char *)next);
00188     ++*next;
00189   }
00190   CalBddPutMark(f, 0);
00191   CalBddGetThenBdd(f, thenBdd);
00192   CalBddGetElseBdd(f, elseBdd);
00193   CalBddNumberSharedNodes(bddManager, thenBdd, hashTable, next);
00194   CalBddNumberSharedNodes(bddManager, elseBdd, hashTable, next);
00195 }

char* CalBddVarName ( Cal_BddManager_t *  bddManager,
Cal_Bdd_t  v,
Cal_VarNamingFn_t  VarNamingFn,
Cal_Pointer_t  env 
)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 144 of file calPrint.c.

00146 {
00147   char *name;
00148   if (VarNamingFn){
00149     Cal_Bdd userV = CalBddGetExternalBdd(bddManager, v);
00150     name = (*VarNamingFn)(bddManager, userV, env);
00151     Cal_BddFree(bddManager, userV);
00152   }
00153  else
00154    name=0;
00155   if (!name){
00156     sprintf(defaultVarName, "var.%d", CalBddGetBddIndex(bddManager, v));
00157     name = defaultVarName;
00158   }
00159   return (name);
00160 }

static void Chars ( char  c,
int  n,
FILE *  fp 
) [static]

AutomaticStart

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 249 of file calPrint.c.

00250 {
00251   int i;
00252   for (i=0; i < n; ++i){
00253     fputc(c, fp);
00254   }
00255 }

Variable Documentation

char defaultTerminalId[] = "terminal XXXXXXXXXX XXXXXXXXXX" [static]

CFile***********************************************************************

FileName [calPrint.c]

PackageName [cal]

Synopsis [Routine for printing a BDD.]

Description []

SeeAlso [None]

Author [Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) and Jagesh V. Sanghavi (sanghavi@eecs.berkeley.edu) Originally written by David Long. ]

Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California. All rights reserved.

Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.

IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]

Revision [

Id
calPrint.c,v 1.2 1998/09/16 16:40:41 ravi Exp

]

Definition at line 61 of file calPrint.c.

char defaultVarName[] = "var.XXXXXXXXXX" [static]

Definition at line 62 of file calPrint.c.

Generated on Tue Jan 12 13:57:12 2010 for glu-2.2 by  doxygen 1.6.1