Version abc90714

committer: Baruch Sterin <baruchs@gmail.com>

4 files changed, 19 insertions, 4 deletions

diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c
index f6845acd..3da92fc0 100644
--- a/src/aig/saig/saigAbs.c
+++ b/src/aig/saig/saigAbs.c
@@ -24,6 +24,7 @@
 #include "satSolver.h"
 #include "satStore.h"
 #include "ssw.h"
+#include "ioa.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -681,7 +682,7 @@ Ssw_Cex_t * Saig_ManCexShrink( Aig_Man_t * p, Aig_Man_t * pAbs, Ssw_Cex_t * pCex
     }
     return pCex;
 }
-
+ 
 /**Function*************************************************************
 
   Synopsis    [Performs proof-based abstraction using BMC of the given depth.]
@@ -859,6 +860,7 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax,
         printf( "Refining abstraction...\n" );
         for ( Iter = 0; ; Iter++ )
         {
+            char FileName[100];
             pTemp = Saig_ManProofRefine( p, pResult, vFlops, nFramesBmc, nConfMaxBmc, fVerbose );
             if ( pTemp == NULL )
                 break;
@@ -869,9 +871,16 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax,
                 Aig_ManPrintStats( pResult );
             else
                 printf( " -----------------------------------------------------\n" );
+            // output the intermediate result of abstraction
+            sprintf( FileName, "gabs%02d.aig", Iter );
+            Ioa_WriteAiger( pResult, FileName, 0, 0 );
+            printf( "Intermediate abstracted model was written into file \"%s\".\n", FileName );
+            // check if the ratio is reached
             if ( 100.0*(Aig_ManRegNum(p)-Aig_ManRegNum(pTemp))/Aig_ManRegNum(p) < 1.0*nRatio )
             {
                 printf( "Refinements is stopped because flop reduction is less than %d%%\n", nRatio );
+                Aig_ManStop( pResult );
+                pResult = NULL;
                 break;
             }
         }
diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c
index d56d97a9..57759594 100644
--- a/src/aig/saig/saigBmc.c
+++ b/src/aig/saig/saigBmc.c
@@ -87,7 +87,7 @@ Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nFramesMax, int nNodesMax,
     Saig_Bmc_t * p;
     Aig_Obj_t * pObj;
     int i, Lit;
-    assert( Aig_ManRegNum(pAig) > 0 );
+//    assert( Aig_ManRegNum(pAig) > 0 );
     p = (Saig_Bmc_t *)ABC_ALLOC( char, sizeof(Saig_Bmc_t) );
     memset( p, 0, sizeof(Saig_Bmc_t) );
     // set parameters
@@ -589,7 +589,7 @@ void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConf
             Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
         printf( "Params: FramesMax = %d. NodesDelta = %d. ConfMaxOne = %d. ConfMaxAll = %d.\n", 
             nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll );
-    }
+    } 
     for ( Iter = 0; ; Iter++ )
     {
         clk2 = clock();
diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c
index f8799e38..240168e6 100644
--- a/src/aig/saig/saigBmc2.c
+++ b/src/aig/saig/saigBmc2.c
@@ -162,6 +162,8 @@ Aig_Man_t * Saig_ManFramesBmcLimit( Aig_Man_t * pAig, int nFrames, int nSizeMax
     return pFrames;
 }
 
+#include "utilMem.h"
+
 /**Function*************************************************************
 
   Synopsis    [Performs BMC for the given AIG.]
@@ -228,6 +230,8 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
     // create the SAT solver
     clk = clock();
     pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) );  
+//if ( s_fInterrupt )
+//return -1;
     pSat = sat_solver_new();
     sat_solver_setnvars( pSat, pCnf->nVars );
     for ( i = 0; i < pCnf->nClauses; i++ )
@@ -255,6 +259,8 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
         int clkPart = clock();
         Aig_ManForEachPo( pFrames, pObj, i )
         {
+//if ( s_fInterrupt )
+//return -1;
             Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
             if ( fVerbose )
             {
diff --git a/src/aig/saig/saigSimExt.c b/src/aig/saig/saigSimExt.c
index ead0ece5..97b91b1d 100644
--- a/src/aig/saig/saigSimExt.c
+++ b/src/aig/saig/saigSimExt.c
@@ -251,7 +251,7 @@ Vec_Int_t * Saig_ManExtendCounterExample( Aig_Man_t * p, int iFirstPi, Ssw_Cex_t
 {
     Vec_Int_t * vRes, * vResInv, * vUndo, * vVis, * vVis2;
     int i, f, Value;
-    assert( Aig_ManRegNum(p) > 0 );
+//    assert( Aig_ManRegNum(p) > 0 );
     assert( (unsigned *)Vec_PtrEntry(vSimInfo,1) - (unsigned *)Vec_PtrEntry(vSimInfo,0) >= Aig_BitWordNum(2*(pCex->iFrame+1)) );
     // start simulation data
     Value = Saig_ManSimDataInit( p, pCex, vSimInfo, NULL );