Unsuccessful attempt to improve PDR and a few minor changes.

1 files changed, 58 insertions, 265 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 415e2797..b100ba19 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -8418,68 +8418,49 @@ usage:
 int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
-    Abc_Ntk_t * pNtkRes = NULL;
+    int nCutMax      =  1;
+    int nLeafMax     = 10;
+    int nDivMax      = 50;
+    int nDecMax      =  3;
+    int fVerbose     =  0;
+    int fVeryVerbose =  0;
     int c;
-    int fBmc;
-    int nFrames;
-    int nLevels;
-    int fVerbose;
-    int fVeryVerbose;
-//    char * pFileName;
-
-//    extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk );
-//    extern Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk );
-//    extern void Abc_NtkMaxFlowTest( Abc_Ntk_t * pNtk );
-//    extern int Pr_ManProofTest( char * pFileName );
-    extern void Abc_NtkCompareSupports( Abc_Ntk_t * pNtk );
-    extern void Abc_NtkCompareCones( Abc_Ntk_t * pNtk );
-    extern Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk );
-    extern Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName );
-    extern Abc_Ntk_t * Abc_NtkFilter( Abc_Ntk_t * pNtk );
-//    extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
-//    extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose );
-    extern Abc_Ntk_t * Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose );
-//    extern void Abc_NtkDarTestBlif( char * pFileName );
-//    extern Abc_Ntk_t * Abc_NtkDarPartition( Abc_Ntk_t * pNtk );
-//    extern Abc_Ntk_t * Abc_NtkTestExor( Abc_Ntk_t * pNtk, int fVerbose );
-//    extern Abc_Ntk_t * Abc_NtkNtkTest( Abc_Ntk_t * pNtk, If_Lib_t * pLutLib );
-    extern Abc_Ntk_t * Abc_NtkDarRetimeStep( Abc_Ntk_t * pNtk, int fVerbose );
-    extern void Abc_NtkDarTest( Abc_Ntk_t * pNtk, int Num );
-//    extern void Aig_ProcedureTest();
-    extern Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk );
-    extern void Amap_LibertyTest( char * pFileName );
-    extern void Bbl_ManTest( Abc_Ntk_t * pNtk );
-    extern void Bbl_ManSimpleDemo();
-    extern Abc_Ntk_t * Abc_NtkCRetime( Abc_Ntk_t * pNtk, int fVerbose );
-    extern void Abc_NktMffcTest( Abc_Ntk_t * pNtk );
-
-    pNtk = Abc_FrameReadNtk(pAbc);
-
-
-
-//    Abc_Print( -1, "This command is temporarily disabled.\n" );
-//    return 0;
-
-    // set defaults
-    fVeryVerbose = 0;
-    fVerbose = 1;
-    fBmc     = 0;
-    nFrames  = 1;
-    nLevels  = 10;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FNbvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CKDNvwh" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'F':
+        case 'C':
             if ( globalUtilOptind >= argc )
             {
-                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
                 goto usage;
             }
-            nFrames = atoi(argv[globalUtilOptind]);
+            nCutMax = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nFrames < 0 ) 
+            if ( nCutMax < 0 ) 
+                goto usage;
+            break;
+        case 'K':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nLeafMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nLeafMax < 0 ) 
+                goto usage;
+            break;
+        case 'D':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-D\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nDivMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nDivMax < 0 ) 
                 goto usage;
             break;
         case 'N':
@@ -8488,14 +8469,11 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
                 Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
                 goto usage;
             }
-            nLevels = atoi(argv[globalUtilOptind]);
+            nDecMax = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nLevels < 0 ) 
+            if ( nDecMax < 0 ) 
                 goto usage;
             break;
-        case 'b':
-            fBmc ^= 1;
-            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -8508,12 +8486,13 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
             goto usage;
         }
     }
