Version abc90215

1 files changed, 117 insertions, 117 deletions

diff --git a/src/aig/cec/cecCore.c b/src/aig/cec/cecCore.c
index 86287a96..ab8fd5cf 100644
--- a/src/aig/cec/cecCore.c
+++ b/src/aig/cec/cecCore.c
@@ -37,20 +37,20 @@
   SideEffects []
 
   SeeAlso     []
-
+ 
 ***********************************************************************/
 void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p )
 {
     memset( p, 0, sizeof(Cec_ParSat_t) );
-    p->nBTLimit       =   100;  // conflict limit at a node
-    p->nSatVarMax     =  2000;  // the max number of SAT variables
-    p->nCallsRecycle  =    10;  // calls to perform before recycling SAT solver
-    p->fFirstStop     =     0;  // stop on the first sat output
-    p->fPolarFlip     =     0;  // uses polarity adjustment
-    p->fVerbose       =     0;  // verbose stats
-}
-
-/**Function*************************************************************
+    p->nBTLimit       =      10;  // conflict limit at a node
+    p->nSatVarMax     =    2000;  // the max number of SAT variables
+    p->nCallsRecycle  =     100;  // calls to perform before recycling SAT solver
+    p->fPolarFlip     =       1;  // flops polarity of variables
+    p->fFirstStop     =       0;  // stop on the first sat output
+    p->fVerbose       =       1;  // verbose stats
+}  
+  
+/**Function************  *************************************************
 
   Synopsis    [This procedure sets default parameters.]
 
@@ -64,12 +64,19 @@ void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p )
 void Cec_ManCswSetDefaultParams( Cec_ParCsw_t * p )
 {
     memset( p, 0, sizeof(Cec_ParCsw_t) );
-    p->nWords         =    15;  // the number of simulation words
-    p->nRounds        =    10;  // the number of simulation rounds
-    p->nBTlimit       =    10;  // conflict limit at a node
-    p->fRewriting     =     0;  // enables AIG rewriting
-    p->fVerbose       =     1;  // verbose stats
-}
+    p->nWords         =      20;  // the number of simulation words
+    p->nRounds        =      20;  // the number of simulation rounds
+    p->nItersMax      =      20;  // the maximum number of iterations of SAT sweeping
+    p->nBTLimit       =   10000;  // conflict limit at a node
+    p->nSatVarMax     =    2000;  // the max number of SAT variables
+    p->nCallsRecycle  =     100;  // calls to perform before recycling SAT solver
+    p->nLevelMax      =       0;  // restriction on the level of nodes to be swept
+    p->nDepthMax      =       1;  // the depth in terms of steps of speculative reduction
+    p->fRewriting     =       0;  // enables AIG rewriting
+    p->fFirstStop     =       0;  // stop on the first sat output
+    p->fVeryVerbose   =       0;  // verbose stats
+    p->fVerbose       =       0;  // verbose stats
+} 
 
 /**Function*************************************************************
 
@@ -85,20 +92,19 @@ void Cec_ManCswSetDefaultParams( Cec_ParCsw_t * p )
 void Cec_ManCecSetDefaultParams( Cec_ParCec_t * p )
 {
     memset( p, 0, sizeof(Cec_ParCec_t) );
-    p->nIters         =     5;  // iterations of SAT solving/sweeping
-    p->nBTLimitBeg    =     2;  // starting backtrack limit
-    p->nBTlimitMulti  =     8;  // multiple of backtrack limiter
-    p->fUseSmartCnf   =     0;  // use smart CNF computation
-    p->fRewriting     =     0;  // enables AIG rewriting
-    p->fSatSweeping   =     0;  // enables SAT sweeping
-    p->fFirstStop     =     0;  // stop on the first sat output
-    p->fVerbose       =     1;  // verbose stats
-}
-
+    p->nIters         =       1;  // iterations of SAT solving/sweeping
+    p->nBTLimitBeg    =       2;  // starting backtrack limit
+    p->nBTlimitMulti  =       8;  // multiple of backtrack limiter
+    p->fUseSmartCnf   =       0;  // use smart CNF computation
+    p->fRewriting     =       0;  // enables AIG rewriting
+    p->fSatSweeping   =       0;  // enables SAT sweeping
+    p->fFirstStop     =       0;  // stop on the first sat output
+    p->fVerbose       =       1;  // verbose stats
+}  
 
 /**Function*************************************************************
 
-  Synopsis    [Performs equivalence checking.]
+  Synopsis    [Core procedure for SAT sweeping.]
 
   Description []
                
@@ -107,39 +113,21 @@ void Cec_ManCecSetDefaultParams( Cec_ParCec_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Cec_Sweep( Aig_Man_t * pAig, int nBTLimit )
+Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars )
 {
-    Cec_MtrStatus_t Status;
-    Cec_ParCsw_t ParsCsw, * pParsCsw = &ParsCsw;
-    Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
-    Caig_Man_t * pCaig;
-    Aig_Man_t * pSRAig;
-    int clk;
-
-    Cec_ManCswSetDefaultParams( pParsCsw );
-    pParsCsw->nBTlimit = nBTLimit;
-    pCaig = Caig_ManClassesPrepare( pAig, pParsCsw->nWords, pParsCsw->nRounds );
-
-    pSRAig = Caig_ManSpecReduce( pCaig );
-    Aig_ManPrintStats( pSRAig );
-
-    Cec_ManSatSetDefaultParams( pParsSat );
-    pParsSat->fFirstStop = 0;
-    pParsSat->nBTLimit = pParsCsw->nBTlimit;
-clk = clock();
-    Status = Cec_SatSolveOutputs( pSRAig, pParsSat );
-    Cec_MiterStatusPrint( Status, "SRM   ", clock() - clk );
-
-    Aig_ManStop( pSRAig );
-
-    Caig_ManDelete( pCaig );
-
-    return 1;
+    Gia_Man_t * pNew;
+    Cec_ManPat_t * pPat;
+    pPat = Cec_ManPatStart();
+    Cec_ManSatSolve( pPat, pAig, pPars );
+    pNew = Gia_ManDupDfsSkip( pAig );
+    Cec_ManPatStop( pPat );
+    return pNew;
 }
 
+
 /**Function*************************************************************
 
-  Synopsis    [Performs equivalence checking.]
+  Synopsis    [Core procedure for SAT sweeping.]
 
   Description []
                
@@ -148,82 +136,94 @@ clk = clock();
   SeeAlso     []
 
 ***********************************************************************/
