diff options
Diffstat (limited to 'src/aig/fra')
-rw-r--r-- | src/aig/fra/fra.h | 5 | ||||
-rw-r--r-- | src/aig/fra/fraClass.c | 6 | ||||
-rw-r--r-- | src/aig/fra/fraInd.c | 7 | ||||
-rw-r--r-- | src/aig/fra/fraLcr.c | 2 | ||||
-rw-r--r-- | src/aig/fra/fraSec.c | 6 | ||||
-rw-r--r-- | src/aig/fra/fraSim.c | 2 | ||||
-rw-r--r-- | src/aig/fra/module.make | 3 |
7 files changed, 18 insertions, 13 deletions
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index 8cd677d1..8d7116c7 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -76,6 +76,7 @@ struct Fra_Par_t_ int nFramesP; // the number of timeframes to in the prefix int nFramesK; // the number of timeframes to unroll int nMaxImps; // the maximum number of implications to consider + int nMaxLevs; // the maximum number of levels to consider int fRewrite; // use rewriting for constraint reduction int fLatchCorr; // computes latch correspondence only int fUseImps; // use implications @@ -245,7 +246,7 @@ extern Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig ); extern void Fra_ClassesStop( Fra_Cla_t * p ); extern void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed ); extern void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose ); -extern void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr ); +extern void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr, int nMaxLevs ); extern int Fra_ClassesRefine( Fra_Cla_t * p ); extern int Fra_ClassesRefine1( Fra_Cla_t * p, int fRefineNewClass, int * pSkipped ); extern int Fra_ClassesCountLits( Fra_Cla_t * p ); @@ -274,7 +275,7 @@ extern double Fra_ImpComputeStateSpaceRatio( Fra_Man_t * p ); extern int Fra_ImpVerifyUsingSimulation( Fra_Man_t * p ); extern void Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew ); /*=== fraInd.c ========================================================*/ -extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose, int * pnIter ); +extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int nMaxImps, int nMaxLevs, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose, int * pnIter ); /*=== fraLcr.c ========================================================*/ extern Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter ); /*=== fraMan.c ========================================================*/ diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c index 962e7f7b..2d03e65d 100644 --- a/src/aig/fra/fraClass.c +++ b/src/aig/fra/fraClass.c @@ -270,7 +270,7 @@ void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose ) SeeAlso [] ***********************************************************************/ -void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr ) +void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr, int nMaxLevs ) { Aig_Obj_t ** ppTable, ** ppNexts; Aig_Obj_t * pObj, * pTemp; @@ -296,8 +296,8 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr ) if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) continue; // skip the node with more that the given number of levels -// if ( pObj->Level > 3 ) -// continue; + if ( nMaxLevs && (int)pObj->Level >= nMaxLevs ) + continue; } // hash the node by its simulation info iEntry = p->pFuncNodeHash( pObj, nTableSize ); diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c index dbc6401f..1c2140bb 100644 --- a/src/aig/fra/fraInd.c +++ b/src/aig/fra/fraInd.c @@ -243,7 +243,7 @@ void Fra_FramesAddMore( Aig_Man_t * p, int nFrames ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose, int * pnIter ) +Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int nMaxImps, int nMaxLevs, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose, int * pnIter ) { int fUseSimpleCnf = 0; int fUseOldSimulation = 0; @@ -282,12 +282,13 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, pPars->nFramesP = nFramesP; pPars->nFramesK = nFramesK; pPars->nMaxImps = nMaxImps; + pPars->nMaxLevs = nMaxLevs; pPars->fVerbose = fVerbose; pPars->fRewrite = fRewrite; pPars->fLatchCorr = fLatchCorr; pPars->fUseImps = fUseImps; pPars->fWriteImps = fWriteImps; - + // start the fraig manager for this run p = Fra_ManStart( pManAig, pPars ); // derive and refine e-classes using K initialized frames @@ -313,7 +314,7 @@ if ( fVerbose ) { PRT( "Time", clock() - clk ); } - Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr ); + Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr, p->pPars->nMaxLevs ); // Fra_ClassesPostprocess( p->pCla ); // allocate new simulation manager for simulating counter-examples Fra_SmlStop( p->pSml ); diff --git a/src/aig/fra/fraLcr.c b/src/aig/fra/fraLcr.c index daa789a8..a6460ed7 100644 --- a/src/aig/fra/fraLcr.c +++ b/src/aig/fra/fraLcr.c @@ -550,7 +550,7 @@ timeSim = clock() - clk2; // get preliminary info about equivalence classes pTemp->pCla = p->pCla = Fra_ClassesStart( p->pAig ); - Fra_ClassesPrepare( p->pCla, 1 ); + Fra_ClassesPrepare( p->pCla, 1, 0 ); p->pCla->pFuncNodeIsConst = Fra_LcrNodeIsConst; p->pCla->pFuncNodesAreEqual = Fra_LcrNodesAreEqual; Fra_SmlStop( pTemp->pSml ); diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index 17a7335c..4ccb48e3 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -49,7 +49,7 @@ int Fra_FraigSec2( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose { nFrames = nFramesFix; // perform seq sweeping for one frame number - pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter ); + pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter ); } else { @@ -57,7 +57,7 @@ int Fra_FraigSec2( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose for ( nFrames = 1; ; nFrames++ ) { clk = clock(); - pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter ); + pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter ); RetValue = Fra_FraigMiterStatus( pNew ); if ( fVerbose ) { @@ -185,7 +185,7 @@ PRT( "Time", clock() - clk ); for ( nFrames = 1; nFrames <= nFramesMax; nFrames *= 2 ) { clk = clock(); - pNew = Fra_FraigInduction( pTemp = pNew, 0, nFrames, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter ); + pNew = Fra_FraigInduction( pTemp = pNew, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter ); Aig_ManStop( pTemp ); RetValue = Fra_FraigMiterStatus( pNew ); if ( fVerbose ) diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c index 3e8f2da1..1ad2d4f7 100644 --- a/src/aig/fra/fraSim.c +++ b/src/aig/fra/fraSim.c @@ -685,7 +685,7 @@ void Fra_SmlSimulate( Fra_Man_t * p, int fInit ) Fra_SmlSimulateOne( p->pSml ); if ( p->pPars->fProve && Fra_SmlCheckOutput(p) ) return; - Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr ); + Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr, 0 ); // Fra_ClassesPrint( p->pCla, 0 ); if ( fVerbose ) printf( "Starting classes = %5d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) ); diff --git a/src/aig/fra/module.make b/src/aig/fra/module.make index e7264fdc..ffaca75c 100644 --- a/src/aig/fra/module.make +++ b/src/aig/fra/module.make @@ -1,12 +1,15 @@ SRC += src/aig/fra/fraBmc.c \ src/aig/fra/fraCec.c \ src/aig/fra/fraClass.c \ + src/aig/fra/fraClau.c \ + src/aig/fra/fraClaus.c \ src/aig/fra/fraCnf.c \ src/aig/fra/fraCore.c \ src/aig/fra/fraImp.c \ src/aig/fra/fraInd.c \ src/aig/fra/fraLcr.c \ src/aig/fra/fraMan.c \ + src/aig/fra/fraPart.c \ src/aig/fra/fraSat.c \ src/aig/fra/fraSec.c \ src/aig/fra/fraSim.c |