Version abc50807

5 files changed, 57 insertions, 17 deletions

diff --git a/src/bdd/dsd/dsd.h b/src/bdd/dsd/dsd.h
index 60cf4a4e..5396bacd 100644
--- a/src/bdd/dsd/dsd.h
+++ b/src/bdd/dsd/dsd.h
@@ -88,6 +88,7 @@ extern Dsd_Node_t *    Dsd_NodeReadDec ( Dsd_Node_t * p, int i );
 extern int             Dsd_NodeReadDecsNum( Dsd_Node_t * p );
 extern int             Dsd_NodeReadMark( Dsd_Node_t * p );
 extern void            Dsd_NodeSetMark( Dsd_Node_t * p, int Mark ); 
+extern DdManager *     Dsd_ManagerReadDd( Dsd_Manager_t * pMan );
 extern Dsd_Node_t *    Dsd_ManagerReadRoot( Dsd_Manager_t * pMan, int i );
 extern Dsd_Node_t *    Dsd_ManagerReadInput( Dsd_Manager_t * pMan, int i );
 /*=== dsdMan.c =======================================================*/
@@ -95,6 +96,7 @@ extern Dsd_Manager_t * Dsd_ManagerStart( DdManager * dd, int nSuppMax, int fVerb
 extern void            Dsd_ManagerStop( Dsd_Manager_t * dMan );
 /*=== dsdProc.c =======================================================*/
 extern void            Dsd_Decompose( Dsd_Manager_t * dMan, DdNode ** pbFuncs, int nFuncs );
+extern Dsd_Node_t *    Dsd_DecomposeOne( Dsd_Manager_t * pDsdMan, DdNode * bFunc );
 /*=== dsdTree.c =======================================================*/
 extern void            Dsd_TreeNodeGetInfo( Dsd_Manager_t * dMan, int * DepthMax, int * GateSizeMax );
 extern void            Dsd_TreeNodeGetInfoOne( Dsd_Node_t * pNode, int * DepthMax, int * GateSizeMax );
@@ -104,6 +106,7 @@ extern int             Dsd_TreeCountPrimeNodes( Dsd_Manager_t * pDsdMan );
 extern int             Dsd_TreeCountPrimeNodesOne( Dsd_Node_t * pRoot );
 extern int             Dsd_TreeCollectDecomposableVars( Dsd_Manager_t * dMan, int * pVars );
 extern Dsd_Node_t **   Dsd_TreeCollectNodesDfs( Dsd_Manager_t * dMan, int * pnNodes );
+extern Dsd_Node_t **   Dsd_TreeCollectNodesDfsOne( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pNode, int * pnNodes );
 extern void            Dsd_TreePrint( FILE * pFile, Dsd_Manager_t * dMan, char * pInputNames[], char * pOutputNames[], int fShortNames, int Output );
 /*=== dsdLocal.c =======================================================*/
 extern DdNode *        Dsd_TreeGetPrimeFunction( DdManager * dd, Dsd_Node_t * pNode );
diff --git a/src/bdd/dsd/dsdApi.c b/src/bdd/dsd/dsdApi.c
index f2269092..daf3080f 100644
--- a/src/bdd/dsd/dsdApi.c
+++ b/src/bdd/dsd/dsdApi.c
@@ -89,6 +89,7 @@ void          Dsd_NodeSetMark( Dsd_Node_t * p, int Mark ){ p->Mark = Mark;     }
 ***********************************************************************/
 Dsd_Node_t *  Dsd_ManagerReadRoot( Dsd_Manager_t * pMan, int i )  { return pMan->pRoots[i];  } 
 Dsd_Node_t *  Dsd_ManagerReadInput( Dsd_Manager_t * pMan, int i ) { return pMan->pInputs[i]; } 
+DdManager *   Dsd_ManagerReadDd( Dsd_Manager_t * pMan )           { return pMan->dd;         } 
 
 ////////////////////////////////////////////////////////////////////////
 ///                           END OF FILE                            ///
diff --git a/src/bdd/dsd/dsdInt.h b/src/bdd/dsd/dsdInt.h
index 81440460..5008c24e 100644
--- a/src/bdd/dsd/dsdInt.h
+++ b/src/bdd/dsd/dsdInt.h
@@ -61,6 +61,8 @@ struct Dsd_Node_t_
 ///                       MACRO DEFITIONS                            ///
 ////////////////////////////////////////////////////////////////////////
 
+#define MAXINPUTS 1000
+
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/bdd/dsd/dsdProc.c b/src/bdd/dsd/dsdProc.c
index 38cdc2b8..08c029e1 100644
--- a/src/bdd/dsd/dsdProc.c
+++ b/src/bdd/dsd/dsdProc.c
@@ -225,6 +225,22 @@ s_Loops2Useless = 0;
 
 /**Function*************************************************************
 
+  Synopsis    [Performs decomposition for one function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dsd_Node_t * Dsd_DecomposeOne( Dsd_Manager_t * pDsdMan, DdNode * bFunc )
+{
+    return dsdKernelDecompose_rec( pDsdMan, bFunc );
+}
+
+/**Function*************************************************************
+
   Synopsis    [The main function of this module. Recursive implementation of DSD.]
 
   Description []
@@ -1053,7 +1069,7 @@ if ( s_Show )
                     // go through the decomposition list of pPrev and find components 
                     // whose support does not overlap with supp(Lower) 
 
-                    Dsd_Node_t ** pNonOverlap = ALLOC( Dsd_Node_t *, dd->size );
+                    static Dsd_Node_t * pNonOverlap[MAXINPUTS];
                     int i, nNonOverlap = 0;
                     for ( i = 0; i < pPrev->nDecs; i++ )
                     {
@@ -1089,7 +1105,6 @@ if ( s_Show )
                         // assign the support to be subtracted from both components
                         bSuppSubract = pDENew->S;
                     }
-                    free( pNonOverlap );
                 }
                 
                 // subtract its support from the support of upper component
@@ -1106,8 +1121,8 @@ if ( s_Show )
             } // end of if ( !fEqualLevel )
             else // if ( fEqualLevel ) -- they have the same top level var
             {
-                Dsd_Node_t ** pMarkedLeft = ALLOC( Dsd_Node_t *, dd->size ); // the pointers to the marked blocks
-                char * pMarkedPols = ALLOC( char, dd->size );                // polarities of the marked blocks
+                static Dsd_Node_t * pMarkedLeft[MAXINPUTS]; // the pointers to the marked blocks
+                static char pMarkedPols[MAXINPUTS]; // polarities of the marked blocks
                 int nMarkedLeft = 0;
 
                 int fPolarity = 0;
@@ -1198,9 +1213,6 @@ if ( s_Show )
                 SuppH = Cudd_bddExistAbstract( dd, bTemp = SuppH, bSuppSubract ), Cudd_Ref( SuppH );
                 Cudd_RecursiveDeref(dd, bTemp);
 
-                free( pMarkedLeft );
-                free( pMarkedPols );
-
             } // end of if ( fEqualLevel ) 
 
         } // end of decomposition list comparison
@@ -1333,7 +1345,7 @@ Dsd_Node_t * dsdKernelFindContainingComponent( Dsd_Manager_t * pDsdMan, Dsd_Node
 ***********************************************************************/
 int dsdKernelFindCommonComponents( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pL, Dsd_Node_t * pH, Dsd_Node_t *** pCommon, Dsd_Node_t ** pLastDiffL, Dsd_Node_t ** pLastDiffH )
 {
-    Dsd_Node_t ** Common = ALLOC( Dsd_Node_t *, pDsdMan->dd->size );
+    static Dsd_Node_t * Common[MAXINPUTS];
     int nCommon = 0;
 
     // pointers to the current decomposition entries
@@ -1402,7 +1414,6 @@ int dsdKernelFindCommonComponents( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pL, Dsd
     // return the pointer to the array
     *pCommon = Common;
     // return the number of common components
-    free( Common );
     return nCommon;            
 }
 
@@ -1567,7 +1578,7 @@ int dsdKernelVerifyDecomposition( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pDE )
     else if ( pR->Type == DSD_NODE_PRIME )
     {
         int i;
-        DdNode ** bGVars = ALLOC( DdNode *, dd->size );
+        static DdNode * bGVars[MAXINPUTS];
         // transform the function of this block, so that it depended on inputs
         // corresponding to the formal inputs
         DdNode * bNewFunc = Dsd_TreeGetPrimeFunctionOld( dd, pR, 1 );  Cudd_Ref( bNewFunc );
@@ -1589,7 +1600,6 @@ int dsdKernelVerifyDecomposition( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pDE )
         RetValue = (int)( bRes == pR->G );//|| bRes == Cudd_Not(pR->G) );
         /////////////////////////////////////////////////////////
         Cudd_Deref( bRes );
-        free( bGVars );
     }
     else
     {
diff --git a/src/bdd/dsd/dsdTree.c b/src/bdd/dsd/dsdTree.c
index b1532715..7905cbdd 100644
--- a/src/bdd/dsd/dsdTree.c
+++ b/src/bdd/dsd/dsdTree.c
@@ -517,6 +517,33 @@ Dsd_Node_t ** Dsd_TreeCollectNodesDfs( Dsd_Manager_t * pDsdMan, int * pnNodes )
     return ppNodes;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Creates the DFS ordered array of DSD nodes in the tree.]
+
+  Description [The collected nodes do not include the terminal nodes
+  and the constant 1 node. The array of nodes is returned. The number
+  of entries in the array is returned in the variale pnNodes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dsd_Node_t ** Dsd_TreeCollectNodesDfsOne( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pNode, int * pnNodes )
+{
+    Dsd_Node_t ** ppNodes;
+    int nNodes, nNodesAlloc;
+    nNodesAlloc = Dsd_TreeCountNonTerminalNodesOne(pNode);
+    nNodes  = 0;
+    ppNodes = ALLOC( Dsd_Node_t *, nNodesAlloc );
+    Dsd_TreeCollectNodesDfs_rec( Dsd_Regular(pNode), ppNodes, &nNodes );
+    Dsd_TreeUnmark_rec(Dsd_Regular(pNode));
+    assert( nNodesAlloc == nNodes );
+    *pnNodes = nNodes;
+    return ppNodes;
+}
+
 
 /**Function*************************************************************
 
@@ -777,9 +804,7 @@ DdNode * Dsd_TreeGetPrimeFunctionOld( DdManager * dd, Dsd_Node_t * pNode, int fR
     DdNode * bCof0,  * bCof1, * bCube0, * bCube1, * bNewFunc, * bTemp;
     int i;
     int fAllBuffs = 1;
-    int * pPermute;
-
-    pPermute = ALLOC( int, dd->size );
+    static int Permute[MAXINPUTS];
 
     assert( pNode );
     assert( !Dsd_IsComplement( pNode ) );
@@ -821,14 +846,13 @@ DdNode * Dsd_TreeGetPrimeFunctionOld( DdManager * dd, Dsd_Node_t * pNode, int fR
         // remap the function to the first variables of the manager
         for ( i = 0; i < pNode->nDecs; i++ )
     //        Permute[ pNode->pDecs[i]->S->index ] = dd->invperm[i];
-            pPermute[ pNode->pDecs[i]->S->index ] = i;
+            Permute[ pNode->pDecs[i]->S->index ] = i;
 
-        bNewFunc = Cudd_bddPermute( dd, bTemp = bNewFunc, pPermute );   Cudd_Ref( bNewFunc );
+        bNewFunc = Cudd_bddPermute( dd, bTemp = bNewFunc, Permute );   Cudd_Ref( bNewFunc );
         Cudd_RecursiveDeref( dd, bTemp );
     }
 
     Cudd_Deref( bNewFunc );
-    free( pPermute );
     return bNewFunc;
 }