1 files changed, 70 insertions, 3 deletions

diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c
index 4f2c8db..08571a3 100644
--- a/src/sat/bmc/bmcMaj.c
+++ b/src/sat/bmc/bmcMaj.c
@@ -500,6 +500,8 @@ Exa_Man_t * Exa_ManAlloc( Bmc_EsPar_t * pPars, word * pTruth )
     p->vInfo      = Exa_ManTruthTables( p );
     p->pSat       = bmcg_sat_solver_start();
     bmcg_sat_solver_set_nvars( p->pSat, p->iVar );
+    if ( pPars->RuntimeLim )
+        bmcg_sat_solver_set_runtime_limit( p->pSat, Abc_Clock() + pPars->RuntimeLim * CLOCKS_PER_SEC );
     return p;
 }
 void Exa_ManFree( Exa_Man_t * p )
@@ -572,6 +574,59 @@ static inline int Exa_ManEval( Exa_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+void Exa_ManDumpBlif( Exa_Man_t * p, int fCompl )
+{
+    char Buffer[1000];
+    char FileName[1000];
+    FILE * pFile;
+    int i, k, iVar;
+    if ( fCompl )
+        Abc_TtNot( p->pTruth, p->nWords );
+    Extra_PrintHexadecimalString( Buffer, (unsigned *)p->pTruth, p->nVars );
+    if ( fCompl )
+        Abc_TtNot( p->pTruth, p->nWords );
+    sprintf( FileName, "%s_%d_%d.blif", Buffer, 2, p->nNodes );
+    pFile = fopen( FileName, "wb" );
+    fprintf( pFile, "# Realization of the %d-input function %s using %d two-input gates:\n", p->nVars, Buffer, p->nNodes );
+    fprintf( pFile, ".model %s_%d_%d\n", Buffer, 2, p->nNodes );
+    fprintf( pFile, ".inputs" );
+    for ( i = 0; i < p->nVars; i++ )
+        fprintf( pFile, " %c", 'a'+i );
+    fprintf( pFile, "\n" );
+    fprintf( pFile, ".outputs F\n" );
+    for ( i = p->nObjs - 1; i >= p->nVars; i-- )
+    {
+        int iVarStart = 1 + 3*(i - p->nVars);
+        int Val1 = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart);
+        int Val2 = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart+1);
+        int Val3 = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart+2);
+
+        fprintf( pFile, ".names" );
+        for ( k = 1; k >= 0; k-- )
+        {
+            iVar = Exa_ManFindFanin( p, i, k );
+            if ( iVar >= 0 && iVar < p->nVars )
+                fprintf( pFile, " %c", 'a'+iVar );
+            else
+                fprintf( pFile, " %02d", iVar );
+        }
+        if ( i == p->nObjs - 1 )
+            fprintf( pFile, " F\n" );
+        else
+            fprintf( pFile, " %02d\n", i );
+        if ( i == p->nObjs - 1 && fCompl )
+            fprintf( pFile, "00 1\n" );
+        if ( (i == p->nObjs - 1 && fCompl) ^ Val1 )
+            fprintf( pFile, "01 1\n" );
+        if ( (i == p->nObjs - 1 && fCompl) ^ Val2 )
+            fprintf( pFile, "10 1\n" );
+        if ( (i == p->nObjs - 1 && fCompl) ^ Val3 )
+            fprintf( pFile, "11 1\n" );
+    }
+    fprintf( pFile, ".end\n\n" );
+    fclose( pFile );
+    printf( "Solution was dumped into file \"%s\".\n", FileName );
+}
 void Exa_ManPrintSolution( Exa_Man_t * p, int fCompl )
 {
     int i, k, iVar;
@@ -775,10 +830,18 @@ void Exa_ManExactSynthesis( Bmc_EsPar_t * pPars )
             printf( "The problem has no solution.\n" );
             break;
         }
+        if ( status == GLUCOSE_UNDEC )
+        {
+            printf( "The problem timed out after %d sec.\n", pPars->RuntimeLim );
+            break;
+        }
         iMint = Exa_ManEval( p );
     }
     if ( iMint == -1 )
+    {
         Exa_ManPrintSolution( p, fCompl );
+        Exa_ManDumpBlif( p, fCompl );
+    }
     Exa_ManFree( p );
     Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
 }
@@ -915,6 +978,8 @@ static Exa3_Man_t * Exa3_ManAlloc( Bmc_EsPar_t * pPars, word * pTruth )
     p->vUsed3     = Vec_BitStart( (1 << p->pPars->nVars) * p->pPars->nNodes * p->nObjs * p->nObjs * p->nObjs );
     p->pSat       = bmcg_sat_solver_start();
     bmcg_sat_solver_set_nvars( p->pSat, p->iVar );
+    if ( pPars->RuntimeLim )
+        bmcg_sat_solver_set_runtime_limit( p->pSat, Abc_Clock() + pPars->RuntimeLim * CLOCKS_PER_SEC );
     return p;
 }
 static void Exa3_ManFree( Exa3_Man_t * p )
@@ -1267,15 +1332,17 @@ void Exa3_ManExactSynthesis( Bmc_EsPar_t * pPars )
         status = bmcg_sat_solver_solve( p->pSat, NULL, 0 );
         if ( pPars->fVerbose && (!pPars->fUseIncr || i % 100 == 0) )
             Exa3_ManPrint( p, i, iMint, Abc_Clock() - clkTotal );
-        if ( status == GLUCOSE_UNSAT )
+        if ( status == GLUCOSE_UNSAT || status == GLUCOSE_UNDEC )
             break;
         iMint = Exa3_ManEval( p );
     }
-    if ( pPars->fVerbose )
+    if ( pPars->fVerbose && status != GLUCOSE_UNDEC )
         Exa3_ManPrint( p, i, iMint, Abc_Clock() - clkTotal );
     if ( iMint == -1 )
         Exa3_ManPrintSolution( p, fCompl );
-    else
+    else if ( status == GLUCOSE_UNDEC )
+        printf( "The problem timed out after %d sec.\n", pPars->RuntimeLim );
+    else 
         printf( "The problem has no solution.\n" );
     printf( "Added = %d.  Tried = %d.  ", p->nUsed[1], p->nUsed[0] );
     Exa3_ManFree( p );