the latest version

4 files changed, 120 insertions, 117 deletions

diff --git a/src/aig/saig/saigUnfold2.c b/src/aig/saig/saigUnfold2.c
index 72558ab8..e5ff9d2c 100644
--- a/src/aig/saig/saigUnfold2.c
+++ b/src/aig/saig/saigUnfold2.c
@@ -292,9 +292,10 @@ Vec_Vec_t * Ssw_ManFindDirectImplications2( Aig_Man_t * p, int nFrames, int nCon
 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;
+  Vec_Ptr_t  * vNewFlops;
   Aig_Obj_t * pObj;
-  int i, j, k, nNewFlops;
+  int i,  k, nNewFlops;
+  const int fCompl = 0 ;
   if ( fOldAlgo )
     vCands = Saig_ManDetectConstrFunc( pAig, nFrames, nConfs, nProps, fVerbose );
   else
@@ -305,135 +306,57 @@ Aig_Man_t * Saig_ManDupUnfoldConstrsFunc2( Aig_Man_t * pAig, int nFrames, int nC
       return Aig_ManDupDfs( pAig );
     }
   // create new manager
-  pNew = Aig_ManDupWithoutPos( pAig );
+  pNew = Aig_ManDupWithoutPos( pAig ); /* good */
   pNew->nConstrs = pAig->nConstrs + Vec_VecSizeSize(vCands);
+  pNew->nConstrs = pAig->nConstrs + Vec_PtrSize(pAig->unfold2_type_II)
+    + Vec_PtrSize(pAig->unfold2_type_I);
   //  pNew->nConstrsTypeII  = Vec_PtrSize(pAig->unfold2_type_II);
   *typeII_cnt = Vec_PtrSize(pAig->unfold2_type_II);
+
+  /* new set of registers */
+  
   // 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 * type_II_latch
+      = Aig_ObjCreateCi(pNew); /* will get connected later; */
     Aig_Obj_t * x = Aig_ObjRealCopy(pObj);
-    Aig_ObjCreateCo(pNew, x);
+    
+    Aig_Obj_t * n = Aig_And(pNew, 
+                            Aig_NotCond(type_II_latch, fCompl),
+                            Aig_NotCond(x, fCompl));
+    Aig_ObjCreateCo(pNew, n);//Aig_Not(n));
   }                   
-
-
-  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++) );
-             }
-         }
+  Vec_PtrForEachEntry(Aig_Obj_t * , pAig->unfold2_type_II, pObj, k){
+    Aig_Obj_t * x = Aig_ObjRealCopy(pObj);
+    Aig_ObjCreateCo(pNew, x);
+  }                   
+
+  // add new latch outputs
+  nNewFlops = Vec_PtrSize(pAig->unfold2_type_II);
   //assert( nNewFlops == Vec_PtrSize(vNewFlops) );
   Aig_ManSetRegNum( pNew, Aig_ManRegNum(pAig) + nNewFlops );