-
+/*
     if ( pNtk == NULL )
     {
         Abc_Print( -1, "Empty network.\n" );
         return 1;
     }
+*/
 /*
     if ( Abc_NtkLatchNum(pNtk) == 0 )
     {
@@ -8521,79 +8500,6 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 */
-//    if ( fBmc )
-//        Abc_NtkBddDec( pNtk, 1 );
-//    else
-//        Abc_NktMffcTest( pNtk );
-//    Abc_NtkDarTest( pNtk, nLevels );
-
-//    Abc_NtkTestEsop( pNtk );
-//    Abc_NtkTestSop( pNtk );
-//    Abc_Print( -1, "This command is currently not used.\n" );
-    // run the command
-//    pNtkRes = Abc_NtkMiterForCofactors( pNtk, 0, 0, -1 );
-//    pNtkRes = Abc_NtkNewAig( pNtk );
-
-/*
-    pNtkRes = NULL;
-    if ( pNtkRes == NULL )
-    {
-        Abc_Print( -1, "Command has failed.\n" );
-        return 1;
-    }
-    // replace the current network
-    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
-*/
-
-//    if ( Cut_CellIsRunning() )
-//        Cut_CellDumpToFile();
-//    else
-//        Cut_CellPrecompute();
-//        Cut_CellLoad();
-/*
-        {
-            Abc_Ntk_t * pNtkRes;
-            extern Abc_Ntk_t * Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels );
-            pNtkRes = Abc_NtkTopmost( pNtk, nLevels );
-            Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
-        }
-*/
-//    Abc_NtkSimulteBuggyMiter( pNtk );
-
-//    Rwr_Temp();
-//    Abc_MvExperiment();
-//    Ivy_TruthTest();
-
-
-//    Ivy_TruthEstimateNodesTest();
-/*
-    pNtkRes = Abc_NtkIvy( pNtk );
-//    pNtkRes = Abc_NtkPlayer( pNtk, nLevels, 0 );
-//    pNtkRes = NULL;
-    if ( pNtkRes == NULL )
-    {
-        Abc_Print( -1, "Command has failed.\n" );
-        return 1;
-    }
-    // replace the current network
-    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
-*/
-//    Abc_NtkMaxFlowTest( pNtk );
-//    Pr_ManProofTest( "trace.cnf" );
-
-//    Abc_NtkCompareSupports( pNtk );
-//    Abc_NtkCompareCones( pNtk );
-/*
-    {
-        extern Vec_Vec_t * Abc_NtkPartitionSmart( Abc_Ntk_t * pNtk, int fVerbose );
-        Vec_Vec_t * vParts;
-        vParts = Abc_NtkPartitionSmart( pNtk, 1 );
-        Vec_VecFree( vParts );
-    }
-*/
-//    Abc_Ntk4VarTable( pNtk );
-//    Dar_NtkGenerateArrays( pNtk );
-//    Dar_ManDeriveCnfTest2();
 /*
     if ( !Abc_NtkIsStrash(pNtk) )
     {
@@ -8602,150 +8508,37 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 */
 /*
-    if ( !Abc_NtkIsStrash(pNtk) )
-    {
-        Abc_Print( -1, "Currently only works for structurally hashed circuits.\n" );
-        return 0;
-    }
-*/
-/*
-    if ( Abc_NtkIsStrash(pNtk) )
-    {
-        Abc_Print( -1, "Currently only works for logic circuits.\n" );
-        return 0;
-    }
-*/
-
-
-/*
-//    pNtkRes = Abc_NtkDar( pNtk );
-//    pNtkRes = Abc_NtkDarRetime( pNtk, nLevels, 1 ); 
-//    pNtkRes = Abc_NtkPcmTestAig( pNtk, fVerbose );
-    pNtkRes = Abc_NtkPcmTest( pNtk, fVerbose );
-//    pNtkRes = NULL;
-    if ( pNtkRes == NULL )
-    {
-        Abc_Print( -1, "Command has failed.\n" );
-        return 1;
-    }
-    // replace the current network
-    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
-    return 0;
-*/
-
-
-//    Abc_NtkDarClau( pNtk, nFrames, nLevels, fBmc, fVerbose, fVeryVerbose );
-/*
-    if ( globalUtilOptind != 1 )
-    {
-        Abc_Print( -1, "Command has failed.\n" );
-        return 1;
-    }
-    Abc_NtkDarTestBlif( argv[globalUtilOptind] );
-*/
-
-//    Abc_NtkDarPartition( pNtk );
-//Abc_NtkDarTest( pNtk );
-//Abc_NtkWriteAig( pNtk, NULL );
-
-
-/*
-//    pNtkRes = Abc_NtkDarRetimeStep( pNtk, 0 );
-    pNtkRes = Abc_NtkDarHaigRecord( pNtk, 3, 3000, 0, 0, 0, 0 );
-    if ( pNtkRes == NULL )
-    {
-        Abc_Print( -1, "Command has failed.\n" );
-        return 1;
-    }
-    // replace the current network
-    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
-*/
-
-/*
-    pNtkRes = Abc_NtkDarTestNtk( pNtk );
-    if ( pNtkRes == NULL )
-    {
-        Abc_Print( -1, "Command has failed.\n" );
-        return 1;
-    }
-    // replace the current network
-    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
-*/
-
-//Amap_LibertyTest( "bwrc.lib" );
-
-//    Abc_NtkDarTest( pNtk );
-
-//    Bbl_ManTest( pNtk );
-/*
+    if ( pNtk )
     {
-    extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
-    extern void Aig_ManComputeDomsForCofactoring( Aig_Man_t * p );
-    Aig_Man_t * pAig;
-    pAig = Abc_NtkToDar( pNtk, 0, 0 );
-    Aig_ManComputeDomsForCofactoring( pAig );
-    Aig_ManStop( pAig );
+        extern Abc_Ntk_t * Au_ManPerformTest( Abc_Ntk_t * p, int nCutMax, int nLeafMax, int nDivMax, int nDecMax, int fVerbose, int fVeryVerbose );
+        Abc_Ntk_t * pNtkRes = Au_ManPerformTest( pNtk, nCutMax, nLeafMax, nDivMax, nDecMax, fVerbose, fVeryVerbose );
+        if ( pNtkRes == NULL )
+        {
+            Abc_Print( -1, "Command has failed.\n" );
+            return 1;
+        }
+        Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
     }
 */
