merge unfold2

10 files changed, 772 insertions, 4 deletions

diff --git a/Makefile b/Makefile
index 72b35134..50357b3e 100644
--- a/Makefile
+++ b/Makefile
@@ -131,7 +131,7 @@ tags:
 
 $(PROG): $(OBJ)
 	@echo "$(MSG_PREFIX)\`\` Building binary:" $(notdir $@)
-	@$(LD) -o $@ $^ $(LIBS)
+	$(LD) -o $@ $^ $(LIBS)
 
 lib$(PROG).a: $(OBJ)
 	@echo "$(MSG_PREFIX)\`\` Linking:" $(notdir $@)
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index db7d380d..e92e512c 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -165,6 +165,10 @@ struct Aig_Man_t_
     // timing statistics
     abctime          time1;
     abctime          time2;
+  //-- jlong -- begin
+  Vec_Ptr_t *      unfold2_type_I;
+  Vec_Ptr_t *      unfold2_type_II;
+  //-- jlong -- end
 };
 
 // cut computation
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 230a2b18..246e0501 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -60,6 +60,10 @@ Aig_Man_t * Aig_ManStart( int nNodesMax )
     p->vCos  = Vec_PtrAlloc( 100 );
     p->vObjs = Vec_PtrAlloc( 1000 );
     p->vBufs = Vec_PtrAlloc( 100 );
+    //--jlong -- begin
+       p->unfold2_type_I = Vec_PtrAlloc( 4);
+       p->unfold2_type_II = Vec_PtrAlloc( 4);
+       //--jlong -- end
     // prepare the internal memory manager
     p->pMemObjs = Aig_MmFixedStart( sizeof(Aig_Obj_t), nNodesMax );
     // create the constant node
@@ -200,6 +204,10 @@ void Aig_ManStop( Aig_Man_t * p )
     Vec_PtrFreeP( &p->vCos );
     Vec_PtrFreeP( &p->vObjs );
     Vec_PtrFreeP( &p->vBufs );
+    //--jlong -- begin
+    Vec_PtrFreeP( &p->unfold2_type_I );
+    Vec_PtrFreeP( &p->unfold2_type_II );
+    //--jlong -- end
     Vec_IntFreeP( &p->vLevelR );
     Vec_VecFreeP( &p->vLevels );
     Vec_IntFreeP( &p->vFlopNums );
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index 475f476d..380af64b 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -116,6 +116,11 @@ extern void              Saig_ManDetectConstrFuncTest( Aig_Man_t * p, int nFrame
 /*=== saigConstr2.c ==========================================================*/
 extern Aig_Man_t *       Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbose );
 extern Aig_Man_t *       Saig_ManDupUnfoldConstrsFunc( Aig_Man_t * pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose );
+// -- jlong -- begin
+extern Aig_Man_t *       Saig_ManDupFoldConstrsFunc2( Aig_Man_t * pAig, int fCompl, int fVerbose, int typeII_cnt );
+extern Aig_Man_t *       Saig_ManDupUnfoldConstrsFunc2( Aig_Man_t * pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose , int * typeII_cnt);
+// --jlong -- end
+
 /*=== saigDual.c ==========================================================*/
 extern Aig_Man_t *       Saig_ManDupDual( Aig_Man_t * pAig, Vec_Int_t * vDcFlops, int nDualPis, int fDualFfs, int fMiterFfs, int fComplPo, int fCheckZero, int fCheckOne );
 extern void              Saig_ManBlockPo( Aig_Man_t * pAig, int nCycles );
diff --git a/src/aig/saig/saigConstr2.c b/src/aig/saig/saigConstr2.c
index 8ab5df51..6e560b59 100644
--- a/src/aig/saig/saigConstr2.c
+++ b/src/aig/saig/saigConstr2.c
@@ -1008,6 +1008,6 @@ Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbo
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-
+#include "saigUnfold2.c"
 ABC_NAMESPACE_IMPL_END
 
