Exact synthesis minimization.

1 files changed, 121 insertions, 4 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index d49db050..e4e78d08 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -136,6 +136,8 @@ static int Abc_CommandExtract                ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandVarMin                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDetect                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandExact                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandBmsStart               ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandBmsPs                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandLogic                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandComb                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -777,6 +779,9 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Synthesis",    "detect",        Abc_CommandDetect,           0 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "exact",         Abc_CommandExact,            1 );
 
+    Cmd_CommandAdd( pAbc, "Exact synthesis", "bms_start",  Abc_CommandBmsStart,         0 );
+    Cmd_CommandAdd( pAbc, "Exact synthesis", "bms_ps",     Abc_CommandBmsPs,            0 );
+
     Cmd_CommandAdd( pAbc, "Various",      "logic",         Abc_CommandLogic,            1 );
     Cmd_CommandAdd( pAbc, "Various",      "comb",          Abc_CommandComb,             1 );
     Cmd_CommandAdd( pAbc, "Various",      "miter",         Abc_CommandMiter,            1 );
@@ -7407,6 +7412,118 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandBmsStart( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern int Abc_ExactIsRunning();
+    extern void Abc_ExactStart( int nBTLimit, int fVerbose );
+
+    int c, fVerbose = 0, nBTLimit = 10000;
+
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Cvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nBTLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( Abc_ExactIsRunning() )
+    {
+        Abc_Print( -1, "BMS manager is already started." );
+        return 1;
+    }
+
+    Abc_ExactStart( nBTLimit, fVerbose );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: bms_start [-C <num>] [-vh]\n" );
+    Abc_Print( -2, "\t           starts BMS manager for recording optimum networks\n" );
+    Abc_Print( -2, "\t-C <num> : the limit on the number of conflicts [default = %d]\n", nBTLimit );
+    Abc_Print( -2, "\t-v       : toggle verbose printout [default = %s]\n", fVerbose ? "yes" : "no" );
+    Abc_Print( -2, "\t-h       : print the command usage\n" );
+    Abc_Print( -2, "\t\n" );
+    Abc_Print( -2, "\t           This command was contributed by Mathias Soeken from EPFL in July 2016.\n" );
+    Abc_Print( -2, "\t           The author can be contacted as mathias.soeken at epfl.ch\n" );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandBmsPs( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern int Abc_ExactIsRunning();
+    extern void Abc_ExactStats();
+
+    int c;
+
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( !Abc_ExactIsRunning() )
+    {
+        Abc_Print( -1, "BMS manager is not started." );
+        return 1;
+    }
+
+    Abc_ExactStats();
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: bms_ps [-h]\n" );
+    Abc_Print( -2, "\t           shows statistics about BMS manager\n" );
+    Abc_Print( -2, "\t-h       : print the command usage\n" );
+    Abc_Print( -2, "\t\n" );
+    Abc_Print( -2, "\t           This command was contributed by Mathias Soeken from EPFL in July 2016.\n" );
+    Abc_Print( -2, "\t           The author can be contacted as mathias.soeken at epfl.ch\n" );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandLogic( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk, * pNtkRes;
@@ -16928,7 +17045,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
         }
         if ( Abc_NtkRecInputNum3() != pPars->nLutSize )
         {
-            printf( "The number of library inputs (%d) different from the K parameters (%d).\n", Abc_NtkRecInputNum3(), pPars->nLutSize );
+            printf( "The number of library inputs (%d) is different from the K parameters (%d).\n", Abc_NtkRecInputNum3(), pPars->nLutSize );
             return 0;
         }
     }
@@ -16937,12 +17054,12 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
     {
         if ( !Abc_ExactIsRunning() )
         {
-            printf( "LMS manager is not running (use \"rec_start3\").\n" );
+            printf( "BMS manager is not running (use \"bms_start\").\n" );
             return 0;
         }
-        if ( Abc_ExactInputNum() != pPars->nLutSize )
+        if ( Abc_ExactInputNum() < pPars->nLutSize )
         {
-            printf( "The number of library inputs (%d) different from the K parameters (%d).\n", Abc_ExactInputNum(), pPars->nLutSize );
+            printf( "The number of library inputs (%d) is smaller than the K parameters (%d).\n", Abc_ExactInputNum(), pPars->nLutSize );
             return 0;
         }
     }