Changes to several APIs.

4 files changed, 92 insertions, 16 deletions

diff --git a/src/aig/gia/giaSim4.c b/src/aig/gia/giaSim4.c
index 04352761..610bb098 100644
--- a/src/aig/gia/giaSim4.c
+++ b/src/aig/gia/giaSim4.c
@@ -41,7 +41,7 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-int Gia_Sim4Try( char * pFileName0, char * pFileName1, char * pFileName2, int nWords, int fOrder, int fVerbose )
+int Gia_Sim4Try( char * pFileName0, char * pFileName1, char * pFileName2, int nWords, int nBeam, int LevL, int LevU, int fOrder, int fFancy, int fVerbose )
 {
     return 0;
 }
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 17741905..37bdc7ec 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -7128,11 +7128,11 @@ usage:
 ***********************************************************************/
 int Abc_CommandRunSim( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern void Acb_NtkRunSim( char * pFileName[4], int nWords, int fOrder, int fVerbose );
+    extern void Acb_NtkRunSim( char * pFileName[4], int nWords, int nBeam, int LevL, int LevU, int fOrder, int fFancy, int fVerbose );
     char * pFileNames[4] = {NULL, NULL, "out.v", NULL};
-    int c, fOrder = 0, nWords = 1, fVerbose = 0;
+    int c, nWords = 4, nBeam = 4, LevL = 0, LevU = 0, fOrder = 0, fFancy = 0, fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Wovh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "WBLUofvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -7147,9 +7147,45 @@ int Abc_CommandRunSim( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nWords < 0 )
                 goto usage;
             break;
+        case 'B':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-B\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nBeam = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nBeam < 0 )
+                goto usage;
+            break;
+        case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            LevL = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( LevL < 0 )
+                goto usage;
+            break;
+        case 'U':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-U\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            LevU = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( LevU < 0 )
+                goto usage;
+            break;
         case 'o':
             fOrder ^= 1;
             break;
+        case 'f':
+            fFancy ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -7167,15 +7203,19 @@ int Abc_CommandRunSim( Abc_Frame_t * pAbc, int argc, char ** argv )
     Gia_ManRandom(1);
     for ( c = 0; c < argc - globalUtilOptind; c++ )
         pFileNames[c] = argv[globalUtilOptind+c];
-    Acb_NtkRunSim( pFileNames, nWords, fOrder, fVerbose );
+    Acb_NtkRunSim( pFileNames, nWords, nBeam, LevL, LevU, fOrder, fFancy, fVerbose );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: runsim [-W] [-ovh] [-N <num>] <file1> <file2> <file3>\n" );
+    Abc_Print( -2, "usage: runsim [-WBLU] [-ofvh] [-N <num>] <file1> <file2> <file3>\n" );
     Abc_Print( -2, "\t           experimental simulation command\n" );
     Abc_Print( -2, "\t-W <num> : the number of words of simulation info [default = %d]\n", nWords );
+    Abc_Print( -2, "\t-B <num> : the beam width parameter [default = %d]\n", nBeam );
+    Abc_Print( -2, "\t-L <num> : the lower bound on level [default = %d]\n", LevL );
+    Abc_Print( -2, "\t-U <num> : the upper bound on level [default = %d]\n", LevU );
     Abc_Print( -2, "\t-o       : toggle using a different node ordering [default = %s]\n", fOrder? "yes": "no" );
-    Abc_Print( -2, "\t-v       : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-f       : toggle using experimental feature [default = %s]\n",      fFancy? "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;
 }
diff --git a/src/base/acb/acbFunc.c b/src/base/acb/acbFunc.c
index 1708e51d..6ffeb0e8 100644
--- a/src/base/acb/acbFunc.c
+++ b/src/base/acb/acbFunc.c
@@ -888,6 +888,12 @@ Vec_Int_t * Acb_FindSupportStart( sat_solver * pSat, int iFirstDiv, Vec_Int_t *
             //printf( "Selecting divisor %d with weight %d\n", i, Vec_IntEntry(vWeights, i) );
             fFound = 1;
         }
+        if ( fFound == 0 )
+        {
+            Vec_WrdFree( vPats );
+            Vec_IntFree( vSupp );
+            return NULL;
+        }
         assert( fFound );
         iPat++;
     }