diff --git a/src/aig/saig/saigUnfold2.c b/src/aig/saig/saigUnfold2.c
new file mode 100644
index 00000000..72558ab8
--- /dev/null
+++ b/src/aig/saig/saigUnfold2.c
@@ -0,0 +1,558 @@
+
+int  Saig_ManFilterUsingIndOne2( Aig_Man_t * p, Aig_Man_t * pFrame, sat_solver * pSat, Cnf_Dat_t * pCnf, int nConfs, int nProps, int Counter 
+                                 , int type_ /* jlong --  */
+                                 )
+{
+  Aig_Obj_t * pObj;
+  int Lit, status;
+  pObj = Aig_ManCo( pFrame, Counter*3+type_ ); /* which co */
+  Lit  = toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 0 );
+  status = sat_solver_solve( pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfs, 0, 0, 0 );
+  if ( status == l_False )    /* unsat */
+      return status;
+  if ( status == l_Undef )
+    {
+      printf( "Solver returned undecided.\n" );
+      return status;
+    }
+  assert( status == l_True );
+  return status;
+}
+
+Aig_Man_t * Saig_ManCreateIndMiter2( Aig_Man_t * pAig, Vec_Vec_t * vCands )
+{
+  int nFrames = 3;
+    Vec_Ptr_t * vNodes;
+    Aig_Man_t * pFrames;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
+    Aig_Obj_t ** pObjMap;
+    int i, f, k;
+
+    // create mapping for the frames nodes
+    pObjMap  = ABC_CALLOC( Aig_Obj_t *, nFrames * Aig_ManObjNumMax(pAig) );
+
+    // start the fraig package
+    pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * nFrames );
+    pFrames->pName = Abc_UtilStrsav( pAig->pName );
+    pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec );
+    // map constant nodes
+    for ( f = 0; f < nFrames; f++ )
+        Aig_ObjSetFrames( pObjMap, nFrames, Aig_ManConst1(pAig), f, Aig_ManConst1(pFrames) );
+    // create PI nodes for the frames
+    for ( f = 0; f < nFrames; f++ )
+        Aig_ManForEachPiSeq( pAig, pObj, i )
+            Aig_ObjSetFrames( pObjMap, nFrames, pObj, f, Aig_ObjCreateCi(pFrames) );
+    // set initial state for the latches
+    Aig_ManForEachLoSeq( pAig, pObj, i )
+        Aig_ObjSetFrames( pObjMap, nFrames, pObj, 0, Aig_ObjCreateCi(pFrames) );
+
+    // add timeframes
+    for ( f = 0; f < nFrames; f++ )
+    {
+        // add internal nodes of this frame
+        Aig_ManForEachNode( pAig, pObj, i )
+        {
+            pObjNew = Aig_And( pFrames, Aig_ObjChild0Frames(pObjMap,nFrames,pObj,f), Aig_ObjChild1Frames(pObjMap,nFrames,pObj,f) );
+            Aig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew );
+        }
+        // set the latch inputs and copy them into the latch outputs of the next frame
+        Aig_ManForEachLiLoSeq( pAig, pObjLi, pObjLo, i )
+        {
+            pObjNew = Aig_ObjChild0Frames(pObjMap,nFrames,pObjLi,f);
+            if ( f < nFrames - 1 )
+                Aig_ObjSetFrames( pObjMap, nFrames, pObjLo, f+1, pObjNew );
+        }
+    }
+    
+    // go through the candidates
+    Vec_VecForEachLevel( vCands, vNodes, i )
+    {
+        Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
+        {
+            Aig_Obj_t * pObjR  = Aig_Regular(pObj);
+            Aig_Obj_t * pNode0 = pObjMap[nFrames*Aig_ObjId(pObjR)+0];
+            Aig_Obj_t * pNode1 = pObjMap[nFrames*Aig_ObjId(pObjR)+1];
+        {
+          Aig_Obj_t * pFan0  = Aig_NotCond( pNode0,  Aig_IsComplement(pObj) );
+          Aig_Obj_t * pFan1  = Aig_NotCond( pNode1, !Aig_IsComplement(pObj) );
+          Aig_Obj_t * pMiter = Aig_And( pFrames, pFan0, pFan1 );
+          Aig_ObjCreateCo( pFrames, pMiter );
+        
+        /* need to check p & Xp is satisfiable */
+                    /* jlong -- begin */
+          Aig_Obj_t * pMiter2 = Aig_And( pFrames, pFan0, Aig_Not(pFan1));
+          Aig_ObjCreateCo( pFrames, pMiter2 ); /* jlong -- end  */
+        }
+
+        {            /* jlong -- begin */
+          Aig_Obj_t * pNode2 = pObjMap[nFrames*Aig_ObjId(pObjR)+2];
+          Aig_Obj_t * pFan0  = Aig_NotCond( pNode0,  Aig_IsComplement(pObj) );
+          Aig_Obj_t * pFan1  = Aig_NotCond( pNode1,  Aig_IsComplement(pObj) );
+          Aig_Obj_t * pFan2  = Aig_NotCond( pNode2, !Aig_IsComplement(pObj) );
+          Aig_Obj_t * pMiter = Aig_And( pFrames, Aig_And(pFrames, pFan0, pFan1 ), pFan2);
+          Aig_ObjCreateCo( pFrames, pMiter ); /* jlong -- end  */
+        }
+
+        }
+    }
+    Aig_ManCleanup( pFrames );
+    ABC_FREE( pObjMap );
+
+//Aig_ManShow( pAig, 0, NULL );
+//Aig_ManShow( pFrames, 0, NULL );
+    return pFrames;
+}
+
+/**Function*************************************************************
+
+   Synopsis    [Detects constraints functionally.]
+
+   Description []
+               
+   SideEffects []
+
+   SeeAlso     []
+
+***********************************************************************/
+void Saig_ManFilterUsingInd2( Aig_Man_t * p, Vec_Vec_t * vCands, int nConfs, int nProps, int fVerbose )
+{
+  Vec_Ptr_t * vNodes;
+  Aig_Man_t * pFrames;
+  sat_solver * pSat;
+  Cnf_Dat_t * pCnf;
+  Aig_Obj_t * pObj;
+  int i, k, k2, Counter;
+  /*
+    Vec_VecForEachLevel( vCands, vNodes, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
+    printf( "%d ", Aig_ObjId(Aig_Regular(pObj)) );
+    printf( "\n" );
+  */
+  // create timeframes 
+  //    pFrames = Saig_ManUnrollInd( p );
+  pFrames = Saig_ManCreateIndMiter2( p, vCands );
+  assert( Aig_ManCoNum(pFrames) == Vec_VecSizeSize(vCands)*3 );
+  // start the SAT solver
+  pCnf = Cnf_DeriveSimple( pFrames, Aig_ManCoNum(pFrames) );
+  pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+  // check candidates
+  if ( fVerbose )
+    printf( "Filtered cands:  \n" );
+  Counter = 0;
+  Vec_VecForEachLevel( vCands, vNodes, i )
+    {
+      assert(i==0);             /* only one item */
+      k2 = 0;
+      Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
+        {
+          if ( Saig_ManFilterUsingIndOne2( p, pFrames, pSat, pCnf, nConfs, nProps, Counter++ , 0) == l_False)
+            //            if ( Saig_ManFilterUsingIndOne_old( p, pSat, pCnf, nConfs, pObj ) )
+            {
+              Vec_PtrWriteEntry( vNodes, k2++, pObj );
+              if ( fVerbose )
+                printf( "%d:%s%d \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
+              printf( " type I : %d:%s%d \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
+              Vec_PtrPush(p->unfold2_type_I, pObj);
+            }
+          /* jlong -- begin  */
+          else if ( Saig_ManFilterUsingIndOne2( p, pFrames, pSat, pCnf, nConfs, nProps, Counter-1 , 1) == l_True ) /* can be self-conflicting */
+            {
+              if ( Saig_ManFilterUsingIndOne2( p, pFrames, pSat, pCnf, nConfs, nProps, Counter-1 , 2) == l_False ){
+                //Vec_PtrWriteEntry( vNodes, k2++, pObj );
+                if ( fVerbose )
+                  printf( "%d:%s%d  \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
+                printf( " type II: %d:%s%d  \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
+                Vec_PtrWriteEntry( vNodes, k2++, pObj ); /* add type II constraints */
+                Vec_PtrPush(p->unfold2_type_II, pObj);
+              }
+            }
+          /* jlong -- end  */
+        }
+      Vec_PtrShrink( vNodes, k2 );
+    }
+
+  // clean up
+  Cnf_DataFree( pCnf );
+  sat_solver_delete( pSat );
+  if ( fVerbose )
+    Aig_ManPrintStats( pFrames );
+  Aig_ManStop( pFrames );
+}
+
+
+/**Function*************************************************************
+
+   Synopsis    [Returns the number of variables implied by the output.]
+
+   Description []
+               
+   SideEffects []
+
+   SeeAlso     []
+
+***********************************************************************/
+Vec_Vec_t * Ssw_ManFindDirectImplications2( Aig_Man_t * p, int nFrames, int nConfs, int nProps, int fVerbose )
+{
+  Vec_Vec_t * vCands = NULL;
+  Vec_Ptr_t * vNodes;
+  Cnf_Dat_t * pCnf;
+  sat_solver * pSat;
+  Aig_Man_t * pFrames;
+  Aig_Obj_t * pObj, * pRepr, * pReprR;
+  int i, f, k, value;
+  assert(nFrames == 1);
+  vCands = Vec_VecAlloc( nFrames );
+  assert(nFrames == 1);
+  // perform unrolling
+  pFrames = Saig_ManUnrollCOI( p, nFrames );
+  assert( Aig_ManCoNum(pFrames) == 1 );
+  // start the SAT solver
+  pCnf = Cnf_DeriveSimple( pFrames, 0 );
+  pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+  if ( pSat != NULL )
+    {
+      Aig_ManIncrementTravId( p );
+      for ( f = 0; f < nFrames; f++ )
+        {
+          Aig_ManForEachObj( p, pObj, i )
+            {
+              if ( !Aig_ObjIsCand(pObj) )
+                continue;
+              //--jlong : also use internal nodes as well
+              /* if ( !Aig_ObjIsCi(pObj) ) */
+              /*   continue; */ 
+              if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+                continue;
+              // get the node from timeframes
+              pRepr  = p->pObjCopies[nFrames*i + nFrames-1-f];
+              pReprR = Aig_Regular(pRepr);
+              if ( pCnf->pVarNums[Aig_ObjId(pReprR)] < 0 )
+                continue;
+              //                value = pSat->assigns[ pCnf->pVarNums[Aig_ObjId(pReprR)] ];
+              value = sat_solver_get_var_value( pSat, pCnf->pVarNums[Aig_ObjId(pReprR)] );
+              if ( value == l_Undef )
+                continue;
+              // label this node as taken
+              Aig_ObjSetTravIdCurrent(p, pObj);
+              if ( Saig_ObjIsLo(p, pObj) )
+                Aig_ObjSetTravIdCurrent( p, Aig_ObjFanin0(Saig_ObjLoToLi(p, pObj)) );
+              // remember the node
+              Vec_VecPush( vCands, f, Aig_NotCond( pObj, (value == l_True) ^ Aig_IsComplement(pRepr) ) );
+              //        printf( "%s%d ", (value == l_False)? "":"!", i );
+            }
+        }
+      //    printf( "\n" );
+      sat_solver_delete( pSat );
+    }
+  Aig_ManStop( pFrames );
+  Cnf_DataFree( pCnf );
+
+  if ( fVerbose )
+    {
+      printf( "Found %3d candidates.\n", Vec_VecSizeSize(vCands) );
+      Vec_VecForEachLevel( vCands, vNodes, k )
+        {
+          printf( "Level %d. Cands  =%d    ", k, Vec_PtrSize(vNodes) );
+          //            Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
+          //                printf( "%d:%s%d ", k, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
+          printf( "\n" );
+        }
+    }
+
+  ABC_FREE( p->pObjCopies );
+  /* -- jlong -- this does the SAT proof of the constraints */
+  Saig_ManFilterUsingInd2( p, vCands, nConfs, nProps, fVerbose );
+  if ( Vec_VecSizeSize(vCands) )
+    printf( "Found %3d constraints after filtering.\n", Vec_VecSizeSize(vCands) );
+  if ( fVerbose )
+    {
+      Vec_VecForEachLevel( vCands, vNodes, k )
+        {
+          printf( "Level %d. Constr =%d    ", k, Vec_PtrSize(vNodes) );
+          //            Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
+          //                printf( "%d:%s%d ", k, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
+          printf( "\n" );
+        }
+    }
+  
+  return vCands;
+}
+
+/**Function*************************************************************
+
+   Synopsis    [Duplicates the AIG while unfolding constraints.]
+
+   Description []
+               
+   SideEffects []
+
+   SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManDupUnfoldConstrsFunc2( Aig_Man_t * pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose , int * typeII_cnt){
+  Aig_Man_t * pNew;
+  Vec_Vec_t * vCands;
+  Vec_Ptr_t * vNodes, * vNewFlops;
+  Aig_Obj_t * pObj;
+  int i, j, k, nNewFlops;
+  if ( fOldAlgo )
+    vCands = Saig_ManDetectConstrFunc( pAig, nFrames, nConfs, nProps, fVerbose );
+  else
+    vCands = Ssw_ManFindDirectImplications2( pAig, nFrames, nConfs, nProps, fVerbose );
+  if ( vCands == NULL || Vec_VecSizeSize(vCands) == 0 )
+    {
+      Vec_VecFreeP( &vCands );
+      return Aig_ManDupDfs( pAig );
+    }
+  // create new manager
+  pNew = Aig_ManDupWithoutPos( pAig );
+  pNew->nConstrs = pAig->nConstrs + Vec_VecSizeSize(vCands);
+  //  pNew->nConstrsTypeII  = Vec_PtrSize(pAig->unfold2_type_II);
+  *typeII_cnt = Vec_PtrSize(pAig->unfold2_type_II);
+  // add normal POs
+  Saig_ManForEachPo( pAig, pObj, i )
+    Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
+  // create constraint outputs
+  vNewFlops = Vec_PtrAlloc( 100 );
+
+  
+  Vec_PtrForEachEntry(Aig_Obj_t * , pAig->unfold2_type_I, pObj, k){
+    Aig_Obj_t * x = Aig_ObjRealCopy(pObj);
+    Aig_ObjCreateCo(pNew, x);
+  }
+   
+  Vec_PtrForEachEntry(Aig_Obj_t * , pAig->unfold2_type_II, pObj, k){
+    Aig_Obj_t * x = Aig_ObjRealCopy(pObj);
+    Aig_ObjCreateCo(pNew, x);
+  }                   
+
+
+  if(0)  Vec_VecForEachLevel( vCands, vNodes, i )
+    {
+      assert(i==0);
+      Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
+        {
+          Vec_PtrPush( vNewFlops, Aig_ObjRealCopy(pObj) );
+          for ( j = 0; j < i; j++ )
+            Vec_PtrPush( vNewFlops, Aig_ObjCreateCi(pNew) );
+          Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Vec_PtrPop(vNewFlops) );
+        }
+    }
+  // add latch outputs
+  Saig_ManForEachLi( pAig, pObj, i )
+    Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
+  // add new latch outputs
+  nNewFlops = 0;//Vec_VecSizeSize(vCands);
+  
+  if(0)Vec_VecForEachLevel( vCands, vNodes, i )
+         {
+           Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
+             {
+               for ( j = 0; j < i; j++ )
+                 Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Vec_PtrEntry(vNewFlops, nNewFlops++) );
+             }
+         }
+  //assert( nNewFlops == Vec_PtrSize(vNewFlops) );
+  Aig_ManSetRegNum( pNew, Aig_ManRegNum(pAig) + nNewFlops );
+  Vec_VecFreeP( &vCands );
+  Vec_PtrFree( vNewFlops );
+  return pNew;
+
+}
+Aig_Man_t * Saig_ManDupUnfoldConstrsFunc2_( Aig_Man_t * pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose )
+{
+  Aig_Man_t * pNew;
+  Vec_Vec_t * vCands;
+  //  Vec_Ptr_t * vNodes, * vNewFlops;
+  Aig_Obj_t * pObj;
+  int i,  k;
+  Aig_Obj_t * pMiter = NULL;
+  const int fCompl = 0;
+
+
+  if ( fOldAlgo )
+    vCands = Saig_ManDetectConstrFunc( pAig, nFrames, nConfs, nProps, fVerbose );
+  else
+    vCands = Ssw_ManFindDirectImplications2( pAig, nFrames, nConfs, nProps, fVerbose );
+  if ( vCands == NULL || Vec_VecSizeSize(vCands) == 0 )
+    {
+      Vec_VecFreeP( &vCands );
+      return Aig_ManDupDfs( pAig );
+    }
+  // create new manager
+  pNew = Aig_ManDupWithoutPos( pAig );
+  
+  pMiter = Aig_ManConst0( pNew );
+  
+  Vec_PtrForEachEntry(Aig_Obj_t * , pAig->unfold2_type_I, pObj, k){
+    
+    pMiter = Aig_Or( pNew, pMiter, 
+                     Aig_NotCond( Aig_ObjRealCopy(pObj), fCompl ) );
+    printf("new id: %d\n", Aig_ObjId(pMiter));
+  }
+
+  Vec_PtrForEachEntry(Aig_Obj_t * , pAig->unfold2_type_II, pObj, k){
+    Aig_Obj_t * type_II_latch 
+      = Aig_ObjCreateCi(pNew); /* will get connected later; */
+    Aig_Obj_t *kk =   Aig_And(pNew, 
+                            Aig_NotCond(type_II_latch, fCompl),
+                            Aig_NotCond(Aig_ObjRealCopy(pObj), fCompl)
+                            );
+                  
+    pMiter = Aig_Or(pNew, pMiter, kk
+                    );
+  }
+  {
+    Aig_Obj_t * pObjLi, *pObjLo;
+    Aig_Obj_t * pFlopOut = Aig_ObjCreateCi(pNew);
+    Aig_Obj_t * pFlopIn  = Aig_Or(pNew, pMiter, pFlopOut);
+    
+    Saig_ManForEachPo(pAig, pObj, i){
+      Aig_Obj_t *p = Aig_And( pNew, Aig_ObjChild0(pObj), Aig_Not(pFlopIn) );      
+      printf("new id: %d\n", Aig_ObjId(p));
+      Aig_ObjCreateCo(pNew, p);
+    }
+
+    // add latch outputs
+    
+    Saig_ManForEachLiLo(pAig, pObjLi, pObjLo, i){
+      Aig_Obj_t *c = Aig_Mux(pNew, Aig_Not(pFlopIn), 
+                             Aig_ObjChild0Copy(pObjLi) ,
+                             Aig_ObjRealCopy(pObjLo));//->pData);
+      Aig_ObjCreateCo(pNew, c);
+      printf("new id: %d\n", Aig_ObjId(c));
+    }
+
+ 
+    
+    Vec_PtrForEachEntry(Aig_Obj_t * , pAig->unfold2_type_II, pObj, k){
+      Aig_ObjCreateCo( pNew, Aig_ObjRealCopy(pObj));
+    }
+    Aig_ObjCreateCo(pNew, pFlopIn);
+  }
+  Aig_ManSetRegNum( pNew, Aig_ManRegNum(pAig) + Vec_PtrSize(pAig->unfold2_type_II) + 1);
+  Vec_VecFreeP( &vCands );
+  return pNew;
+}
+
+/**Function*************************************************************
+
+   Synopsis    [Duplicates the AIG while unfolding constraints.]
+
+   Description []
+               
+   SideEffects []
+
+   SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManDupFoldConstrsFunc2( Aig_Man_t * pAig, int fCompl, int fVerbose , 
+                                         int typeII_cnt)
+{
+  Aig_Man_t * pAigNew;
+  Aig_Obj_t * pMiter, * pFlopOut, * pFlopIn, * pObj;
+  int i;
+  if ( Aig_ManConstrNum(pAig) == 0 )
+    return Aig_ManDupDfs( pAig );
+  assert( Aig_ManConstrNum(pAig) < Saig_ManPoNum(pAig) );
+  // start the new manager
+  pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
+  pAigNew->pName = Abc_UtilStrsav( pAig->pName );
+  pAigNew->pSpec = Abc_UtilStrsav( pAig->pSpec );
+  // map the constant node
+  Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
+  // create variables for PIs
+  Aig_ManForEachCi( pAig, pObj, i )
+    pObj->pData = Aig_ObjCreateCi( pAigNew );
+  // add internal nodes of this frame
+  Aig_ManForEachNode( pAig, pObj, i )
+    pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+
+  // OR the constraint outputs
+  pMiter = Aig_ManConst0( pAigNew );
+
+  int  type_II = 0;
+    
+  Saig_ManForEachPo( pAig, pObj, i )
+    {
+      
+      if ( i < Saig_ManPoNum(pAig)-Aig_ManConstrNum(pAig) )
+        continue;
+      if (i + typeII_cnt >= Saig_ManPoNum(pAig) ) {
+        type_II = 1;
+      }
+      /*  now we got the constraint */
+      if (type_II) {
+        printf("modeling typeII \n");
+        Aig_Obj_t * type_II_latch
+          = Aig_ObjCreateCi(pAigNew); /* will get connected later; */
+        pMiter = Aig_Or(pAigNew, pMiter, 
+                        Aig_And(pAigNew, 
+                                Aig_NotCond(type_II_latch, fCompl),
+                                Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) )
+                        );
+      } else 
+        pMiter = Aig_Or( pAigNew, pMiter, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) );
+    }
+
+  // create additional flop
+  if ( Saig_ManRegNum(pAig) > 0 )
+    {
+      pFlopOut = Aig_ObjCreateCi( pAigNew );
+      pFlopIn  = Aig_Or( pAigNew, pMiter, pFlopOut );
+    }
+  else 
+    pFlopIn = pMiter;
+
+  // create primary output
+  Saig_ManForEachPo( pAig, pObj, i )
+    {
+      if ( i >= Saig_ManPoNum(pAig)-Aig_ManConstrNum(pAig) )
+        continue;
+      pMiter = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_Not(pFlopIn) );
+      Aig_ObjCreateCo( pAigNew, pMiter );
+    }
+
+  // transfer to register outputs
+  {
+    /* the same for type I and type II */
+    Aig_Obj_t * pObjLi, *pObjLo;
+    Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )    {
+      Aig_Obj_t *c = Aig_Mux(pAigNew, Aig_Not(pFlopIn), 
+                             Aig_ObjChild0Copy(pObjLi) ,
+                             pObjLo->pData);
+      Aig_ObjCreateCo( pAigNew, c);
+    }
+
+  }
+  if(0)Saig_ManForEachLi( pAig, pObj, i ) {
+      Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
+    }
+  Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
+    
+  Saig_ManForEachPo( pAig, pObj, i )
+    {
+    
+      if ( i < Saig_ManPoNum(pAig)-Aig_ManConstrNum(pAig) )
+        continue;
+      /*  now we got the constraint */
+      if (type_II) {
+        Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj));
+        Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAigNew)+1 );
+      }
+    }
+
+    
+  // create additional flop 
+
+  if ( Saig_ManRegNum(pAig) > 0 )
+    {
+      Aig_ObjCreateCo( pAigNew, pFlopIn );
+      Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAigNew)+1 );
+    }
+
+  // perform cleanup
+  Aig_ManCleanup( pAigNew );
+  Aig_ManSeqCleanup( pAigNew );
+  return pAigNew;
+}
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 2323ac36..63cc04b8 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -294,6 +294,7 @@ static int Abc_CommandTempor                 ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandInduction              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandConstr                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandUnfold                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandUnfold2                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandFold                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandBm                     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandBm2                    ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -870,6 +871,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Verification", "ind",           Abc_CommandInduction,        0 );
     Cmd_CommandAdd( pAbc, "Verification", "constr",        Abc_CommandConstr,           0 );
     Cmd_CommandAdd( pAbc, "Verification", "unfold",        Abc_CommandUnfold,           1 );
