Added deriving abstraction in GIA from the precomputed flop map.

7 files changed, 115 insertions, 62 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 195abcc9..3beed711 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -656,6 +656,7 @@ extern Gia_Man_t *         Gia_ManMiter( Gia_Man_t * pAig0, Gia_Man_t * pAig1, i
 extern Gia_Man_t *         Gia_ManTransformMiter( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManChoiceMiter( Vec_Ptr_t * vGias );
 extern Gia_Man_t *         Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes );
+extern Gia_Man_t *         Gia_ManDupAbstraction( Gia_Man_t * p, Vec_Int_t * vFlopClasses );
 /*=== giaEnable.c ==========================================================*/
 extern void                Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset, int fVerbose );
 extern Gia_Man_t *         Gia_ManUnrollAndCofactor( Gia_Man_t * p, int nFrames, int nFanMax, int fVerbose );
diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c
index 7a4e51f4..2f7959a8 100644
--- a/src/aig/gia/giaAbs.c
+++ b/src/aig/gia/giaAbs.c
@@ -120,12 +120,12 @@ Vec_Int_t * Gia_ManClasses2Flops( Vec_Int_t * vFlopClasses )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManCexAbstraction( Gia_Man_t * p, Vec_Int_t * vFlops )
+Gia_Man_t * Gia_ManDupAbstractionAig( Gia_Man_t * p, Vec_Int_t * vFlops )
 {
     Gia_Man_t * pGia;
     Aig_Man_t * pNew, * pTemp;
     pNew = Gia_ManToAig( p, 0 );
-    pNew = Saig_ManDeriveAbstraction( pTemp = pNew, vFlops );
+    pNew = Saig_ManDupAbstraction( pTemp = pNew, vFlops );
     Aig_ManStop( pTemp );
     pGia = Gia_ManFromAig( pNew );
 //    pGia->vCiNumsOrig = pNew->vCiNumsOrig; 
@@ -168,32 +168,6 @@ void Gia_ManCexAbstractionStart( Gia_Man_t * pGia, Gia_ParAbs_t * pPars )
 
 /**Function*************************************************************
 
-  Synopsis    [Derives abstraction using the latch map.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Gia_Man_t * Gia_ManCexAbstractionDerive( Gia_Man_t * pGia )
-{
-    Vec_Int_t * vFlops;
-    Gia_Man_t * pAbs = NULL;
-    if ( pGia->vFlopClasses == NULL )
-    {
-        printf( "Gia_ManCexAbstractionDerive(): Abstraction latch map is missing.\n" );
-        return NULL;
-    }
-    vFlops = Gia_ManClasses2Flops( pGia->vFlopClasses );
-    pAbs = Gia_ManCexAbstraction( pGia, vFlops );
-    Vec_IntFree( vFlops );
-    return pAbs;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Refines abstraction using the latch map.]
 
   Description []
@@ -273,8 +247,7 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbo
         return 0;
     }
     // derive abstraction
-    vFlops = Saig_ManClasses2Flops( pGia->vFlopClasses );
-    pAbs = Gia_ManCexAbstraction( pGia, vFlops );
+    pAbs = Gia_ManDupAbstraction( pGia, pGia->vFlopClasses );
     // refine abstraction using PBA
     pAig = Gia_ManToAigSimple( pAbs );
     Gia_ManStop( pAbs );
@@ -283,6 +256,7 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbo
     // derive new classes
     if ( vFlopsNew != NULL )
     {
+        vFlops = Gia_ManClasses2Flops( pGia->vFlopClasses );
         vSelected = Gia_ManFlopsSelect( vFlops, vFlopsNew );
         Vec_IntFree( pGia->vFlopClasses );
         pGia->vFlopClasses = Saig_ManFlops2Classes( Gia_ManRegNum(pGia), vSelected );
@@ -292,7 +266,6 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbo
         Vec_IntFree( vFlops );
         return 1;
     }
-    Vec_IntFree( vFlops );
     // found counter-eample for the abstracted model
     // or exceeded conflict limit
     return 0;
@@ -321,8 +294,7 @@ int Gia_ManCbaPerform( Gia_Man_t * pGia, void * p )
         pGia->vFlopClasses = Vec_IntStart( Gia_ManRegNum(pGia) );
     }
     // derive abstraction
-    vFlops = Saig_ManClasses2Flops( pGia->vFlopClasses );
-    pAbs = Gia_ManCexAbstraction( pGia, vFlops );
+    pAbs = Gia_ManDupAbstraction( pGia, pGia->vFlopClasses );
     // refine abstraction using PBA
     pAig = Gia_ManToAigSimple( pAbs );
     Gia_ManStop( pAbs );
@@ -331,6 +303,7 @@ int Gia_ManCbaPerform( Gia_Man_t * pGia, void * p )
     // derive new classes
     if ( vFlopsNew != NULL )
     {
+        vFlops = Gia_ManClasses2Flops( pGia->vFlopClasses );
 //        vSelected = Saig_ManFlopsSelect( vFlops, vFlopsNew );
         vSelected = NULL;
         Vec_IntFree( pGia->vFlopClasses );
@@ -341,7 +314,6 @@ int Gia_ManCbaPerform( Gia_Man_t * pGia, void * p )
         Vec_IntFree( vFlops );
         return 1;
     }
-    Vec_IntFree( vFlops );
     // found counter-eample for the abstracted model
     // or exceeded conflict limit
     return 0;
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 0c9e2fb7..9942d37f 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -1506,6 +1506,81 @@ Gia_Man_t * Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes )
     return pNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the AIG manager recursively.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManDupAbstraction_rec( Gia_Man_t * pNew, Gia_Obj_t * pObj )
+{
+    if ( ~pObj->Value )
+        return;
+    Gia_ManDupAbstraction_rec( pNew, Gia_ObjFanin0(pObj) );
+    Gia_ManDupAbstraction_rec( pNew, Gia_ObjFanin1(pObj) );
+    pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs abstraction of the AIG to preserve the included flops.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupAbstraction( Gia_Man_t * p, Vec_Int_t * vFlopClasses )
+{ 
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj;
+    int i, nFlops = 0;
+    Gia_ManFillValue( p );
+    // start the new manager
+    pNew = Gia_ManStart( 5000 );
+    pNew->pName = Gia_UtilStrsav( p->pName );
+    // create PIs
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachPi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi(pNew);
+    // create additional PIs
+    Gia_ManForEachRo( p, pObj, i )
+        if ( !Vec_IntEntry(vFlopClasses, i) )
+            pObj->Value = Gia_ManAppendCi(pNew);
+    // create ROs
+    Gia_ManForEachRo( p, pObj, i )
+        if ( Vec_IntEntry(vFlopClasses, i) )
+            pObj->Value = Gia_ManAppendCi(pNew);
+    // create POs
+    Gia_ManHashAlloc( pNew );
+    Gia_ManForEachPo( p, pObj, i )
+    {
+        Gia_ManDupAbstraction_rec( pNew, Gia_ObjFanin0(pObj) );
+        Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    }
+    // create RIs
+    Gia_ManForEachRi( p, pObj, i )
+        if ( Vec_IntEntry(vFlopClasses, i) )
+        {
+            Gia_ManDupAbstraction_rec( pNew, Gia_ObjFanin0(pObj) );
+            Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+            nFlops++;
+        }
+    Gia_ManHashStop( pNew );
+    Gia_ManSetRegNum( pNew, nFlops );
+    // clean up
+    pNew = Gia_ManSeqCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index 93375fd8..d2ef8838 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -154,7 +154,7 @@ extern Aig_Man_t *       Saig_ManDupUnfoldConstrsFunc( Aig_Man_t * pAig, int nFr
 /*=== saigDup.c ==========================================================*/
 extern Aig_Man_t *       Saig_ManDupOrpos( Aig_Man_t * p );
 extern Aig_Man_t *       Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t * vPairs );
