Version abc80209

8 files changed, 96 insertions, 24 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index cd810b5e..1124c2fb 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -517,7 +517,8 @@ extern void            Aig_ObjOrderInsert( Aig_Man_t * p, int ObjId );
 extern void            Aig_ObjOrderRemove( Aig_Man_t * p, int ObjId );
 extern void            Aig_ObjOrderAdvance( Aig_Man_t * p );
 /*=== aigPart.c =========================================================*/
-extern Vec_Ptr_t *     Aig_ManSupports( Aig_Man_t * pMan );
+extern Vec_Ptr_t *     Aig_ManSupports( Aig_Man_t * p );
+extern Vec_Ptr_t *     Aig_ManSupportsInverse( Aig_Man_t * p );
 extern Vec_Ptr_t *     Aig_ManPartitionSmart( Aig_Man_t * p, int nPartSizeLimit, int fVerbose, Vec_Ptr_t ** pvPartSupps );
 extern Vec_Ptr_t *     Aig_ManPartitionNaive( Aig_Man_t * p, int nPartSize );
 extern Vec_Ptr_t *     Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSize );
diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c
index e2100b57..edf51a2e 100644
--- a/src/aig/aig/aigPart.c
+++ b/src/aig/aig/aigPart.c
@@ -258,7 +258,7 @@ Vec_Int_t * Part_ManTransferEntry( Part_One_t * p )
   Synopsis    [Computes supports of the POs in the multi-output AIG.]
 
   Description [Returns the array of integer arrays containing indices
-  of the primary inputs.]
+  of the primary inputsf or each primary output.]
                
   SideEffects [Adds the integer PO number at end of each array.]
 
@@ -346,6 +346,40 @@ Vec_Ptr_t * Aig_ManSupports( Aig_Man_t * pMan )
 
 /**Function*************************************************************
 
+  Synopsis    [Computes the set of outputs for each input.]
+
+  Description [Returns the array of integer arrays containing indices
+  of the primary outputsf for each primary input.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Aig_ManSupportsInverse( Aig_Man_t * p )
+{
+    Vec_Ptr_t * vSupps, * vSuppsInv;
+    Vec_Int_t * vSupp;
+    int i, k, iIn, iOut;
+    // get structural supports for each output
+    vSupps = Aig_ManSupports( p );
+    // start the inverse supports
+    vSuppsInv = Vec_PtrAlloc( Aig_ManPiNum(p) );
+    for ( i = 0; i < Aig_ManPiNum(p); i++ )
+        Vec_PtrPush( vSuppsInv, Vec_IntAlloc(8) );
+    // transforms the supports into the inverse supports
+    Vec_PtrForEachEntry( vSupps, vSupp, i )
+    {
+        iOut = Vec_IntPop( vSupp );
+        Vec_IntForEachEntry( vSupp, iIn, k )
+            Vec_IntPush( Vec_PtrEntry(vSuppsInv, iIn), iOut );
+    }
+    Vec_VecFree( (Vec_Vec_t *)vSupps );
+    return vSuppsInv;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Start char-bases support representation.]
 
   Description []
diff --git a/src/aig/fra/fraClaus.c b/src/aig/fra/fraClaus.c
index 8e3a03e1..d95515d5 100644
--- a/src/aig/fra/fraClaus.c
+++ b/src/aig/fra/fraClaus.c
@@ -515,7 +515,7 @@ int Fra_ClausCollectLatchClauses( Clu_Man_t * p, Fra_Sml_t * pSeq )
 
     nCountConst = nCountImps = 0;
     CostMax = p->nSimWords * 32;
-
+/*
     // add the property
     {
         Aig_Obj_t * pObj;
@@ -528,7 +528,7 @@ int Fra_ClausCollectLatchClauses( Clu_Man_t * p, Fra_Sml_t * pSeq )
         nCountConst++;
 //        printf( "Added the target property to the set of clauses to be inductively checked.\n" );
     }
-
+*/
 
     pSeq->nWordsPref = p->nSimWordsPref;
     Aig_ManForEachLoSeq( p->pAig, pObj1, i )
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 72606dcf..d703cfc4 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -95,8 +95,8 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters )
     if ( fRegisters )
     {
         pMan->nRegs = Abc_NtkLatchNum(pNtk);
-//        pMan->vFlopNums = Vec_IntStartNatural( pMan->nRegs );
-        pMan->vFlopNums = NULL;
+        pMan->vFlopNums = Vec_IntStartNatural( pMan->nRegs );
+//        pMan->vFlopNums = NULL;
     }
     // transfer the pointers to the basic nodes
     Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan);
