the latest version

3 files changed, 72 insertions, 6 deletions

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;
+}