-extern Aig_Man_t *       Saig_ManDeriveAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops );
+extern Aig_Man_t *       Saig_ManDupAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops );
 extern int               Saig_ManVerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p );
 extern int               Saig_ManFindFailedPoCex( Aig_Man_t * pAig, Abc_Cex_t * p );
 /*=== saigHaig.c ==========================================================*/
diff --git a/src/aig/saig/saigAbsStart.c b/src/aig/saig/saigAbsStart.c
index 6ec2c21d..13d11224 100644
--- a/src/aig/saig/saigAbsStart.c
+++ b/src/aig/saig/saigAbsStart.c
@@ -204,7 +204,7 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo
     Vec_IntForEachEntryStart( vFlops, Entry, i, 1 )
         assert( Vec_IntEntry(vFlops, i-1) != Entry );
 
-    return Saig_ManDeriveAbstraction( p, vFlops );
+    return Saig_ManDupAbstraction( p, vFlops );
 }
  
 /**Function*************************************************************
@@ -223,7 +223,7 @@ int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Abc_Cex_t * pCex,
     Aig_Man_t * pAbs;
     Vec_Int_t * vFlopsNew;
     int i, Entry, clk = clock();
-    pAbs = Saig_ManDeriveAbstraction( p, vFlops );
+    pAbs = Saig_ManDupAbstraction( p, vFlops );
     if ( fSensePath )
         vFlopsNew = Saig_ManExtendCounterExampleTest2( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pCex, fVerbose );
     else
@@ -291,7 +291,7 @@ Vec_Int_t * Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars )
     Vec_IntPush( vFlops, iFlop );
 */
     // create the resulting AIG
