Version abc90408

6 files changed, 12 insertions, 11 deletions

diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index f11345eb..5ddef829 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -90,7 +90,7 @@ static inline Aig_Obj_t *  Saig_ObjLiToLo( Aig_Man_t * p, Aig_Obj_t * pObj )  {
 ////////////////////////////////////////////////////////////////////////
 
 /*=== sswAbs.c ==========================================================*/
-extern Aig_Man_t *       Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int fVerbose );
+extern Aig_Man_t *       Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int fVerbose );
 /*=== saigBmc.c ==========================================================*/
 extern int               Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit );
 extern void              Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose );
diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c
index c9e76626..a2a915f7 100644
--- a/src/aig/saig/saigAbs.c
+++ b/src/aig/saig/saigAbs.c
@@ -693,15 +693,15 @@ Ssw_Cex_t * Saig_ManCexShrink( Aig_Man_t * p, Aig_Man_t * pAbs, Ssw_Cex_t * pCex
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlops, int fVerbose )
-{
+Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlops, int nFrames, int nConfMaxOne, int fVerbose )
+{ 
     extern void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose );
     extern Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstPi, void * pCex, int fVerbose );
 
     Vec_Int_t * vFlopsNew, * vPiToReg;
     Aig_Obj_t * pObj;
     int i, Entry, iFlop;
-    Saig_BmcPerform( pAbs, 2000, 2000, 5000, 1000000, fVerbose );
+    Saig_BmcPerform( pAbs, nFrames, 2000, nConfMaxOne, 1000000, fVerbose );
     if ( pAbs->pSeqModel == NULL )
         return NULL;
 //    Saig_ManExtendCounterExampleTest( p->pAig, 0, p->pAig->pSeqModel );
@@ -765,7 +765,7 @@ Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vF
   SeeAlso     []
  
 ***********************************************************************/
-Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int fVerbose )
+Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int fVerbose )
 {
     Aig_Man_t * pResult, * pTemp;
     Cnf_Dat_t * pCnf;
@@ -779,11 +779,12 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax,
 
     if ( fSkipProof )
     {
-        assert( 0 );
+//        assert( 0 );
         if ( fVerbose )
             printf( "Performing counter-example-based refinement.\n" );
 //        vFlops = Vec_IntStartNatural( 100 );
 //        Vec_IntPush( vFlops, 0 );
+        vFlops = Vec_IntStartNatural( 1 );
     }
     else
     {
@@ -858,7 +859,7 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax,
         printf( "Refining abstraction...\n" );
         for ( Iter = 0; ; Iter++ )
         {
-            pTemp = Saig_ManProofRefine( p, pResult, vFlops, fVerbose );
+            pTemp = Saig_ManProofRefine( p, pResult, vFlops, nFramesBmc, nConfMaxBmc, fVerbose );
             if ( pTemp == NULL )
                 break;
             Aig_ManStop( pResult );
diff --git a/src/aig/saig/saigMiter.c b/src/aig/saig/saigMiter.c
index 71bdadf6..0a9f230b 100644
--- a/src/aig/saig/saigMiter.c
+++ b/src/aig/saig/saigMiter.c
@@ -327,7 +327,7 @@ Aig_Man_t * Saig_ManUnrollTwo( Aig_Man_t * pBot, Aig_Man_t * pTop, int nFrames )
     assert( Saig_ManRegNum(pBot) == Saig_ManRegNum(pTop) );
     assert( Saig_ManRegNum(pBot) > 0 || Saig_ManRegNum(pTop) > 0 );
     // start timeframes
-    p = Aig_ManStart( nFrames * AIG_MAX(Aig_ManObjNumMax(pBot), Aig_ManObjNumMax(pTop)) );
+    p = Aig_ManStart( nFrames * ABC_MAX(Aig_ManObjNumMax(pBot), Aig_ManObjNumMax(pTop)) );
     p->pName = Aig_UtilStrsav( "frames" );
     // create variables for register outputs
     pAig = pBot;
diff --git a/src/aig/saig/saigSimMv.c b/src/aig/saig/saigSimMv.c
index 9bc6416b..a3fdaf93 100644
--- a/src/aig/saig/saigSimMv.c
+++ b/src/aig/saig/saigSimMv.c
@@ -180,7 +180,7 @@ static inline int Saig_MvCreateObj( Saig_MvMan_t * p, int iFan0, int iFan1 )
     pNode->iFan1 = iFan1;
     pNode->iNext = 0;
     if ( iFan0 || iFan1 )
-        p->pLevels[p->nObjs] = 1 + AIG_MAX( Saig_MvLev(p, iFan0), Saig_MvLev(p, iFan1) );
+        p->pLevels[p->nObjs] = 1 + ABC_MAX( Saig_MvLev(p, iFan0), Saig_MvLev(p, iFan1) );
     else
         p->pLevels[p->nObjs] = 0, p->nPis++;
     return p->nObjs++;
diff --git a/src/aig/saig/saigSynch.c b/src/aig/saig/saigSynch.c
index ff46634e..b29fcb9b 100644
--- a/src/aig/saig/saigSynch.c
+++ b/src/aig/saig/saigSynch.c
@@ -616,7 +616,7 @@ Aig_Man_t * Saig_Synchronize( Aig_Man_t * pAig1, Aig_Man_t * pAig2, int nWords,
         return NULL;
     }
     clk = clock();
-    vSimInfo = Vec_PtrAllocSimInfo( AIG_MAX( Aig_ManObjNumMax(pAig1), Aig_ManObjNumMax(pAig2) ), 1 );
+    vSimInfo = Vec_PtrAllocSimInfo( ABC_MAX( Aig_ManObjNumMax(pAig1), Aig_ManObjNumMax(pAig2) ), 1 );
 
     // process Design 1
     RetValue = Saig_SynchSequenceRun( pAig1, vSimInfo, vSeq1, 1 );
diff --git a/src/aig/saig/saigTrans.c b/src/aig/saig/saigTrans.c
index f50af285..a92d9369 100644
--- a/src/aig/saig/saigTrans.c
+++ b/src/aig/saig/saigTrans.c
@@ -398,7 +398,7 @@ ABC_PRT( "Fraiging", clock() - clk );
 clk = clock();
     pRes2 = Saig_ManFramesInitialMapped( pAig, nFrames, nFramesMax, fInit );
 ABC_PRT( "Mapped", clock() - clk );
-    // ABC_FREE mapping
+    // free mapping
     Saig_ManStopMap2( pAig );
 clk = clock();
     pRes1 = Saig_ManFramesInitialMapped( pAig, nFrames, nFramesMax, fInit );