@@ -1102,7 +1108,10 @@ Vec_Int_t * Acb_FindSupport( sat_solver * pSat, int iFirstDiv, Vec_Int_t * vWeig
         else
             vSupp = Acb_FindSupportNext( pSat, iFirstDiv, vWeights, vPats, &nPats );
         if ( vSupp == NULL )
-            break;
+        {
+            Vec_IntFree( vSuppBest );
+            return NULL;
+        }
         //vSupp = Acb_FindSupportMin( pSat, iFirstDiv, vPats, &nPats, vTemp = vSupp );
         //Vec_IntFree( vTemp );
         if ( vSupp == NULL )
@@ -1241,6 +1250,7 @@ Vec_Int_t * Acb_DerivePatchSupport( Cnf_Dat_t * pCnf, int iTar, int nTargets, in
             // find minimum subset
             if ( fUseMinAssump )
             {
+                int fUseSuppMin = 1;
                 // solve in a standard way
                 abctime clk = Abc_Clock();
                 nSuppNew = sat_solver_minimize_assumptions( pSat, Vec_IntArray(vSupp), Vec_IntSize(vSupp), 0 );
@@ -1250,20 +1260,25 @@ Vec_Int_t * Acb_DerivePatchSupport( Cnf_Dat_t * pCnf, int iTar, int nTargets, in
                 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
 
                 // perform minimization
-                if ( Vec_IntSize(vSupp) > 0 )
+                if ( fUseSuppMin && Vec_IntSize(vSupp) > 0 )
                 {
                     abctime clk = Abc_Clock();
+                    Vec_Int_t * vSupp2 = Vec_IntDup( vSupp );
                     Vec_Int_t * vTemp, * vWeights = Acb_DeriveWeights( vDivs, pNtkF );
                     vSupp = Acb_FindSupport( pSat, iDivVar, vWeights, vTemp = vSupp, TimeOut );
                     Vec_IntFree( vWeights );
                     Vec_IntFree( vTemp );
                     if ( vSupp == NULL )
                     {
-                        printf( "Support minimization timed out after %d sec.\n", TimeOut );
-                        sat_solver_delete( pSat );
-                        return NULL;
+                        printf( "Support minimization did not succeed.  " );
+                        //sat_solver_delete( pSat );
+                        vSupp = vSupp2;
+                    }
+                    else
+                    {
+                        Vec_IntFree( vSupp2 );
+                        printf( "Minimized support to %d supp vars.  ", Vec_IntSize(vSupp) );
                     }
-                    printf( "Minimized support to %d supp vars.  ", Vec_IntSize(vSupp) );
                     Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
                 }
             }
@@ -1504,6 +1519,17 @@ char * Acb_EnumerateSatAssigns( sat_solver * pSat, int PivotVar, int FreeVar, Ve
     {
         if ( iMint == 1000 )
         {
+            //if ( Vec_IntSize(vDivVars) == 0 )
+            {
+                printf( "Assuming constant 0 function.\n" );
+                Vec_StrClear( vTempSop );
+                Vec_StrPush( vTempSop, ' ' );
+                Vec_StrPush( vTempSop, '0' );
+                Vec_StrPush( vTempSop, '\n' );
+                Vec_StrPush( vTempSop, '\0' );
+                return Vec_StrReleaseArray(vTempSop);
+            }
+
             printf( "Reached the limit on the number of cubes (1000).\n" );
             Vec_IntFree( vTemp );
             Vec_IntFree( vLits );
@@ -2039,7 +2065,17 @@ Cnf_Dat_t * Acb_NtkDeriveMiterCnf( Gia_Man_t * p, int iTar, int nTars, int fVerb
     Cnf_Dat_t * pCnf; int v;
     for ( v = 0; v < iTar; v++ )
     {
+        Gia_Man_t * pTemp;
         pCof = Gia_ManDupUniv( p = pCof, Gia_ManCiNum(pCof) - nTars + v );
+        //pCof = Acb_NtkEcoSynthesize( pTemp = pCof );
+        //pCof = Gia_ManCompress2( pTemp = pCof, 1, 0 );
+        pCof = Gia_ManAigSyn2( pTemp = pCof, 0, 1, 0, 100, 0, 0, 0 );
+        Gia_ManStop( pTemp );
+        if ( Gia_ManAndNum(pCof) > 10000 )
+        {
+            printf( "Quantifying target %3d ", v );
+            Gia_ManPrintStats( pCof, NULL );
+        }
         assert( Gia_ManCiNum(pCof) == Gia_ManCiNum(p) );
         Gia_ManStop( p );
     }
diff --git a/src/base/acb/acbUtil.c b/src/base/acb/acbUtil.c
index 89163770..11ff6163 100644
--- a/src/base/acb/acbUtil.c
+++ b/src/base/acb/acbUtil.c
@@ -764,12 +764,12 @@ void Acb_NtkInsert( char * pFileNameIn, char * pFileNameOut, Vec_Ptr_t * vNames
   SeeAlso     []
 
 ***********************************************************************/
-void Acb_NtkRunSim( char * pFileName[4], int nWords, int fOrder, int fVerbose )
+void Acb_NtkRunSim( char * pFileName[4], int nWords, int nBeam, int LevL, int LevU, int fOrder, int fFancy, int fVerbose )
 {
-    extern int Gia_Sim4Try( char * pFileName0, char * pFileName1, char * pFileName2, int nWords, int fOrder, int fVerbose );
+    extern int Gia_Sim4Try( char * pFileName0, char * pFileName1, char * pFileName2, int nWords, int nBeam, int LevL, int LevU, int fOrder, int fFancy, int fVerbose );
     extern void Acb_NtkRunEco( char * pFileNames[4], int fCheck, int fVerbose );
     char * pFileNames[4] = { pFileName[2], pFileName[1], NULL, pFileName[2] };
-    if ( Gia_Sim4Try( pFileName[0], pFileName[1], pFileName[2], nWords, fOrder, fVerbose ) )
+    if ( Gia_Sim4Try( pFileName[0], pFileName[1], pFileName[2], nWords, nBeam, LevL, LevU, fOrder, fFancy, fVerbose ) )
         Acb_NtkRunEco( pFileNames, 1, fVerbose );
 }