@@ -154,6 +154,7 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
     Abc_Obj_t * pObjNew;
     Aig_Obj_t * pObj;
     int i;
+    assert( pMan->nAsserts == 0 );
 //    assert( Aig_ManRegNum(pMan) == Abc_NtkLatchNum(pNtkOld) );
     // perform strashing
     pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
@@ -203,11 +204,12 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
 {
-    Vec_Ptr_t * vNodes;
+    Vec_Ptr_t * vNodes; 
     Abc_Ntk_t * pNtkNew;
     Abc_Obj_t * pObjNew, * pLatch;
     Aig_Obj_t * pObj, * pObjLo, * pObjLi;
-    int i, iNodeId;
+    int i, iNodeId, nDigits; 
+    assert( pMan->nAsserts == 0 );
 //    assert( Aig_ManRegNum(pMan) != Abc_NtkLatchNum(pNtkOld) );
     // perform strashing
     pNtkNew = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
@@ -237,19 +239,6 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
         Abc_ObjAddFanin( pObjLo->pData, pObjNew );
         Abc_LatchSetInit0( pObjNew );
     }
-    if ( pMan->vFlopNums == NULL )
-        Abc_NtkAddDummyBoxNames( pNtkNew );
-    else
-    {
-        assert( Abc_NtkBoxNum(pNtkOld) == Abc_NtkLatchNum(pNtkOld) );
-        Abc_NtkForEachLatch( pNtkNew, pObjNew, i )
-        {
-            pLatch = Abc_NtkBox( pNtkOld, Vec_IntEntry( pMan->vFlopNums, i ) );
-            Abc_ObjAssignName( pObjNew, Abc_ObjName(pLatch), NULL );
-            Abc_ObjAssignName( Abc_ObjFanin0(pObjNew),  Abc_ObjName(Abc_ObjFanin0(pLatch)), NULL );
-            Abc_ObjAssignName( Abc_ObjFanout0(pObjNew), Abc_ObjName(Abc_ObjFanout0(pLatch)), NULL );
-        }
-    }
     // rebuild the AIG
     vNodes = Aig_ManDfs( pMan );
     Vec_PtrForEachEntry( vNodes, pObj, i )
@@ -261,8 +250,8 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
     // connect the PO nodes
     Aig_ManForEachPo( pMan, pObj, i )
     {
-        if ( pMan->nAsserts && i == Aig_ManPoNum(pMan) - pMan->nAsserts )
-            break;
+//        if ( pMan->nAsserts && i == Aig_ManPoNum(pMan) - pMan->nAsserts )
+//            break;
         iNodeId = Nm_ManFindIdByNameTwoTypes( pNtkNew->pManName, Abc_ObjName(Abc_NtkCo(pNtkNew, i)), ABC_OBJ_PI, ABC_OBJ_BO );
         if ( iNodeId >= 0 )
             pObjNew = Abc_NtkObj( pNtkNew, iNodeId );
@@ -270,6 +259,29 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
             pObjNew = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
         Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), pObjNew );
     }
+    if ( pMan->vFlopNums == NULL )
+        Abc_NtkAddDummyBoxNames( pNtkNew );
+    else
+    {
+        assert( Abc_NtkBoxNum(pNtkOld) == Abc_NtkLatchNum(pNtkOld) );
+        nDigits = Extra_Base10Log( Abc_NtkLatchNum(pNtkNew) );
+        Abc_NtkForEachLatch( pNtkNew, pObjNew, i )
+        {
+            pLatch = Abc_NtkBox( pNtkOld, Vec_IntEntry( pMan->vFlopNums, i ) );
+            iNodeId = Nm_ManFindIdByName( pNtkNew->pManName, Abc_ObjName(Abc_ObjFanout0(pLatch)), ABC_OBJ_PO );
+            if ( iNodeId >= 0 )
+            {
+                Abc_ObjAssignName( pObjNew, Abc_ObjNameDummy("l", i, nDigits), NULL );
+                Abc_ObjAssignName( Abc_ObjFanin0(pObjNew), Abc_ObjNameDummy("li", i, nDigits), NULL );
+                Abc_ObjAssignName( Abc_ObjFanout0(pObjNew), Abc_ObjNameDummy("lo", i, nDigits), NULL );
+//printf( "happening   %s -> %s\n", Abc_ObjName(Abc_ObjFanin0(pObjNew)), Abc_ObjName(Abc_ObjFanout0(pObjNew)) );
+                continue;
+            }
+            Abc_ObjAssignName( pObjNew, Abc_ObjName(pLatch), NULL );
+            Abc_ObjAssignName( Abc_ObjFanin0(pObjNew),  Abc_ObjName(Abc_ObjFanin0(pLatch)), NULL );
+            Abc_ObjAssignName( Abc_ObjFanout0(pObjNew), Abc_ObjName(Abc_ObjFanout0(pLatch)), NULL );
+        }
+    }
     // if there are assertions, add them
     if ( pMan->nAsserts > 0 )
         Aig_ManForEachAssert( pMan, pObj, i )
diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c
index aed0abe5..082b35d4 100644
--- a/src/opt/mfs/mfsCore.c
+++ b/src/opt/mfs/mfsCore.c
@@ -175,6 +175,7 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
         pTemp = Abc_NtkStrash( pNtk->pExcare, 0, 0, 0 );
         p->pCare = Abc_NtkToDar( pTemp, 0 );
         Abc_NtkDelete( pTemp );
+        p->vSuppsInv = Aig_ManSupportsInverse( p->pCare );
     }
 //    if ( pPars->fVerbose )
     {
diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h
index ddd16407..e51e0bba 100644
--- a/src/opt/mfs/mfsInt.h
+++ b/src/opt/mfs/mfsInt.h
@@ -49,6 +49,7 @@ struct Mfs_Man_t_
     Mfs_Par_t *         pPars;
     Abc_Ntk_t *         pNtk;
     Aig_Man_t *         pCare;
+    Vec_Ptr_t *         vSuppsInv;
     int                 nFaninMax;
     // intermeditate data for the node
     Vec_Ptr_t *         vRoots;    // the roots of the window
diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c
index 519b855d..768e5295 100644
--- a/src/opt/mfs/mfsMan.c
+++ b/src/opt/mfs/mfsMan.c
@@ -155,6 +155,8 @@ void Mfs_ManStop( Mfs_Man_t * p )
         Mfs_ManPrint( p );
     if ( p->pCare )
         Aig_ManStop( p->pCare );
+    if ( p->vSuppsInv )
+        Vec_VecFree( (Vec_Vec_t *)p->vSuppsInv );
     Mfs_ManClean( p );
     Int_ManFree( p->pMan );
     Vec_IntFree( p->vMem );
diff --git a/src/opt/mfs/mfsStrash.c b/src/opt/mfs/mfsStrash.c
index 8e945045..a3475752 100644
--- a/src/opt/mfs/mfsStrash.c
+++ b/src/opt/mfs/mfsStrash.c
@@ -179,7 +179,8 @@ Aig_Man_t * Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode )
     Aig_Man_t * pMan;
     Abc_Obj_t * pFanin;
     Aig_Obj_t * pObjAig, * pPi, * pPo;
-    int i;
+    Vec_Int_t * vOuts;
+    int i, k, iOut;
     // start the new manager
     pMan = Aig_ManStart( 1000 );
     // construct the root node's AIG cone
@@ -197,6 +198,25 @@ Aig_Man_t * Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode )
             pPi->pData = pFanin->pCopy;
         }
         // construct the constraints
+        Vec_PtrForEachEntry( p->vSupp, pFanin, i )
+        {
+            vOuts = Vec_PtrEntry( p->vSuppsInv, (int)pFanin->pData );
+            Vec_IntForEachEntry( vOuts, iOut, k )
+            {
+                pPo = Aig_ManPo( p->pCare, iOut );
+                if ( Aig_ObjIsTravIdCurrent( p->pCare, pPo ) )
+                    continue;
+                Aig_ObjSetTravIdCurrent( p->pCare, pPo );
+                if ( Aig_ObjFanin0(pPo) == Aig_ManConst1(p->pCare) )
+                    continue;
+                pObjAig = Abc_NtkConstructCare_rec( p->pCare, Aig_ObjFanin0(pPo), pMan );
+                if ( pObjAig == NULL )
+                    continue;
+                pObjAig = Aig_NotCond( pObjAig, Aig_ObjFaninC0(pPo) );
+                Aig_ObjCreatePo( pMan, pObjAig );
+            }
+        }
+/*
         Aig_ManForEachPo( p->pCare, pPo, i )
         {
 //            assert( Aig_ObjFanin0(pPo) != Aig_ManConst1(p->pCare) );
@@ -208,6 +228,7 @@ Aig_Man_t * Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode )
             pObjAig = Aig_NotCond( pObjAig, Aig_ObjFaninC0(pPo) );
             Aig_ObjCreatePo( pMan, pObjAig );
         }
+*/
     }
     if ( p->pPars->fResub )
     {