+  printf("#reg after unfold2: %d\n", 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*************************************************************
 
@@ -470,7 +393,9 @@ Aig_Man_t * Saig_ManDupFoldConstrsFunc2( Aig_Man_t * pAig, int fCompl, int fVerb
 
   // OR the constraint outputs
   pMiter = Aig_ManConst0( pAigNew );
-
+  int typeII_cc = 0;//typeII_cnt;
+  typeII_cnt = 0;
+  
   int  type_II = 0;
     
   Saig_ManForEachPo( pAig, pObj, i )
@@ -483,7 +408,7 @@ Aig_Man_t * Saig_ManDupFoldConstrsFunc2( Aig_Man_t * pAig, int fCompl, int fVerb
       }
       /*  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, 
@@ -491,6 +416,7 @@ Aig_Man_t * Saig_ManDupFoldConstrsFunc2( Aig_Man_t * pAig, int fCompl, int fVerb
                                 Aig_NotCond(type_II_latch, fCompl),
                                 Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) )
                         );
+        printf( "modeling typeII : %d:%s%d \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
       } else 
         pMiter = Aig_Or( pAigNew, pMiter, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) );
     }
@@ -517,11 +443,17 @@ Aig_Man_t * Saig_ManDupFoldConstrsFunc2( Aig_Man_t * pAig, int fCompl, int fVerb
   {
     /* 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( i + typeII_cc < Aig_ManRegNum(pAig)) {
+        Aig_Obj_t *c = Aig_Mux(pAigNew, Aig_Not(pFlopIn), 
+                               Aig_ObjChild0Copy(pObjLi) ,
+                               pObjLo->pData);
+        Aig_ObjCreateCo( pAigNew, c);
+      } else {
+        printf ( "skipping: reg%d\n", i);
+        Aig_ObjCreateCo( pAigNew,Aig_ObjChild0Copy(pObjLi));
+      }
     }
 
   }
@@ -530,19 +462,24 @@ Aig_Man_t * Saig_ManDupFoldConstrsFunc2( Aig_Man_t * pAig, int fCompl, int fVerb
     }
   Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
     
+  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) {
         Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj));
         Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAigNew)+1 );
+        printf( "Latch for typeII : %d:%s%d \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
       }
     }
 
-    
+     
   // create additional flop 
 
   if ( Saig_ManRegNum(pAig) > 0 )
@@ -550,7 +487,7 @@ Aig_Man_t * Saig_ManDupFoldConstrsFunc2( Aig_Man_t * pAig, int fCompl, int fVerb
       Aig_ObjCreateCo( pAigNew, pFlopIn );
       Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAigNew)+1 );
     }
-
+  printf("#reg after fold2: %d\n", Aig_ManRegNum(pAigNew));
   // perform cleanup
   Aig_ManCleanup( pAigNew );
   Aig_ManSeqCleanup( pAigNew );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 63cc04b8..37d0a014 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -294,8 +294,9 @@ 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_CommandUnfold2                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFold2                 ( 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 );
 static int Abc_CommandSaucy                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -871,9 +872,9 @@ 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", "unfold2",        Abc_CommandUnfold2,           1 );    // jlong 
+    Cmd_CommandAdd( pAbc, "Verification", "fold2",        Abc_CommandFold2,           1 );    // jlong 
     Cmd_CommandAdd( pAbc, "Verification", "bm",            Abc_CommandBm,               1 );
     Cmd_CommandAdd( pAbc, "Verification", "bm2",           Abc_CommandBm2,              1 );
     Cmd_CommandAdd( pAbc, "Verification", "saucy3",        Abc_CommandSaucy,            1 );
@@ -35350,5 +35351,5 @@ usage:
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#include "abciUnfold2.c"
+
 ABC_NAMESPACE_IMPL_END
diff --git a/src/base/abci/abcDarUnfold2.c b/src/base/abci/abcDarUnfold2.c
index bacda407..7ebc316c 100644
--- a/src/base/abci/abcDarUnfold2.c
+++ b/src/base/abci/abcDarUnfold2.c
@@ -32,7 +32,7 @@ Abc_Ntk_t * Abc_NtkDarUnfold2( Abc_Ntk_t * pNtk, int nFrames, int nConfs, int nP
     pNtkAig->pSpec = Extra_UtilStrsav(pMan->pSpec);
     Aig_ManStop( pMan );
 
-    return Abc_NtkDarFold2(pNtkAig, 0, fVerbose, typeII_cnt);
+    return pNtkAig;//Abc_NtkDarFold2(pNtkAig, 0, fVerbose, typeII_cnt);
     
     //return pNtkAig;
 }
diff --git a/src/base/abci/abciUnfold2.c b/src/base/abci/abciUnfold2.c
index ec5047d2..c3780c15 100644
--- a/src/base/abci/abciUnfold2.c
+++ b/src/base/abci/abciUnfold2.c
@@ -110,7 +110,7 @@ int Abc_CommandUnfold2( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
     return 0;
 usage:
-    Abc_Print( -2, "usage: unfold [-FCP num] [-savh]\n" );
+    Abc_Print( -2, "usage: unfold2 [-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 );
@@ -119,3 +119,68 @@ usage:
     return 1;
 }
 
+
+
+int Abc_CommandFold2( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int fCompl;
+    int fVerbose;
+    int c;
+    extern Abc_Ntk_t * Abc_NtkDarFold2( Abc_Ntk_t * pNtk, int fCompl, int fVerbose , int);
+    pNtk = Abc_FrameReadNtk(pAbc);
+    // set defaults
+    fCompl    =   0;
+    fVerbose  =   0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "cvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        /* case 'c': */
+        /*     fCompl ^= 1; */
+        /*     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_NtkIsStrash(pNtk) )
+    {
+        Abc_Print( -1, "Currently only works for structurally hashed circuits.\n" );
+        return 0;
+    }
+    if ( Abc_NtkConstrNum(pNtk) == 0 )
+    {
+        Abc_Print( 0, "The network has no constraints.\n" );
+        return 0;
+    }
+    if ( Abc_NtkIsComb(pNtk) )
+        Abc_Print( 0, "The network is combinational.\n" );
+    // modify the current network
+    pNtkRes = Abc_NtkDarFold2( pNtk, fCompl, fVerbose ,0);
+    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: fold [-cvh]\n" );
+    Abc_Print( -2, "\t         folds constraints represented as separate outputs\n" );
+    //    Abc_Print( -2, "\t-c     : toggle complementing constraints while folding [default = %s]\n", fCompl? "yes": "no" );
+    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;
+}