-
 /*
-    if ( Abc_NtkIsStrash(pNtk) )
     {
-        extern Abc_Ntk_t * Au_ManTransformTest( Abc_Ntk_t * pAig );
-        pNtkRes = Au_ManTransformTest( pNtk );
-    }
-    else
-    {
-        extern Abc_Ntk_t * Au_ManResubTest( Abc_Ntk_t * pAig );
-        pNtkRes = Au_ManResubTest( pNtk );
-    }
-    if ( pNtkRes == NULL )
-    {
-        Abc_Print( -1, "Command has failed.\n" );
-        return 1;
+        extern void Aig_ManTerSimulate( Aig_Man_t * pAig );
+        extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
+        Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 0 );
+        Aig_ManTerSimulate( pAig );
+        Aig_ManStop( pAig );
     }
-    // replace the current network
-    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
-*/
-
-/*
-{
-    extern int Au_DsdVecTest( int nVars );
-    Au_DsdVecTest( 6 );
-}
 */
-
-{
-//    extern void Au_Sat3DeriveImpls();
-//    Au_Sat3DeriveImpls();
-//    extern void Au_Sat3DeriveJusts();
-//    Au_Sat3DeriveJusts();
-}
-
-{
-//    extern void Au_NtkReadFour( Abc_Ntk_t * pNtk );
-//    extern void Au_Data4VerifyFour();
-//    Au_NtkReadFour( pNtk );
-//    Au_Data4VerifyFour();
-}
-
-
-//    Abc_NtkCheckAbsorb( pNtk, 4 );
-/*
-    if ( fBmc )
-        Abc_NktMffcServerTest( pNtk );
-    else
-        Abc_ResPartitionTest( pNtk );
-*/
-//    Abc_NtkHelloWorld( pNtk );
-//    Abc_NktMffcTest( pNtk );
-//    Abc_NktMffcServerTest( pNtk );
     return 0;
 usage:
-    Abc_Print( -2, "usage: test [-h] <file_name>\n" );
+    Abc_Print( -2, "usage: test [-CKDN] [-vwh] <file_name>\n" );
     Abc_Print( -2, "\t         testbench for new procedures\n" );
-//    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
-//    Abc_Print( -2, "\t-w     : toggle printing very verbose information [default = %s]\n", fVeryVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-C num : the max number of cuts [default = %d]\n", nCutMax );
+    Abc_Print( -2, "\t-K num : the max number of leaves [default = %d]\n", nLeafMax );
+    Abc_Print( -2, "\t-D num : the max number of divisors [default = %d]\n", nDivMax );
+    Abc_Print( -2, "\t-N num : the max number of node inputs [default = %d]\n", nDecMax );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-w     : toggle printing very verbose information [default = %s]\n", fVeryVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
 }