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

2 files changed, 162 insertions, 31 deletions

diff --git a/src/proof/abs/abs.h b/src/proof/abs/abs.h
index 537a8a36..bef7ad05 100644
--- a/src/proof/abs/abs.h
+++ b/src/proof/abs/abs.h
@@ -46,37 +46,62 @@ ABC_NAMESPACE_HEADER_START
 typedef struct Abs_Par_t_ Abs_Par_t;
 struct Abs_Par_t_
 {
-    int                  nFramesMax;         // maximum frames
-    int                  nFramesStart;       // starting frame 
-    int                  nFramesPast;        // overlap frames
-    int                  nConfLimit;         // conflict limit
-    int                  nLearnedMax;        // max number of learned clauses
-    int                  nLearnedStart;      // max number of learned clauses
-    int                  nLearnedDelta;      // delta increase of learned clauses
-    int                  nLearnedPerce;      // percentage of clauses to leave
-    int                  nTimeOut;           // timeout in seconds
-    int                  nRatioMin;          // stop when less than this % of object is abstracted
-    int                  nRatioMax;          // restart when the number of abstracted object is more than this
-    int                  fUseTermVars;       // use terminal variables
-    int                  fUseRollback;       // use rollback to the starting number of frames
-    int                  fPropFanout;        // propagate fanout implications
-    int                  fAddLayer;          // refinement strategy by adding layers
-    int                  fNewRefine;         // uses new refinement heuristics
-    int                  fUseSkip;           // skip proving intermediate timeframes
-    int                  fUseSimple;         // use simple CNF construction
-    int                  fSkipHash;          // skip hashing CNF while unrolling
-    int                  fUseFullProof;      // use full proof for UNSAT cores
-    int                  fDumpVabs;          // dumps the abstracted model
-    int                  fDumpMabs;          // dumps the original AIG with abstraction map
-    int                  fCallProver;        // calls the prover
-    int                  fSimpProver;        // calls simplification before prover
-    char *               pFileVabs;          // dumps the abstracted model into this file
-    int                  fVerbose;           // verbose flag
-    int                  fVeryVerbose;       // print additional information
-    int                  iFrame;             // the number of frames covered
-    int                  iFrameProved;       // the number of frames proved
-    int                  nFramesNoChange;    // the number of last frames without changes
-    int                  nFramesNoChangeLim; // the number of last frames without changes to dump abstraction
+    int            nFramesMax;         // maximum frames
+    int            nFramesStart;       // starting frame 
+    int            nFramesPast;        // overlap frames
+    int            nConfLimit;         // conflict limit
+    int            nLearnedMax;        // max number of learned clauses
+    int            nLearnedStart;      // max number of learned clauses
+    int            nLearnedDelta;      // delta increase of learned clauses
+    int            nLearnedPerce;      // percentage of clauses to leave
+    int            nTimeOut;           // timeout in seconds
+    int            nRatioMin;          // stop when less than this % of object is abstracted
+    int            nRatioMax;          // restart when the number of abstracted object is more than this
+    int            fUseTermVars;       // use terminal variables
+    int            fUseRollback;       // use rollback to the starting number of frames
+    int            fPropFanout;        // propagate fanout implications
+    int            fAddLayer;          // refinement strategy by adding layers
+    int            fNewRefine;         // uses new refinement heuristics
+    int            fUseSkip;           // skip proving intermediate timeframes
+    int            fUseSimple;         // use simple CNF construction
+    int            fSkipHash;          // skip hashing CNF while unrolling
+    int            fUseFullProof;      // use full proof for UNSAT cores
+    int            fDumpVabs;          // dumps the abstracted model
+    int            fDumpMabs;          // dumps the original AIG with abstraction map
+    int            fCallProver;        // calls the prover
+    int            fSimpProver;        // calls simplification before prover
+    char *         pFileVabs;          // dumps the abstracted model into this file
+    int            fVerbose;           // verbose flag
+    int            fVeryVerbose;       // print additional information
+    int            iFrame;             // the number of frames covered
+    int            iFrameProved;       // the number of frames proved
+    int            nFramesNoChange;    // the number of last frames without changes
+    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
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -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 );
diff --git a/src/proof/abs/absOldRef.c b/src/proof/abs/absOldRef.c
index 0b99ab40..3199803f 100644
--- a/src/proof/abs/absOldRef.c
+++ b/src/proof/abs/absOldRef.c
@@ -38,6 +38,40 @@ ABC_NAMESPACE_IMPL_START
 
 /**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.]
 
   Description []
@@ -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                                ///
 ////////////////////////////////////////////////////////////////////////