Enabling ISOP-based minimization in 'collapse' if EXDC is available.

src/base/abci/abcCollapse.c

@@ -117,6 +117,40 @@ Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk )
     DdManager * dd = (DdManager *)Abc_NtkGlobalBddMan( pNtk );
     int i;
 
+    // extract don't-care and compute ISOP
+    if ( pNtk->pExdc )
+    {
+        DdManager * ddExdc = NULL;
+        DdNode * bBddMin, * bBddDc, * bBddL, * bBddU;
+        assert( Abc_NtkIsStrash(pNtk->pExdc) );
+        assert( Abc_NtkCoNum(pNtk->pExdc) == 1 );
+        // compute the global BDDs
+        if ( Abc_NtkBuildGlobalBdds(pNtk->pExdc, 10000000, 1, 1, 0) == NULL )
+            return NULL;
+        // transfer tot the same manager
+        ddExdc = (DdManager *)Abc_NtkGlobalBddMan( pNtk->pExdc );
+        bBddDc = (DdNode *)Abc_ObjGlobalBdd(Abc_NtkCo(pNtk->pExdc, 0));
+        bBddDc = Cudd_bddTransfer( ddExdc, dd, bBddDc );  Cudd_Ref( bBddDc );
+        Abc_NtkFreeGlobalBdds( pNtk->pExdc, 1 );
+        // minimize the output
+        Abc_NtkForEachCo( pNtk, pNode, i )
+        {
+            bBddMin = (DdNode *)Abc_ObjGlobalBdd(pNode);
+            // derive lower and uppwer bound
+            bBddL = Cudd_bddAnd( dd, bBddMin,           Cudd_Not(bBddDc) );  Cudd_Ref( bBddL );
+            bBddU = Cudd_bddAnd( dd, Cudd_Not(bBddMin), Cudd_Not(bBddDc) );  Cudd_Ref( bBddU );
+            Cudd_RecursiveDeref( dd, bBddMin );
+            // compute new one
+            bBddMin = Cudd_bddIsop( dd, bBddL, Cudd_Not(bBddU) );            Cudd_Ref( bBddMin );
+            Cudd_RecursiveDeref( dd, bBddL );
+            Cudd_RecursiveDeref( dd, bBddU );
+            // update global BDD
+            Abc_ObjSetGlobalBdd( pNode, bBddMin );
+            //Extra_bddPrint( dd, bBddMin ); printf( "\n" );
+        }
+        Cudd_RecursiveDeref( dd, bBddDc );
+    }
+
 //    pReo = Extra_ReorderInit( Abc_NtkCiNum(pNtk), 1000 );
 //    runtime1 = runtime2 = 0;
 
@@ -176,7 +210,6 @@ Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode
     return pNodeNew;
 }
 
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/base/abci/abcStrash.c

@@ -293,7 +293,7 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, int fAllNodes, int fCleanup, int fR
 //        printf( "Warning: AIG cleanup removed %d nodes (this is not a bug).\n", nNodes );
     // duplicate EXDC 
     if ( pNtk->pExdc )
-        pNtkAig->pExdc = Abc_NtkDup( pNtk->pExdc );
+        pNtkAig->pExdc = Abc_NtkStrash( pNtk->pExdc, fAllNodes, fCleanup, fRecord );
     // make sure everything is okay
     if ( !Abc_NtkCheck( pNtkAig ) )
     {