text: /**CFile****************************************************************
  
    FileName    [dsdInt.h]
  
    PackageName [DSD: Disjoint-support decomposition package.]
  
    Synopsis    [Internal declarations of the package.]
  
    Author      [Alan Mishchenko]
    
    Affiliation [UC Berkeley]
  
    Date        [Ver. 8.0. Started - September 22, 2003.]
  
    Revision    [$Id: dsdInt.h,v 1.0 2002/22/09 00:00:00 alanmi Exp $]
  
  ***********************************************************************/
  
  #ifndef __DSD_INT_H__
  #define __DSD_INT_H__
  
  #include "extra.h"
  #include "dsd.h"
  
  ////////////////////////////////////////////////////////////////////////
  ///                      TYPEDEF DEFINITIONS                         ///
  ////////////////////////////////////////////////////////////////////////
   
  typedef unsigned char byte;
  
  ////////////////////////////////////////////////////////////////////////
  ///                    STRUCTURE DEFINITIONS                         ///
  ////////////////////////////////////////////////////////////////////////
  
  // DSD manager
  struct Dsd_Manager_t_ 
  {
  	DdManager *    dd;         // the BDD manager
  	st_table *     Table;      // the mapping of BDDs into their DEs
  	int            nInputs;    // the number of primary inputs
  	int            nRoots;     // the number of primary outputs
  	int            nRootsAlloc;// the number of primary outputs
  	Dsd_Node_t **  pInputs;    // the primary input nodes
  	Dsd_Node_t **  pRoots;     // the primary output nodes
      Dsd_Node_t *   pConst1;    // the constant node
  	int            fVerbose;   // the verbosity level 
  };
  
  // DSD node
  struct Dsd_Node_t_
  {
  	Dsd_Type_t     Type;       // decomposition type
  	DdNode *       G;          // function of the node	 
  	DdNode *       S;          // support of this function
  	Dsd_Node_t **  pDecs;      // pointer to structures for formal inputs
  	int            Mark;       // the mark used by CASE 4 of disjoint decomposition
  	short          nDecs;      // the number of formal inputs
  	short          nVisits;    // the counter of visits
  };
  
  ////////////////////////////////////////////////////////////////////////
  ///                       MACRO DEFINITIONS                          ///
  ////////////////////////////////////////////////////////////////////////
  
  #define MAXINPUTS 1000
  
  ////////////////////////////////////////////////////////////////////////
  ///                         PARAMETERS                               ///
  ////////////////////////////////////////////////////////////////////////
  
  ////////////////////////////////////////////////////////////////////////
  ///                     FUNCTION DECLARATIONS                        ///
  ////////////////////////////////////////////////////////////////////////
  
  /*=== dsdCheck.c =======================================================*/
  extern void         Dsd_CheckCacheAllocate( int nEntries );
  extern void         Dsd_CheckCacheDeallocate();
  extern void         Dsd_CheckCacheClear();
  extern int          Dsd_CheckRootFunctionIdentity( DdManager * dd, DdNode * bF1, DdNode * bF2, DdNode * bC1, DdNode * bC2 );
  /*=== dsdTree.c =======================================================*/
  extern Dsd_Node_t * Dsd_TreeNodeCreate( int Type, int nDecs, int BlockNum );
  extern void         Dsd_TreeNodeDelete( DdManager * dd, Dsd_Node_t * pNode );
  extern void         Dsd_TreeUnmark( Dsd_Manager_t * dMan );
  extern DdNode *     Dsd_TreeGetPrimeFunctionOld( DdManager * dd, Dsd_Node_t * pNode, int fRemap );
  
  #endif
  
  ////////////////////////////////////////////////////////////////////////
  ///                           END OF FILE                            ///
  ////////////////////////////////////////////////////////////////////////
  
  