-int Cec_Solve( Aig_Man_t * pAig0, Aig_Man_t * pAig1, Cec_ParCec_t * pPars )
+Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParCsw_t * pPars )
 {
     Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
-    Cec_MtrStatus_t Status;
-    Aig_Man_t * pMiter;
-    int i, clk = clock();
-    if ( pPars->fVerbose )
-    {
-        Status = Cec_MiterStatusTrivial( pAig0 );
-        Status.nNodes += pAig1? Aig_ManNodeNum( pAig1 ) : 0;
-        Cec_MiterStatusPrint( Status, "Init  ", 0 );
-    }
-    // create combinational miter
-    if ( pAig1 == NULL )
+    Gia_Man_t * pNew;
+    Cec_ManCsw_t * p;
+    Cec_ManPat_t * pPat;
+    int i, RetValue, clk, clk2, clkTotal = clock();
+    Aig_ManRandom( 1 );
+    Gia_ManSetPhase( pAig );
+    Gia_ManCleanMark0( pAig );
+    Gia_ManCleanMark1( pAig );
+    p = Cec_ManCswStart( pAig, pPars );
+clk = clock();
+    RetValue = Cec_ManCswClassesPrepare( p );
+p->timeSim += clock() - clk;
+    Cec_ManSatSetDefaultParams( pParsSat );
+    pParsSat->nBTLimit = pPars->nBTLimit;
+    pParsSat->fVerbose = pPars->fVeryVerbose;
+    pPat = Cec_ManPatStart();
+    pPat->fVerbose = pPars->fVeryVerbose;
+    for ( i = 1; i <= pPars->nItersMax; i++ )
     {
-        Status = Cec_MiterStatus( pAig0 );
-        if ( Status.nSat > 0 && pPars->fFirstStop )
+        clk2 = clock();
+        pNew = Cec_ManCswSpecReduction( p ); 
+        if ( pPars->fVeryVerbose )
         {
-            if ( pPars->fVerbose )
-            printf( "Output %d is trivially SAT.\n", Status.iOut );
-            return 0;
+            Gia_ManPrintStats( p->pAig );
+            Gia_ManPrintStats( pNew );
         }
-        if ( Status.nUndec == 0 )
+        if ( Gia_ManCoNum(pNew) == 0 )
         {
-            if ( pPars->fVerbose )
-            printf( "The miter has no undecided outputs.\n" );
-            return 1;
+            Gia_ManStop( pNew );
+            break;
         }
-        pMiter = Cec_Duplicate( pAig0 );
-    }
-    else
-    {
-        pMiter = Cec_DeriveMiter( pAig0, pAig1 );
-        Status = Cec_MiterStatus( pMiter );
-        if ( Status.nSat > 0 && pPars->fFirstStop )
+clk = clock();
+        Cec_ManSatSolve( pPat, pNew, pParsSat ); 
+p->timeSat += clock() - clk;
+clk = clock();
+        Cec_ManCswClassesUpdate( p, pPat, pNew );
+p->timeSim += clock() - clk;
+        Gia_ManStop( pNew );
+        pNew = Cec_ManCswDupWithClasses( p );
+        Gia_WriteAiger( pNew, "gia_temp_new.aig", 0, 1 );
+        if ( p->pPars->fVerbose )
         {
-            if ( pPars->fVerbose )
-            printf( "Output %d is trivially SAT.\n", Status.iOut );
-            Aig_ManStop( pMiter );
-            return 0;
+            printf( "%3d : P =%7d. D =%7d. F =%6d. Lit =%8d. And =%8d. ", 
+                i, p->nAllProved, p->nAllDisproved, p->nAllFailed,  
+                Cec_ManCswCountLitsAll(p), Gia_ManAndNum(pNew) );
+            ABC_PRT( "Time", clock() - clk2 );
         }
-        if ( Status.nUndec == 0 )
+        if ( p->pPars->fVeryVerbose )
         {
-            if ( pPars->fVerbose )
-            printf( "The problem is solved by structrual hashing.\n" );
-            Aig_ManStop( pMiter );
-            return 1;
+            ABC_PRTP( "Sim ", p->timeSim, clock() - clkTotal );
+            ABC_PRTP( "Sat ", p->timeSat, clock() - clkTotal );
+            ABC_PRT( "Time", clock() - clkTotal );
+            printf( "****** Intermedate result %3d ******\n", i );
+            Gia_ManPrintStats( p->pAig );
+            Gia_ManPrintStats( pNew );
+            printf("The result is written into file \"%s\".\n", "gia_temp.aig" );
+            printf( "************************************\n" );
         }
-    }
-    if ( pPars->fVerbose )
-        Cec_MiterStatusPrint( Status, "Strash", clock() - clk );
-    // start parameter structures
-    Cec_ManSatSetDefaultParams( pParsSat );
-    pParsSat->fFirstStop = pPars->fFirstStop;
-    pParsSat->nBTLimit = pPars->nBTLimitBeg;
-    for ( i = 0; i < pPars->nIters; i++ )
-    {
-        // try SAT solving
-        clk = clock();
-        pParsSat->nBTLimit *= pPars->nBTlimitMulti;
-        Status = Cec_SatSolveOutputs( pMiter, pParsSat );
-        if ( pPars->fVerbose )
-            Cec_MiterStatusPrint( Status, "SAT   ", clock() - clk );
-        if ( Status.nSat && pParsSat->fFirstStop )
-            break;
-        if ( Status.nUndec == 0 )
+        if ( Gia_ManAndNum(pNew) == 0 )
+        {
+            Gia_ManStop( pNew );
             break;
+        }
+        Gia_ManStop( pNew );
+    }
+    Gia_ManCleanMark0( pAig );
+    Gia_ManCleanMark1( pAig );
 
-        // try rewriting
-
-        // try SAT sweeping
-        Cec_Sweep( pMiter, 10 );
-        i = i;
+    // verify the result
+    if ( p->pPars->fVerbose )
+    {
+        printf( "Verifying the result:\n" );
+        pNew = Cec_ManCswSpecReductionProved( p );
+        pParsSat->nBTLimit = 1000000;
+        pParsSat->fVerbose = 1;
+        Cec_ManSatSolve( NULL, pNew, pParsSat ); 
+        Gia_ManStop( pNew );
     }
-    Aig_ManStop( pMiter );
-    return 1;
+
+    // create the resulting miter
+    pAig->pReprs = Cec_ManCswDeriveReprs( p );
+    pNew = Gia_ManDupDfsClasses( pAig );
+    Cec_ManCswStop( p );
+    Cec_ManPatStop( pPat );
+    return pNew;
 }
 
 ////////////////////////////////////////////////////////////////////////