Added deriving abstraction in GIA from the precomputed flop map.

3 files changed, 26 insertions, 26 deletions

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 );