1 files changed, 60 insertions, 0 deletions
diff --git a/src/aig/saig/saigDup.c b/src/aig/saig/saigDup.c
index 1a050741..165a08f2 100644
--- a/src/aig/saig/saigDup.c
+++ b/src/aig/saig/saigDup.c
@@ -67,6 +67,66 @@ Aig_Man_t * Said_ManDupOrpos( Aig_Man_t * pAig )
     return pAigNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Numbers of flops included in the abstraction.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops )
+{
+    Aig_Man_t * pAigNew;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+    int i, Entry;
+    // start the new manager
+    pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
+    // map the constant node
+    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
+    // label included flops
+    Vec_IntForEachEntry( vFlops, Entry, i )
+    {
+        pObjLi = Saig_ManLi( pAig, Entry );
+        assert( pObjLi->fMarkA == 0 );
+        pObjLi->fMarkA = 1;
+        pObjLo = Saig_ManLo( pAig, Entry );
+        assert( pObjLo->fMarkA == 0 );
+        pObjLo->fMarkA = 1;
+    }
+    // create variables for PIs
+    Aig_ManForEachPi( pAig, pObj, i )
+        if ( !pObj->fMarkA )
+            pObj->pData = Aig_ObjCreatePi( pAigNew );
+    // create variables for LOs
+    Aig_ManForEachPi( pAig, pObj, i )
+        if ( pObj->fMarkA )
+        {
+            pObj->fMarkA = 0;
+            pObj->pData = Aig_ObjCreatePi( pAigNew );
+        }
+    // add internal nodes of this frame
+    Aig_ManForEachNode( pAig, pObj, i )
+        pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    // create POs
+    Aig_ManForEachPo( pAig, pObj, i )
+        if ( !pObj->fMarkA )
+            Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) );
+    // create LIs
+    Aig_ManForEachPo( pAig, pObj, i )
+        if ( pObj->fMarkA )
+        {
+            pObj->fMarkA = 0;
+            Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) );
+        }
+    Aig_ManCleanup( pAigNew );
+    Aig_ManSetRegNum( pAigNew, Vec_IntSize(vFlops) );
+    return pAigNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////