Version abc80420

3 files changed, 151 insertions, 2 deletions

diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
index 4f00cbda..fc9d21bc 100644
--- a/src/aig/ntl/ntl.h
+++ b/src/aig/ntl/ntl.h
@@ -120,6 +120,7 @@ struct Ntl_Net_t_
 {
     Ntl_Net_t *        pNext;          // next net in the hash table
     void *             pCopy;          // the copy of this object
+    void *             pCopy2;         // the copy of this object
     Ntl_Obj_t *        pDriver;        // driver of the net
     char               nVisits;        // the number of times the net is visited
     char               fMark;          // temporary mark
diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c
index 18ca1a53..5a681a7e 100644
--- a/src/aig/ntl/ntlExtract.c
+++ b/src/aig/ntl/ntlExtract.c
@@ -233,7 +233,10 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p )
     pRoot = Ntl_ManRootModel( p );
     // clear net visited flags
     Ntl_ModelForEachNet( pRoot, pNet, i )
+    {
         pNet->nVisits = 0;
+        pNet->pCopy = NULL;
+    }
     // collect primary inputs
     Ntl_ModelForEachPi( pRoot, pObj, i )
     {
@@ -417,7 +420,10 @@ Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p )
     pRoot = Ntl_ManRootModel( p );
     // clear net visited flags
     Ntl_ModelForEachNet( pRoot, pNet, i )
+    {
         pNet->nVisits = 0;
+        pNet->pCopy = NULL;
+    }
     // collect primary inputs
     Ntl_ModelForEachPi( pRoot, pObj, i )
     {
@@ -486,9 +492,17 @@ Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p )
 Aig_Man_t * Ntl_ManCollapseForCec( Ntl_Man_t * p )
 {
     Aig_Man_t * pAig;
+    Ntl_Mod_t * pRoot;
     Ntl_Obj_t * pObj;
     Ntl_Net_t * pNet;
     int i;
+    // clear net visited flags
+    pRoot = Ntl_ManRootModel(p);
+    Ntl_ModelForEachNet( pRoot, pNet, i )
+    {
+        pNet->nVisits = 0;
+        pNet->pCopy = NULL;
+    }
     // create the manager
     p->pAig = Aig_ManStart( 10000 );
     p->pAig->pName = Aig_UtilStrsav( p->pName );
@@ -557,6 +571,13 @@ Aig_Man_t * Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 )
     Aig_ObjCreatePo( pAig, Aig_ManConst1(pAig) );
 
     /////////////////////////////////////////////////////
+    // clear net visited flags
+    pRoot1 = Ntl_ManRootModel(p1);
+    Ntl_ModelForEachNet( pRoot1, pNet, i )
+    {
+        pNet->nVisits = 0;
+        pNet->pCopy = NULL;
+    }
     // primary inputs
     Ntl_ManForEachCiNet( p1, pObj, i )
     {
@@ -571,7 +592,6 @@ Aig_Man_t * Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 )
         pNet->nVisits = 2;
     }
     // latch outputs
-    pRoot1 = Ntl_ManRootModel(p1);
     Ntl_ModelForEachLatch( pRoot1, pObj, i )
     {
         assert( Ntl_ObjFanoutNum(pObj) == 1 );
@@ -614,6 +634,13 @@ Aig_Man_t * Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 )
     }
 
     /////////////////////////////////////////////////////
+    // clear net visited flags
+    pRoot2 = Ntl_ManRootModel(p2);
+    Ntl_ModelForEachNet( pRoot2, pNet, i )
+    {
+        pNet->nVisits = 0;
+        pNet->pCopy = NULL;
+    }
     // primary inputs
     Ntl_ManForEachCiNet( p2, pObj, i )
     {
@@ -628,7 +655,6 @@ Aig_Man_t * Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 )
         pNet->nVisits = 2;
     }
     // latch outputs
