summaryrefslogtreecommitdiffstats
path: root/src/aig/fra
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/fra')
-rw-r--r--src/aig/fra/fra.h5
-rw-r--r--src/aig/fra/fraClass.c6
-rw-r--r--src/aig/fra/fraInd.c7
-rw-r--r--src/aig/fra/fraLcr.c2
-rw-r--r--src/aig/fra/fraSec.c6
-rw-r--r--src/aig/fra/fraSim.c2
-rw-r--r--src/aig/fra/module.make3
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-18 12:28:37 +0000