-    pAbs = Saig_ManDeriveAbstraction( p, vFlops );
+    pAbs = Saig_ManDupAbstraction( p, vFlops );
     if ( !pPars->fVerbose )
     {
         printf( "Init : " );
diff --git a/src/aig/saig/saigDup.c b/src/aig/saig/saigDup.c
index b2b33bdb..103cdf7b 100644
--- a/src/aig/saig/saigDup.c
+++ b/src/aig/saig/saigDup.c
@@ -129,26 +129,6 @@ Aig_Man_t * Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t * vPairs )
 
 /**Function*************************************************************
 
-  Synopsis    [Duplicates the AIG manager recursively.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t * Saig_ManAbstractionDfs_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj )
-{
-    if ( pObj->pData )
-        return (Aig_Obj_t *)pObj->pData;
-    Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin0(pObj) );
-    Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin1(pObj) );
-    return (Aig_Obj_t *)(pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ));
-}
-
-/**Function*************************************************************
-
   Synopsis    [Trims the model by removing PIs without fanout.]
 
   Description []
@@ -193,6 +173,26 @@ Aig_Man_t * Saig_ManTrimPis( Aig_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Duplicates the AIG manager recursively.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Saig_ManAbstractionDfs_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj )
+{
+    if ( pObj->pData )
+        return (Aig_Obj_t *)pObj->pData;
+    Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin0(pObj) );
+    Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin1(pObj) );
+    return (Aig_Obj_t *)(pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ));
+}
+
+/**Function*************************************************************
+
   Synopsis    [Performs abstraction of the AIG to preserve the included flops.]
 
   Description []
@@ -202,14 +202,14 @@ Aig_Man_t * Saig_ManTrimPis( Aig_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Saig_ManDeriveAbstraction( Aig_Man_t * p, Vec_Int_t * vFlops )
+Aig_Man_t * Saig_ManDupAbstraction( Aig_Man_t * p, Vec_Int_t * vFlops )
 { 
     Aig_Man_t * pNew;//, * pTemp;
     Aig_Obj_t * pObj, * pObjLi, * pObjLo;
     int i, Entry;
     Aig_ManCleanData( p );
     // start the new manager
-    pNew = Aig_ManStart( Aig_ManNodeNum(p) );
+    pNew = Aig_ManStart( 5000 );
     pNew->pName = Aig_UtilStrsav( p->pName );
     // map the constant node
     Aig_ManConst1(p)->pData = Aig_ManConst1( pNew );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 2492fb37..20c1e471 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -27955,13 +27955,18 @@ int Abc_CommandAbc9AbsDerive( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "The network is combinational.\n" );
         return 0;
     }
-    pTemp = Gia_ManCexAbstractionDerive( pAbc->pGia );
+    if ( pAbc->pGia->vFlopClasses == NULL )
+    {
+        Abc_Print( -1, "Abstraction flop map is missing.\n" );
+        return 0;
+    }
+    pTemp = Gia_ManDupAbstraction( pAbc->pGia, pAbc->pGia->vFlopClasses );
     Abc_CommandUpdate9( pAbc, pTemp );
     return 0;
 
 usage:
     Abc_Print( -2, "usage: &abs_derive [-vh]\n" );
-    Abc_Print( -2, "\t        performs abstraction using the pre-computed flop map\n" );
+    Abc_Print( -2, "\t        derives abstracted model using the pre-computed flop map\n" );
     Abc_Print( -2, "\t-v    : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h    : print the command usage\n");
     return 1;