-    pRoot2 = Ntl_ManRootModel(p2);
     Ntl_ModelForEachLatch( pRoot2, pObj, i )
     {
         assert( Ntl_ObjFanoutNum(pObj) == 1 );
diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c
index 63725558..86d92b3c 100644
--- a/src/aig/ntl/ntlFraig.c
+++ b/src/aig/ntl/ntlFraig.c
@@ -369,6 +369,128 @@ Ntl_Man_t * Ntl_ManSsw( Ntl_Man_t * p, Fra_Ssw_t * pPars )
 }
 
 
+
+
+/**Function*************************************************************
+
+  Synopsis    [Transfers the copy field into the second copy field.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManTransferCopy( Ntl_Man_t * p )
+{
+    Ntl_Net_t * pNet;
+    Ntl_Mod_t * pRoot;
+    int i;
+    pRoot = Ntl_ManRootModel( p );
+    Ntl_ModelForEachNet( pRoot, pNet, i )
+    {
+        pNet->pCopy2 = pNet->pCopy;
+        pNet->pCopy = NULL;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reattaches one white-box.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManAttachWhiteBox( Ntl_Man_t * p, Aig_Man_t * pAigCol, Aig_Man_t * pAigRed, Ntl_Man_t * pNew, Ntl_Obj_t * pBox )
+{
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reattaches white-boxes after reducing the netlist.]
+
+  Description [The following parameters are given:
+  Original netlist (p) whose nets point to the nodes of collapsed AIG.
+  Collapsed AIG (pAigCol) whose objects point to those of reduced AIG.
+  Reduced AIG (pAigRed) whose objects point to the nets of the new netlist.
+  The new netlist is changed by this procedure to have those white-boxes
+  from the original AIG (p) those outputs are preserved after reduction.
+  Note that if outputs are preserved, the inputs are also preserved.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManAttachWhiteBoxes( Ntl_Man_t * p, Aig_Man_t * pAigCol, Aig_Man_t * pAigRed, Ntl_Man_t * pNew, int fVerbose )
+{
+    Ntl_Mod_t * pRoot;
+    Ntl_Obj_t * pBox;
+    Ntl_Net_t * pNet;
+    int i, k, Counter = 0;
+    // go through the white-boxes and check if they are preserved
+    pRoot = Ntl_ManRootModel( p );
+    Ntl_ModelForEachBox( pRoot, pBox, i )
+    {
+        Ntl_ObjForEachFanout( pBox, pNet, k )
+        {
+            // skip dangling outputs of the box
+            if ( pNet->pCopy == NULL )
+                continue;
+            // skip the outputs that are not preserved after merging equivalence
+            if ( Aig_Regular(pNet->pCopy2)->pData == NULL )
+                continue;
+            break;
+        }
+        if ( k == Ntl_ObjFanoutNum(pBox) )
+            continue;
+        // the box is preserved
+        Ntl_ManAttachWhiteBox( p, pAigCol, pAigRed, pNew, pBox );
+        Counter++;
+    }
+    if ( fVerbose )
+        printf( "Attached %d boxed (out of %d).\n", Counter, Ntl_ModelBoxNum(pRoot) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns AIG with WB after sequential SAT sweeping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ntl_Man_t * Ntl_ManSsw2( Ntl_Man_t * p, Fra_Ssw_t * pPars )
+{
+    Ntl_Man_t * pNew;
+    Aig_Man_t * pAigRed, * pAigCol;
+    // collapse the AIG
+    pAigCol = Ntl_ManCollapse( p );
+    pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p));
+    // transform the collapsed AIG
+    pAigRed = Fra_FraigInduction( pAigCol, pPars );
+    Aig_ManStop( pAigRed );
+    pAigRed = Aig_ManDupReprBasic( pAigCol );
+    // insert the result back
+    Ntl_ManTransferCopy( p );
+    pNew = Ntl_ManInsertAig( p, pAigRed );
+    // attach the white-boxes
+    Ntl_ManAttachWhiteBoxes( p, pAigCol, pAigRed, pNew, pPars->fVerbose );
+    Ntl_ManSweep( pNew, pPars->fVerbose );
+    // cleanup
+    Aig_ManStop( pAigRed );
+    Aig_ManStop( pAigCol );
+    return pNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////