Exact synthesis.

src/base/abci/abc.c

@@ -7295,7 +7295,7 @@ int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern Gia_Man_t * Gia_ManFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrivalTimes, int nBTLimit, int nStartGates, int fVerbose );
 
-    int c, nMaxDepth = -1, fMakeAIG = 0, fTest = 0, fVerbose = 0, nVars = 0, nVarsTmp, nFunc = 0, nStartGates = 1, nBTLimit = 100;
+    int c, nMaxDepth = -1, fMakeAIG = 0, fTest = 0, fVerbose = 0, nVars = 0, nVarsTmp, nFunc = 0, nStartGates = 1, nBTLimit = 400000;
     char * p1, * p2;
     word pTruth[64];
     int pArrTimeProfile[8], fHasArrTimeProfile = 0;
@@ -7423,7 +7423,7 @@ int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv )
         if ( pGiaRes )
             Abc_FrameUpdateGia( pAbc, pGiaRes );
         else
-            Abc_Print( 0, "Could not find AIG within given resource constraints.\n" );
+            Abc_Print( 0, "Could not find AIG within given resource constraints, retry with different value for -C.\n" );
     }
     else
     {
@@ -7434,7 +7434,7 @@ int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv )
             Abc_FrameClearVerifStatus( pAbc );
         }
         else
-            Abc_Print( 0, "Could not find network within given resource constraints.\n" );
+            Abc_Print( 0, "Could not find network within given resource constraints, retry with different value for -C.\n" );
     }
     return 0;
 
@@ -7444,7 +7444,7 @@ usage:
     Abc_Print( -2, "\t-D <num>  : constrain maximum depth (if too low, algorithm may not terminate)\n" );
     Abc_Print( -2, "\t-A <list> : input arrival times (comma separated list)\n" );
     Abc_Print( -2, "\t-S <num>  : number of start gates in search [default = %s]\n", nStartGates );
-    Abc_Print( -2, "\t-C <num>  : the limit on the number of conflicts [default = %d]\n", nBTLimit );
+    Abc_Print( -2, "\t-C <num>  : the limit on the number of conflicts; turn off with 0 [default = %d]\n", nBTLimit );
     Abc_Print( -2, "\t-a        : toggle create AIG [default = %s]\n", fMakeAIG ? "yes" : "no" );
     Abc_Print( -2, "\t-t        : run test suite\n" );
     Abc_Print( -2, "\t-v        : toggle verbose printout [default = %s]\n", fVerbose ? "yes" : "no" );

src/base/abci/abcExact.c

@@ -2314,7 +2314,7 @@ static char * Ses_ManFindMinimumSizeTopDown( Ses_Man_t * pSes, int nMinGates )
 
 static char * Ses_ManFindMinimumSize( Ses_Man_t * pSes )
 {
-    char * pSol;
+    char * pSol = NULL;
 
     /* do the arrival times allow for a network? */
     if ( pSes->nMaxDepth != -1 && pSes->pArrTimeProfile )
@@ -2326,7 +2326,7 @@ static char * Ses_ManFindMinimumSize( Ses_Man_t * pSes )
 
     pSol = Ses_ManFindMinimumSizeBottomUp( pSes );
 
-    if ( !pSol && pSes->fHitResLimit && pSes->nGates != pSes->nMaxGates )
+    if ( !pSol && pSes->nMaxDepth != -1 && pSes->fHitResLimit && pSes->nGates != pSes->nMaxGates )
         return Ses_ManFindMinimumSizeTopDown( pSes, pSes->nGates + 1 );
     else
         return pSol;
@@ -2360,8 +2360,8 @@ Abc_Ntk_t * Abc_NtkFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth
 
     pSes = Ses_ManAlloc( pTruth, nVars, nFunc, nMaxDepth, pArrTimeProfile, 0, nBTLimit, fVerbose );
     pSes->nStartGates = nStartGates;
-    pSes->fReasonVerbose = 1;
-    pSes->fSatVerbose = 1;
+    pSes->fReasonVerbose = 0;
+    pSes->fSatVerbose = 0;
     if ( fVerbose )
         Ses_ManPrintFuncs( pSes );