Reintroduced the old abstraction procedure Saig_ManCexAbstractionFlops() formerly called from &abs_start for backward compatibility.

src/proof/abs/abs.h

@@ -79,6 +79,31 @@ struct Abs_Par_t_
     int            nFramesNoChangeLim; // the number of last frames without changes to dump abstraction
 };
 
+// old abstraction parameters
+typedef struct Gia_ParAbs_t_ Gia_ParAbs_t;
+struct Gia_ParAbs_t_
+{
+    int            Algo;               // the algorithm to be used
+    int            nFramesMax;         // timeframes for PBA
+    int            nConfMax;           // conflicts for PBA
+    int            fDynamic;           // dynamic unfolding for PBA
+    int            fConstr;            // use constraints
+    int            nFramesBmc;         // timeframes for BMC
+    int            nConfMaxBmc;        // conflicts for BMC
+    int            nStableMax;         // the number of stable frames to quit
+    int            nRatio;             // ratio of flops to quit
+    int            TimeOut;            // approximate timeout in seconds
+    int            TimeOutVT;          // approximate timeout in seconds
+    int            nBobPar;            // Bob's parameter
+    int            fUseBdds;           // use BDDs to refine abstraction
+    int            fUseDprove;         // use 'dprove' to refine abstraction
+    int            fUseStart;          // use starting frame
+    int            fVerbose;           // verbose output
+    int            fVeryVerbose;       // printing additional information
+    int            Status;             // the problem status
+    int            nFramesDone;        // the number of frames covered
+};
+
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -127,6 +152,8 @@ extern int               Gia_GlaCountNodes( Gia_Man_t * p, Vec_Int_t * vGla );
 extern Gia_Man_t *       Abs_RpmPerform( Gia_Man_t * p, int nCutMax, int fVerbose, int fVeryVerbose );
 /*=== absRpmOld.c =========================================================*/
 extern Gia_Man_t *       Abs_RpmPerformOld( Gia_Man_t * p, int fVerbose );
+extern void              Gia_ManAbsSetDefaultParams( Gia_ParAbs_t * p );
+extern Vec_Int_t *       Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars );
 
 /*=== absOldCex.c ==========================================================*/
 extern Vec_Int_t *       Saig_ManCbaFilterFlops( Aig_Man_t * pAig, Abc_Cex_t * pAbsCex, Vec_Int_t * vFlopClasses, Vec_Int_t * vAbsFfsToAdd, int nFfsToSelect );

src/proof/abs/absOldRef.c

@@ -36,6 +36,40 @@ ABC_NAMESPACE_IMPL_START
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+/**Function*************************************************************
+
+  Synopsis    [This procedure sets default parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManAbsSetDefaultParams( Gia_ParAbs_t * p )
+{
+    memset( p, 0, sizeof(Gia_ParAbs_t) );
+    p->Algo        =        0;    // algorithm: CBA
+    p->nFramesMax  =       10;    // timeframes for PBA
+    p->nConfMax    =    10000;    // conflicts for PBA
+    p->fDynamic    =        1;    // dynamic unfolding for PBA
+    p->fConstr     =        0;    // use constraints
+    p->nFramesBmc  =      250;    // timeframes for BMC
+    p->nConfMaxBmc =     5000;    // conflicts for BMC
+    p->nStableMax  =  1000000;    // the number of stable frames to quit
+    p->nRatio      =       10;    // ratio of flops to quit
+    p->nBobPar     =  1000000;    // the number of frames before trying to quit
+    p->fUseBdds    =        0;    // use BDDs to refine abstraction
+    p->fUseDprove  =        0;    // use 'dprove' to refine abstraction
+    p->fUseStart   =        1;    // use starting frame
+    p->fVerbose    =        0;    // verbose output
+    p->fVeryVerbose=        0;    // printing additional information
+    p->Status      =       -1;    // the problem status
+    p->nFramesDone =       -1;    // the number of rames covered
+}
+
+
 /**Function*************************************************************
 
   Synopsis    [Derive a new counter-example.]
@@ -361,6 +395,76 @@ int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int nFfToAd
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Computes the flops to remain after abstraction.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+ 
+***********************************************************************/
+Vec_Int_t * Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars )
+{
+    int nUseStart = 0;
+    Aig_Man_t * pAbs, * pTemp;
+    Vec_Int_t * vFlops;
+    int Iter, clk = clock(), clk2 = clock();//, iFlop;
+    assert( Aig_ManRegNum(p) > 0 );
+    if ( pPars->fVerbose )
+        printf( "Performing counter-example-based refinement.\n" );
+    Aig_ManSetCioIds( p );
+    vFlops = Vec_IntStartNatural( 1 );
+/*
+    iFlop = Saig_ManFindFirstFlop( p );
+    assert( iFlop >= 0 );
+    vFlops = Vec_IntAlloc( 1 );
+    Vec_IntPush( vFlops, iFlop );
+*/
+    // create the resulting AIG
+    pAbs = Saig_ManDupAbstraction( p, vFlops );
+    if ( !pPars->fVerbose )
+    {
+        printf( "Init : " );
+        Aig_ManPrintStats( pAbs );
+    }
+    printf( "Refining abstraction...\n" );
+    for ( Iter = 0; ; Iter++ )
+    {
+        pTemp = Saig_ManCexRefine( p, pAbs, vFlops, pPars->nFramesBmc, pPars->nConfMaxBmc, pPars->fUseBdds, pPars->fUseDprove, pPars->fVerbose, pPars->fUseStart?&nUseStart:NULL, &pPars->Status, &pPars->nFramesDone );
+        if ( pTemp == NULL )
+        {
+            ABC_FREE( p->pSeqModel );
+            p->pSeqModel = pAbs->pSeqModel;
+            pAbs->pSeqModel = NULL;
+            Aig_ManStop( pAbs );
+            break;
+        }
+        Aig_ManStop( pAbs );
+        pAbs = pTemp;
+        printf( "ITER %4d : ", Iter );
+        if ( !pPars->fVerbose )
+            Aig_ManPrintStats( pAbs );
+        // output the intermediate result of abstraction
+        Ioa_WriteAiger( pAbs, "gabs.aig", 0, 0 );
+//            printf( "Intermediate abstracted model was written into file \"%s\".\n", "gabs.aig" );
+        // check if the ratio is reached
+        if ( 100.0*(Aig_ManRegNum(p)-Aig_ManRegNum(pAbs))/Aig_ManRegNum(p) < 1.0*pPars->nRatio )
+        {
+            printf( "Refinements is stopped because flop reduction is less than %d%%\n", pPars->nRatio );
+            Aig_ManStop( pAbs );
+            pAbs = NULL;
+            Vec_IntFree( vFlops );
+            vFlops = NULL;
+            break;
+        }
+    }
+    return vFlops;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////