+
+    Cmd_CommandAdd( pAbc, "Verification", "unfold2",        Abc_CommandUnfold2,           1 );    // jlong 
     Cmd_CommandAdd( pAbc, "Verification", "fold",          Abc_CommandFold,             1 );
     Cmd_CommandAdd( pAbc, "Verification", "bm",            Abc_CommandBm,               1 );
     Cmd_CommandAdd( pAbc, "Verification", "bm2",           Abc_CommandBm2,              1 );
@@ -35347,5 +35350,5 @@ usage:
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-
+#include "abciUnfold2.c"
 ABC_NAMESPACE_IMPL_END
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 1870e713..894c9d17 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -4560,6 +4560,6 @@ Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk )
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-
+#include "abcDarUnfold2.c"
 ABC_NAMESPACE_IMPL_END
 
diff --git a/src/base/abci/abcDarUnfold2.c b/src/base/abci/abcDarUnfold2.c
new file mode 100644
index 00000000..bacda407
--- /dev/null
+++ b/src/base/abci/abcDarUnfold2.c
@@ -0,0 +1,69 @@
+/**Function*************************************************************
+
+  Synopsis    [Performs BDD-based reachability analysis.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarFold2( Abc_Ntk_t * pNtk, int fCompl, int fVerbose , int);
+Abc_Ntk_t * Abc_NtkDarUnfold2( Abc_Ntk_t * pNtk, int nFrames, int nConfs, int nProps, int fStruct, int fOldAlgo, int fVerbose )
+{
+    Abc_Ntk_t * pNtkAig;
+    Aig_Man_t * pMan, * pTemp;
+    int typeII_cnt = 0;
+    assert( Abc_NtkIsStrash(pNtk) );
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
+    if ( pMan == NULL )
+        return NULL;
+    if ( fStruct ){
+      assert(0);//pMan = Saig_ManDupUnfoldConstrs( pTemp = pMan );
+    }else
+      pMan = Saig_ManDupUnfoldConstrsFunc2( pTemp = pMan, nFrames, nConfs, nProps, fOldAlgo, fVerbose , &typeII_cnt);
+    Aig_ManStop( pTemp );
+    if ( pMan == NULL )
+        return NULL;
+    //    typeII_cnt = pMan->nConstrsTypeII;
+    pNtkAig = Abc_NtkFromAigPhase( pMan );
+    pNtkAig->pName = Extra_UtilStrsav(pMan->pName);
+    pNtkAig->pSpec = Extra_UtilStrsav(pMan->pSpec);
+    Aig_ManStop( pMan );
+
+    return Abc_NtkDarFold2(pNtkAig, 0, fVerbose, typeII_cnt);
+    
+    //return pNtkAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs BDD-based reachability analysis.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarFold2( Abc_Ntk_t * pNtk, int fCompl, int fVerbose
+                             , int typeII_cnt
+                             )
+{
+    Abc_Ntk_t * pNtkAig;
+    Aig_Man_t * pMan, * pTemp;
+    assert( Abc_NtkIsStrash(pNtk) );
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
+    if ( pMan == NULL )
+        return NULL;
+    pMan = Saig_ManDupFoldConstrsFunc2( pTemp = pMan, fCompl, fVerbose, typeII_cnt );
+    Aig_ManStop( pTemp );
+    pNtkAig = Abc_NtkFromAigPhase( pMan );
+    pNtkAig->pName = Extra_UtilStrsav(pMan->pName);
+    pNtkAig->pSpec = Extra_UtilStrsav(pMan->pSpec);
+    Aig_ManStop( pMan );
+    return pNtkAig;
+}
+
diff --git a/src/base/abci/abciUnfold2.c b/src/base/abci/abciUnfold2.c
new file mode 100644
index 00000000..ec5047d2
--- /dev/null
+++ b/src/base/abci/abciUnfold2.c
@@ -0,0 +1,121 @@
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandUnfold2( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int nFrames;
+    int nConfs;
+    int nProps;
+    int fStruct = 0;
+    int fOldAlgo = 0;
+    int fVerbose;
+    int c;
+    extern Abc_Ntk_t * Abc_NtkDarUnfold2( Abc_Ntk_t * pNtk, int nFrames, int nConfs, int nProps, int fStruct, int fOldAlgo, int fVerbose );
+    pNtk = Abc_FrameReadNtk(pAbc);
+    // set defaults
+    nFrames   =      1;
+    nConfs    =   1000;
+    nProps    =   1000;
+    fVerbose  =      0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CPvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        /* case 'F': */
+        /*     if ( globalUtilOptind >= argc ) */
+        /*     { */
+        /*         Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); */
+        /*         goto usage; */
+        /*     } */
+        /*     nFrames = atoi(argv[globalUtilOptind]); */
+        /*     globalUtilOptind++; */
+        /*     if ( nFrames < 0 ) */
+        /*         goto usage; */
+        /*     break; */
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nConfs = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nConfs < 0 )
+                goto usage;
+            break;
+        case 'P':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nProps = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nProps < 0 )
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        Abc_Print( -1, "Empty network.\n" );
+        return 1;
+    }
+    if ( Abc_NtkIsComb(pNtk) )
+    {
+        Abc_Print( -1, "The network is combinational.\n" );
+        return 0;
+    }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        Abc_Print( -1, "Currently only works for structurally hashed circuits.\n" );
+        return 0;
+    }
+    if ( Abc_NtkConstrNum(pNtk) > 0 )
+    {
+        Abc_Print( -1, "Constraints are already extracted.\n" );
+        return 0;
+    }
+    if ( Abc_NtkPoNum(pNtk) > 1 && !fStruct )
+    {
+        Abc_Print( -1, "Functional constraint extraction works for single-output miters (use \"orpos\").\n" );
+        return 0;
+    }
+    // modify the current network
+    pNtkRes = Abc_NtkDarUnfold2( pNtk, nFrames, nConfs, nProps, fStruct, fOldAlgo, fVerbose );
+    if ( pNtkRes == NULL )
+    {
+        Abc_Print( 1,"Transformation has failed.\n" );
+        return 0;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+usage:
+    Abc_Print( -2, "usage: unfold [-FCP num] [-savh]\n" );
+    Abc_Print( -2, "\t         unfold hidden constraints as separate outputs\n" );
+    Abc_Print( -2, "\t-C num : the max number of conflicts in SAT solving [default = %d]\n", nConfs );
+    Abc_Print( -2, "\t-P num : the max number of constraint propagations [default = %d]\n", nProps );
+    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;
+}
+